|
0 |
#! /bin/sh /usr/share/dpatch/dpatch-run
|
|
1 |
## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram <smimram@debian.org>
|
|
2 |
##
|
|
3 |
## All lines beginning with `## DP:' are a description of the patch.
|
|
4 |
## DP: Patch provided by coq's upstream to fix problems with OCaml 3.09.
|
|
5 |
## DP: ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/patch-coq-8.0pl3-ocaml-3.09
|
|
6 |
|
|
7 |
@DPATCH@
|
|
8 |
diff -urNad coq-8.0pl3~/Makefile coq-8.0pl3/Makefile
|
|
9 |
--- coq-8.0pl3~/Makefile 2006-01-11 23:18:05.000000000 +0000
|
|
10 |
+++ coq-8.0pl3/Makefile 2006-02-19 11:28:43.000000000 +0000
|
|
11 |
@@ -77,8 +77,8 @@
|
|
12 |
|
|
13 |
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
|
|
14 |
|
|
15 |
-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
|
|
16 |
-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
|
|
17 |
+BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
|
|
18 |
+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y
|
|
19 |
OCAMLDEP=ocamldep
|
|
20 |
DEPFLAGS=-slash $(LOCALINCLUDES)
|
|
21 |
|
|
22 |
diff -urNad coq-8.0pl3~/contrib/first-order/sequent.ml coq-8.0pl3/contrib/first-order/sequent.ml
|
|
23 |
--- coq-8.0pl3~/contrib/first-order/sequent.ml 2004-07-16 19:30:10.000000000 +0000
|
|
24 |
+++ coq-8.0pl3/contrib/first-order/sequent.ml 2006-02-19 11:28:43.000000000 +0000
|
|
25 |
@@ -6,7 +6,7 @@
|
|
26 |
(* * GNU Lesser General Public License Version 2.1 *)
|
|
27 |
(************************************************************************)
|
|
28 |
|
|
29 |
-(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
|
|
30 |
+(* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *)
|
|
31 |
|
|
32 |
open Term
|
|
33 |
open Util
|
|
34 |
@@ -278,7 +278,7 @@
|
|
35 |
let h dbname=
|
|
36 |
let hdb=
|
|
37 |
try
|
|
38 |
- Util.Stringmap.find dbname !searchtable
|
|
39 |
+ searchtable_map dbname
|
|
40 |
with Not_found->
|
|
41 |
error ("Firstorder: "^dbname^" : No such Hint database") in
|
|
42 |
Hint_db.iter g hdb in
|
|
43 |
diff -urNad coq-8.0pl3~/contrib/interface/blast.ml coq-8.0pl3/contrib/interface/blast.ml
|
|
44 |
--- coq-8.0pl3~/contrib/interface/blast.ml 2004-07-16 19:30:11.000000000 +0000
|
|
45 |
+++ coq-8.0pl3/contrib/interface/blast.ml 2006-02-19 11:28:43.000000000 +0000
|
|
46 |
@@ -351,16 +351,16 @@
|
|
47 |
let db_list =
|
|
48 |
List.map
|
|
49 |
(fun x ->
|
|
50 |
- try Stringmap.find x !searchtable
|
|
51 |
+ try searchtable_map x
|
|
52 |
with Not_found -> error ("EAuto: "^x^": No such Hint database"))
|
|
53 |
("core"::dbnames)
|
|
54 |
in
|
|
55 |
tclTRY (e_search_auto debug np db_list)
|
|
56 |
|
|
57 |
let full_eauto debug n gl =
|
|
58 |
- let dbnames = stringmap_dom !searchtable in
|
|
59 |
+ let dbnames = current_db_names () in
|
|
60 |
let dbnames = list_subtract dbnames ["v62"] in
|
|
61 |
- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
|
|
62 |
+ let db_list = List.map searchtable_map dbnames in
|
|
63 |
let local_db = make_local_hint_db gl in
|
|
64 |
tclTRY (e_search_auto debug n db_list) gl
|
|
65 |
|
|
66 |
@@ -369,8 +369,6 @@
|
|
67 |
(**********************************************************************
|
|
68 |
copié de tactics/auto.ml on a juste modifié search_gen
|
|
69 |
*)
|
|
70 |
-let searchtable_map name =
|
|
71 |
- Stringmap.find name !searchtable
|
|
72 |
|
|
73 |
(* local_db is a Hint database containing the hypotheses of current goal *)
|
|
74 |
(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
|
|
75 |
@@ -499,9 +497,9 @@
|
|
76 |
let default_search_depth = ref 5
|
|
77 |
|
|
78 |
let full_auto n gl =
|
|
79 |
- let dbnames = stringmap_dom !searchtable in
|
|
80 |
+ let dbnames = current_db_names () in
|
|
81 |
let dbnames = list_subtract dbnames ["v62"] in
|
|
82 |
- let db_list = List.map (fun x -> searchtable_map x) dbnames in
|
|
83 |
+ let db_list = List.map searchtable_map dbnames in
|
|
84 |
let hyps = pf_hyps gl in
|
|
85 |
tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
|
|
86 |
|
|
87 |
diff -urNad coq-8.0pl3~/interp/symbols.ml coq-8.0pl3/interp/symbols.ml
|
|
88 |
--- coq-8.0pl3~/interp/symbols.ml 2004-11-17 09:33:38.000000000 +0000
|
|
89 |
+++ coq-8.0pl3/interp/symbols.ml 2006-02-19 11:28:43.000000000 +0000
|
|
90 |
@@ -6,7 +6,7 @@
|
|
91 |
(* * GNU Lesser General Public License Version 2.1 *)
|
|
92 |
(************************************************************************)
|
|
93 |
|
|
94 |
-(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
|
|
95 |
+(* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *)
|
|
96 |
|
|
97 |
(*i*)
|
|
98 |
open Util
|
|
99 |
@@ -43,18 +43,18 @@
|
|
100 |
type delimiters = string
|
|
101 |
|
|
102 |
type scope = {
|
|
103 |
- notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
|
|
104 |
+ notations: (string, interpretation * (dir_path * string) * bool) Gmap.t;
|
|
105 |
delimiters: delimiters option
|
|
106 |
}
|
|
107 |
|
|
108 |
(* Uninterpreted notation map: notation -> level * dir_path *)
|
|
109 |
-let notation_level_map = ref Stringmap.empty
|
|
110 |
+let notation_level_map = ref Gmap.empty
|
|
111 |
|
|
112 |
(* Scopes table: scope_name -> symbol_interpretation *)
|
|
113 |
-let scope_map = ref Stringmap.empty
|
|
114 |
+let scope_map = ref Gmap.empty
|
|
115 |
|
|
116 |
let empty_scope = {
|
|
117 |
- notations = Stringmap.empty;
|
|
118 |
+ notations = Gmap.empty;
|
|
119 |
delimiters = None
|
|
120 |
}
|
|
121 |
|
|
122 |
@@ -62,20 +62,20 @@
|
|
123 |
let type_scope = "type_scope" (* special scope used for interpreting types *)
|
|
124 |
|
|
125 |
let init_scope_map () =
|
|
126 |
- scope_map := Stringmap.add default_scope empty_scope !scope_map;
|
|
127 |
- scope_map := Stringmap.add type_scope empty_scope !scope_map
|
|
128 |
+ scope_map := Gmap.add default_scope empty_scope !scope_map;
|
|
129 |
+ scope_map := Gmap.add type_scope empty_scope !scope_map
|
|
130 |
|
|
131 |
(**********************************************************************)
|
|
132 |
(* Operations on scopes *)
|
|
133 |
|
|
134 |
let declare_scope scope =
|
|
135 |
- try let _ = Stringmap.find scope !scope_map in ()
|
|
136 |
+ try let _ = Gmap.find scope !scope_map in ()
|
|
137 |
with Not_found ->
|
|
138 |
(* Options.if_verbose message ("Creating scope "^scope);*)
|
|
139 |
- scope_map := Stringmap.add scope empty_scope !scope_map
|
|
140 |
+ scope_map := Gmap.add scope empty_scope !scope_map
|
|
141 |
|
|
142 |
let find_scope scope =
|
|
143 |
- try Stringmap.find scope !scope_map
|
|
144 |
+ try Gmap.find scope !scope_map
|
|
145 |
with Not_found -> error ("Scope "^scope^" is not declared")
|
|
146 |
|
|
147 |
let check_scope sc = let _ = find_scope sc in ()
|
|
148 |
@@ -124,7 +124,7 @@
|
|
149 |
(**********************************************************************)
|
|
150 |
(* Delimiters *)
|
|
151 |
|
|
152 |
-let delimiters_map = ref Stringmap.empty
|
|
153 |
+let delimiters_map = ref Gmap.empty
|
|
154 |
|
|
155 |
let declare_delimiters scope key =
|
|
156 |
let sc = find_scope scope in
|
|
157 |
@@ -134,15 +134,15 @@
|
|
158 |
warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
|
|
159 |
end;
|
|
160 |
let sc = { sc with delimiters = Some key } in
|
|
161 |
- scope_map := Stringmap.add scope sc !scope_map;
|
|
162 |
- if Stringmap.mem key !delimiters_map then begin
|
|
163 |
- let oldsc = Stringmap.find key !delimiters_map in
|
|
164 |
+ scope_map := Gmap.add scope sc !scope_map;
|
|
165 |
+ if Gmap.mem key !delimiters_map then begin
|
|
166 |
+ let oldsc = Gmap.find key !delimiters_map in
|
|
167 |
Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
|
|
168 |
end;
|
|
169 |
- delimiters_map := Stringmap.add key scope !delimiters_map
|
|
170 |
+ delimiters_map := Gmap.add key scope !delimiters_map
|
|
171 |
|
|
172 |
let find_delimiters_scope loc key =
|
|
173 |
- try Stringmap.find key !delimiters_map
|
|
174 |
+ try Gmap.find key !delimiters_map
|
|
175 |
with Not_found ->
|
|
176 |
user_err_loc
|
|
177 |
(loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
|
|
178 |
@@ -229,7 +229,7 @@
|
|
179 |
let find_with_delimiters = function
|
|
180 |
| None -> None
|
|
181 |
| Some scope ->
|
|
182 |
- match (Stringmap.find scope !scope_map).delimiters with
|
|
183 |
+ match (Gmap.find scope !scope_map).delimiters with
|
|
184 |
| Some key -> Some (Some scope, Some key)
|
|
185 |
| None -> None
|
|
186 |
|
|
187 |
@@ -257,23 +257,23 @@
|
|
188 |
(* Uninterpreted notation levels *)
|
|
189 |
|
|
190 |
let declare_notation_level ntn level =
|
|
191 |
- if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
|
|
192 |
+ if not !Options.v7 & Gmap.mem ntn !notation_level_map then
|
|
193 |
error ("Notation "^ntn^" is already assigned a level");
|
|
194 |
- notation_level_map := Stringmap.add ntn level !notation_level_map
|
|
195 |
+ notation_level_map := Gmap.add ntn level !notation_level_map
|
|
196 |
|
|
197 |
let level_of_notation ntn =
|
|
198 |
- Stringmap.find ntn !notation_level_map
|
|
199 |
+ Gmap.find ntn !notation_level_map
|
|
200 |
|
|
201 |
(* The mapping between notations and their interpretation *)
|
|
202 |
|
|
203 |
let declare_notation_interpretation ntn scopt pat df pp8only =
|
|
204 |
let scope = match scopt with Some s -> s | None -> default_scope in
|
|
205 |
let sc = find_scope scope in
|
|
206 |
- if Stringmap.mem ntn sc.notations && Options.is_verbose () then
|
|
207 |
+ if Gmap.mem ntn sc.notations && Options.is_verbose () then
|
|
208 |
warning ("Notation "^ntn^" was already used"^
|
|
209 |
(if scopt = None then "" else " in scope "^scope));
|
|
210 |
- let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
|
|
211 |
- scope_map := Stringmap.add scope sc !scope_map;
|
|
212 |
+ let sc = { sc with notations = Gmap.add ntn (pat,df,pp8only) sc.notations } in
|
|
213 |
+ scope_map := Gmap.add scope sc !scope_map;
|
|
214 |
if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
|
|
215 |
|
|
216 |
let declare_uninterpretation rule (metas,c as pat) =
|
|
217 |
@@ -292,7 +292,7 @@
|
|
218 |
let rec interp_notation loc ntn scopes =
|
|
219 |
let f sc =
|
|
220 |
let scope = find_scope sc in
|
|
221 |
- let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
|
|
222 |
+ let (pat,df,pp8only) = Gmap.find ntn scope.notations in
|
|
223 |
if pp8only then raise Not_found;
|
|
224 |
pat,(df,if sc = default_scope then None else Some sc) in
|
|
225 |
try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
|
|
226 |
@@ -308,7 +308,7 @@
|
|
227 |
|
|
228 |
let availability_of_notation (ntn_scope,ntn) scopes =
|
|
229 |
let f scope =
|
|
230 |
- Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
|
|
231 |
+ Gmap.mem ntn (Gmap.find scope !scope_map).notations in
|
|
232 |
find_without_delimiters f (ntn_scope,Some ntn) scopes
|
|
233 |
|
|
234 |
let rec interp_numeral_gen loc f n = function
|
|
235 |
@@ -356,8 +356,8 @@
|
|
236 |
let exists_notation_in_scope scopt ntn r =
|
|
237 |
let scope = match scopt with Some s -> s | None -> default_scope in
|
|
238 |
try
|
|
239 |
- let sc = Stringmap.find scope !scope_map in
|
|
240 |
- let (r',_,pp8only) = Stringmap.find ntn sc.notations in
|
|
241 |
+ let sc = Gmap.find scope !scope_map in
|
|
242 |
+ let (r',_,pp8only) = Gmap.find ntn sc.notations in
|
|
243 |
r' = r, pp8only
|
|
244 |
with Not_found -> false, false
|
|
245 |
|
|
246 |
@@ -487,14 +487,14 @@
|
|
247 |
|
|
248 |
let pr_named_scope prraw scope sc =
|
|
249 |
(if scope = default_scope then
|
|
250 |
- match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
|
|
251 |
+ match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
|
|
252 |
| 0 -> str "No lonely notation"
|
|
253 |
| n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
|
|
254 |
else
|
|
255 |
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
|
|
256 |
++ fnl ()
|
|
257 |
++ pr_scope_classes scope
|
|
258 |
- ++ Stringmap.fold
|
|
259 |
+ ++ Gmap.fold
|
|
260 |
(fun ntn ((_,r),(_,df),_) strm ->
|
|
261 |
pr_notation_info prraw df r ++ fnl () ++ strm)
|
|
262 |
sc.notations (mt ())
|
|
263 |
@@ -502,12 +502,12 @@
|
|
264 |
let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
|
|
265 |
|
|
266 |
let pr_scopes prraw =
|
|
267 |
- Stringmap.fold
|
|
268 |
+ Gmap.fold
|
|
269 |
(fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
|
|
270 |
!scope_map (mt ())
|
|
271 |
|
|
272 |
let rec find_default ntn = function
|
|
273 |
- | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
|
|
274 |
+ | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
|
|
275 |
Some scope
|
|
276 |
| SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
|
|
277 |
| _::scopes -> find_default ntn scopes
|
|
278 |
@@ -531,9 +531,9 @@
|
|
279 |
if String.contains ntn ' ' then (=) ntn
|
|
280 |
else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
|
|
281 |
let l =
|
|
282 |
- Stringmap.fold
|
|
283 |
+ Gmap.fold
|
|
284 |
(fun scope_name sc ->
|
|
285 |
- Stringmap.fold (fun ntn ((_,r),df,_) l ->
|
|
286 |
+ Gmap.fold (fun ntn ((_,r),df,_) l ->
|
|
287 |
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
|
|
288 |
map [] in
|
|
289 |
let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
|
|
290 |
@@ -560,7 +560,7 @@
|
|
291 |
|
|
292 |
let collect_notation_in_scope scope sc known =
|
|
293 |
assert (scope <> default_scope);
|
|
294 |
- Stringmap.fold
|
|
295 |
+ Gmap.fold
|
|
296 |
(fun ntn ((_,r),(_,df),_) (l,known as acc) ->
|
|
297 |
if List.mem ntn known then acc else ((df,r)::l,ntn::known))
|
|
298 |
sc.notations ([],known)
|
|
299 |
@@ -578,7 +578,7 @@
|
|
300 |
if List.mem ntn knownntn then (all,knownntn)
|
|
301 |
else
|
|
302 |
let ((_,r),(_,df),_) =
|
|
303 |
- Stringmap.find ntn (find_scope default_scope).notations in
|
|
304 |
+ Gmap.find ntn (find_scope default_scope).notations in
|
|
305 |
let all' = match all with
|
|
306 |
| (s,lonelyntn)::rest when s = default_scope ->
|
|
307 |
(s,(df,r)::lonelyntn)::rest
|
|
308 |
@@ -614,13 +614,13 @@
|
|
309 |
|
|
310 |
(* Concrete syntax for symbolic-extension table *)
|
|
311 |
let printing_rules =
|
|
312 |
- ref (Stringmap.empty : unparsing_rule Stringmap.t)
|
|
313 |
+ ref (Gmap.empty : (string, unparsing_rule) Gmap.t)
|
|
314 |
|
|
315 |
let declare_notation_printing_rule ntn unpl =
|
|
316 |
- printing_rules := Stringmap.add ntn unpl !printing_rules
|
|
317 |
+ printing_rules := Gmap.add ntn unpl !printing_rules
|
|
318 |
|
|
319 |
let find_notation_printing_rule ntn =
|
|
320 |
- try Stringmap.find ntn !printing_rules
|
|
321 |
+ try Gmap.find ntn !printing_rules
|
|
322 |
with Not_found -> anomaly ("No printing rule found for "^ntn)
|
|
323 |
|
|
324 |
(**********************************************************************)
|
|
325 |
@@ -644,13 +644,13 @@
|
|
326 |
let init () =
|
|
327 |
init_scope_map ();
|
|
328 |
(*
|
|
329 |
- scope_stack := Stringmap.empty
|
|
330 |
+ scope_stack := Gmap.empty
|
|
331 |
arguments_scope := Refmap.empty
|
|
332 |
*)
|
|
333 |
- notation_level_map := Stringmap.empty;
|
|
334 |
- delimiters_map := Stringmap.empty;
|
|
335 |
+ notation_level_map := Gmap.empty;
|
|
336 |
+ delimiters_map := Gmap.empty;
|
|
337 |
notations_key_table := Gmapl.empty;
|
|
338 |
- printing_rules := Stringmap.empty;
|
|
339 |
+ printing_rules := Gmap.empty;
|
|
340 |
class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
|
|
341 |
|
|
342 |
let _ =
|
|
343 |
diff -urNad coq-8.0pl3~/tactics/auto.ml coq-8.0pl3/tactics/auto.ml
|
|
344 |
--- coq-8.0pl3~/tactics/auto.ml 2005-05-15 12:47:04.000000000 +0000
|
|
345 |
+++ coq-8.0pl3/tactics/auto.ml 2006-02-19 11:28:43.000000000 +0000
|
|
346 |
@@ -6,7 +6,7 @@
|
|
347 |
(* * GNU Lesser General Public License Version 2.1 *)
|
|
348 |
(************************************************************************)
|
|
349 |
|
|
350 |
-(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
|
|
351 |
+(* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *)
|
|
352 |
|
|
353 |
open Pp
|
|
354 |
open Util
|
|
355 |
@@ -134,24 +134,28 @@
|
|
356 |
|
|
357 |
end
|
|
358 |
|
|
359 |
-type frozen_hint_db_table = Hint_db.t Stringmap.t
|
|
360 |
+module Hintdbmap = Gmap
|
|
361 |
|
|
362 |
-type hint_db_table = Hint_db.t Stringmap.t ref
|
|
363 |
+type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t
|
|
364 |
+
|
|
365 |
+type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref
|
|
366 |
|
|
367 |
type hint_db_name = string
|
|
368 |
|
|
369 |
-let searchtable = (ref Stringmap.empty : hint_db_table)
|
|
370 |
+let searchtable = (ref Hintdbmap.empty : hint_db_table)
|
|
371 |
|
|
372 |
let searchtable_map name =
|
|
373 |
- Stringmap.find name !searchtable
|
|
374 |
+ Hintdbmap.find name !searchtable
|
|
375 |
let searchtable_add (name,db) =
|
|
376 |
- searchtable := Stringmap.add name db !searchtable
|
|
377 |
+ searchtable := Hintdbmap.add name db !searchtable
|
|
378 |
+let current_db_names () =
|
|
379 |
+ Hintdbmap.dom !searchtable
|
|
380 |
|
|
381 |
(**************************************************************************)
|
|
382 |
(* Definition of the summary *)
|
|
383 |
(**************************************************************************)
|
|
384 |
|
|
385 |
-let init () = searchtable := Stringmap.empty
|
|
386 |
+let init () = searchtable := Hintdbmap.empty
|
|
387 |
let freeze () = !searchtable
|
|
388 |
let unfreeze fs = searchtable := fs
|
|
389 |
|
|
390 |
@@ -498,7 +502,7 @@
|
|
391 |
|
|
392 |
(* Print all hints associated to head c in any database *)
|
|
393 |
let fmt_hint_list_for_head c =
|
|
394 |
- let dbs = stringmap_to_list !searchtable in
|
|
395 |
+ let dbs = Hintdbmap.to_list !searchtable in
|
|
396 |
let valid_dbs =
|
|
397 |
map_succeed
|
|
398 |
(fun (name,db) -> (name,db,Hint_db.map_all c db))
|
|
399 |
@@ -523,7 +527,7 @@
|
|
400 |
| [] -> assert false
|
|
401 |
in
|
|
402 |
let hd = head_of_constr_reference hdc in
|
|
403 |
- let dbs = stringmap_to_list !searchtable in
|
|
404 |
+ let dbs = Hintdbmap.to_list !searchtable in
|
|
405 |
let valid_dbs =
|
|
406 |
if occur_existential cl then
|
|
407 |
map_succeed
|
|
408 |
@@ -568,7 +572,7 @@
|
|
409 |
|
|
410 |
(* displays all the hints of all databases *)
|
|
411 |
let print_searchtable () =
|
|
412 |
- Stringmap.iter
|
|
413 |
+ Hintdbmap.iter
|
|
414 |
(fun name db ->
|
|
415 |
msg (str "In the database " ++ str name ++ fnl ());
|
|
416 |
print_hint_db db)
|
|
417 |
@@ -693,7 +697,7 @@
|
|
418 |
tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
|
|
419 |
|
|
420 |
let full_trivial gl =
|
|
421 |
- let dbnames = stringmap_dom !searchtable in
|
|
422 |
+ let dbnames = Hintdbmap.dom !searchtable in
|
|
423 |
let dbnames = list_subtract dbnames ["v62"] in
|
|
424 |
let db_list = List.map (fun x -> searchtable_map x) dbnames in
|
|
425 |
tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
|
|
426 |
@@ -798,7 +802,7 @@
|
|
427 |
let default_auto = auto !default_search_depth []
|
|
428 |
|
|
429 |
let full_auto n gl =
|
|
430 |
- let dbnames = stringmap_dom !searchtable in
|
|
431 |
+ let dbnames = Hintdbmap.dom !searchtable in
|
|
432 |
let dbnames = list_subtract dbnames ["v62"] in
|
|
433 |
let db_list = List.map (fun x -> searchtable_map x) dbnames in
|
|
434 |
let hyps = pf_hyps gl in
|
|
435 |
@@ -911,7 +915,7 @@
|
|
436 |
to_add empty_named_context in
|
|
437 |
let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
|
|
438 |
let db = Hint_db.add_list db0 (make_local_hint_db g) in
|
|
439 |
- super_search n [Stringmap.find "core" !searchtable] db argl g
|
|
440 |
+ super_search n [Hintdbmap.find "core" !searchtable] db argl g
|
|
441 |
|
|
442 |
let superauto n to_add argl =
|
|
443 |
tclTRY (tclCOMPLETE (search_superauto n to_add argl))
|
|
444 |
diff -urNad coq-8.0pl3~/tactics/auto.mli coq-8.0pl3/tactics/auto.mli
|
|
445 |
--- coq-8.0pl3~/tactics/auto.mli 2005-01-21 16:41:52.000000000 +0000
|
|
446 |
+++ coq-8.0pl3/tactics/auto.mli 2006-02-19 11:28:43.000000000 +0000
|
|
447 |
@@ -6,7 +6,7 @@
|
|
448 |
(* * GNU Lesser General Public License Version 2.1 *)
|
|
449 |
(************************************************************************)
|
|
450 |
|
|
451 |
-(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
|
|
452 |
+(*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*)
|
|
453 |
|
|
454 |
(*i*)
|
|
455 |
open Util
|
|
456 |
@@ -56,12 +56,16 @@
|
|
457 |
val iter : (constr_label -> stored_data list -> unit) -> t -> unit
|
|
458 |
end
|
|
459 |
|
|
460 |
-type frozen_hint_db_table = Hint_db.t Stringmap.t
|
|
461 |
+type frozen_hint_db_table
|
|
462 |
|
|
463 |
-type hint_db_table = Hint_db.t Stringmap.t ref
|
|
464 |
+type hint_db_table
|
|
465 |
|
|
466 |
type hint_db_name = string
|
|
467 |
|
|
468 |
+val searchtable_map : hint_db_name -> Hint_db.t
|
|
469 |
+
|
|
470 |
+val current_db_names : unit -> hint_db_name list
|
|
471 |
+
|
|
472 |
val add_hints : locality_flag -> hint_db_name list -> hints -> unit
|
|
473 |
|
|
474 |
val print_searchtable : unit -> unit
|
|
475 |
diff -urNad coq-8.0pl3~/tactics/eauto.ml4 coq-8.0pl3/tactics/eauto.ml4
|
|
476 |
--- coq-8.0pl3~/tactics/eauto.ml4 2004-07-16 19:30:52.000000000 +0000
|
|
477 |
+++ coq-8.0pl3/tactics/eauto.ml4 2006-02-19 11:28:43.000000000 +0000
|
|
478 |
@@ -8,7 +8,7 @@
|
|
479 |
|
|
480 |
(*i camlp4deps: "parsing/grammar.cma" i*)
|
|
481 |
|
|
482 |
-(* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *)
|
|
483 |
+(* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *)
|
|
484 |
|
|
485 |
open Pp
|
|
486 |
open Util
|
|
487 |
@@ -391,16 +391,16 @@
|
|
488 |
let db_list =
|
|
489 |
List.map
|
|
490 |
(fun x ->
|
|
491 |
- try Stringmap.find x !searchtable
|
|
492 |
+ try searchtable_map x
|
|
493 |
with Not_found -> error ("EAuto: "^x^": No such Hint database"))
|
|
494 |
("core"::dbnames)
|
|
495 |
in
|
|
496 |
tclTRY (e_search_auto debug np db_list)
|
|
497 |
|
|
498 |
let full_eauto debug n gl =
|
|
499 |
- let dbnames = stringmap_dom !searchtable in
|
|
500 |
+ let dbnames = current_db_names () in
|
|
501 |
let dbnames = list_subtract dbnames ["v62"] in
|
|
502 |
- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
|
|
503 |
+ let db_list = List.map (fun x -> searchtable_map x) dbnames in
|
|
504 |
let local_db = make_local_hint_db gl in
|
|
505 |
tclTRY (e_search_auto debug n db_list) gl
|
|
506 |
|