[Pkg-ocaml-maint-commits] r2579 - in
trunk/packages/coq/trunk/debian: . patches
Samuel Mimram
smimram at costa.debian.org
Sun Feb 19 11:36:36 UTC 2006
Author: smimram
Date: 2006-02-19 11:36:35 +0000 (Sun, 19 Feb 2006)
New Revision: 2579
Added:
trunk/packages/coq/trunk/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
Modified:
trunk/packages/coq/trunk/debian/changelog
trunk/packages/coq/trunk/debian/patches/00list
Log:
Apply patch-coq-8.0pl3-ocaml-3.09 patch.
Modified: trunk/packages/coq/trunk/debian/changelog
===================================================================
--- trunk/packages/coq/trunk/debian/changelog 2006-02-17 19:00:24 UTC (rev 2578)
+++ trunk/packages/coq/trunk/debian/changelog 2006-02-19 11:36:35 UTC (rev 2579)
@@ -1,3 +1,10 @@
+coq (8.0pl3-2) unstable; urgency=low
+
+ * Added coq-8.0pl3-ocaml-3.09.dpatch to avoid intuition to loop forever,
+ closes: #353493.
+
+ -- Samuel Mimram <smimram at debian.org> Sun, 19 Feb 2006 11:33:21 +0000
+
coq (8.0pl3-1) unstable; urgency=low
* New upstream release.
Modified: trunk/packages/coq/trunk/debian/patches/00list
===================================================================
--- trunk/packages/coq/trunk/debian/patches/00list 2006-02-17 19:00:24 UTC (rev 2578)
+++ trunk/packages/coq/trunk/debian/patches/00list 2006-02-19 11:36:35 UTC (rev 2579)
@@ -0,0 +1 @@
+coq-8.0pl3-ocaml-3.09
Added: trunk/packages/coq/trunk/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
===================================================================
--- trunk/packages/coq/trunk/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch 2006-02-17 19:00:24 UTC (rev 2578)
+++ trunk/packages/coq/trunk/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch 2006-02-19 11:36:35 UTC (rev 2579)
@@ -0,0 +1,507 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram <smimram at debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Patch provided by coq's upstream to fix problems with OCaml 3.09.
+## DP: ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/patch-coq-8.0pl3-ocaml-3.09
+
+ at DPATCH@
+diff -urNad coq-8.0pl3~/Makefile coq-8.0pl3/Makefile
+--- coq-8.0pl3~/Makefile 2006-01-11 23:18:05.000000000 +0000
++++ coq-8.0pl3/Makefile 2006-02-19 11:28:43.000000000 +0000
+@@ -77,8 +77,8 @@
+
+ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+
+-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
+-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
++BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
++OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y
+ OCAMLDEP=ocamldep
+ DEPFLAGS=-slash $(LOCALINCLUDES)
+
+diff -urNad coq-8.0pl3~/contrib/first-order/sequent.ml coq-8.0pl3/contrib/first-order/sequent.ml
+--- coq-8.0pl3~/contrib/first-order/sequent.ml 2004-07-16 19:30:10.000000000 +0000
++++ coq-8.0pl3/contrib/first-order/sequent.ml 2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (* * GNU Lesser General Public License Version 2.1 *)
+ (************************************************************************)
+
+-(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
++(* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *)
+
+ open Term
+ open Util
+@@ -278,7 +278,7 @@
+ let h dbname=
+ let hdb=
+ try
+- Util.Stringmap.find dbname !searchtable
++ searchtable_map dbname
+ with Not_found->
+ error ("Firstorder: "^dbname^" : No such Hint database") in
+ Hint_db.iter g hdb in
+diff -urNad coq-8.0pl3~/contrib/interface/blast.ml coq-8.0pl3/contrib/interface/blast.ml
+--- coq-8.0pl3~/contrib/interface/blast.ml 2004-07-16 19:30:11.000000000 +0000
++++ coq-8.0pl3/contrib/interface/blast.ml 2006-02-19 11:28:43.000000000 +0000
+@@ -351,16 +351,16 @@
+ let db_list =
+ List.map
+ (fun x ->
+- try Stringmap.find x !searchtable
++ try searchtable_map x
+ with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+ ("core"::dbnames)
+ in
+ tclTRY (e_search_auto debug np db_list)
+
+ let full_eauto debug n gl =
+- let dbnames = stringmap_dom !searchtable in
++ let dbnames = current_db_names () in
+ let dbnames = list_subtract dbnames ["v62"] in
+- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
++ let db_list = List.map searchtable_map dbnames in
+ let local_db = make_local_hint_db gl in
+ tclTRY (e_search_auto debug n db_list) gl
+
+@@ -369,8 +369,6 @@
+ (**********************************************************************
+ copié de tactics/auto.ml on a juste modifié search_gen
+ *)
+-let searchtable_map name =
+- Stringmap.find name !searchtable
+
+ (* local_db is a Hint database containing the hypotheses of current goal *)
+ (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+@@ -499,9 +497,9 @@
+ let default_search_depth = ref 5
+
+ let full_auto n gl =
+- let dbnames = stringmap_dom !searchtable in
++ let dbnames = current_db_names () in
+ let dbnames = list_subtract dbnames ["v62"] in
+- let db_list = List.map (fun x -> searchtable_map x) dbnames in
++ let db_list = List.map searchtable_map dbnames in
+ let hyps = pf_hyps gl in
+ tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+
+diff -urNad coq-8.0pl3~/interp/symbols.ml coq-8.0pl3/interp/symbols.ml
+--- coq-8.0pl3~/interp/symbols.ml 2004-11-17 09:33:38.000000000 +0000
++++ coq-8.0pl3/interp/symbols.ml 2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (* * GNU Lesser General Public License Version 2.1 *)
+ (************************************************************************)
+
+-(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
++(* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *)
+
+ (*i*)
+ open Util
+@@ -43,18 +43,18 @@
+ type delimiters = string
+
+ type scope = {
+- notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
++ notations: (string, interpretation * (dir_path * string) * bool) Gmap.t;
+ delimiters: delimiters option
+ }
+
+ (* Uninterpreted notation map: notation -> level * dir_path *)
+-let notation_level_map = ref Stringmap.empty
++let notation_level_map = ref Gmap.empty
+
+ (* Scopes table: scope_name -> symbol_interpretation *)
+-let scope_map = ref Stringmap.empty
++let scope_map = ref Gmap.empty
+
+ let empty_scope = {
+- notations = Stringmap.empty;
++ notations = Gmap.empty;
+ delimiters = None
+ }
+
+@@ -62,20 +62,20 @@
+ let type_scope = "type_scope" (* special scope used for interpreting types *)
+
+ let init_scope_map () =
+- scope_map := Stringmap.add default_scope empty_scope !scope_map;
+- scope_map := Stringmap.add type_scope empty_scope !scope_map
++ scope_map := Gmap.add default_scope empty_scope !scope_map;
++ scope_map := Gmap.add type_scope empty_scope !scope_map
+
+ (**********************************************************************)
+ (* Operations on scopes *)
+
+ let declare_scope scope =
+- try let _ = Stringmap.find scope !scope_map in ()
++ try let _ = Gmap.find scope !scope_map in ()
+ with Not_found ->
+ (* Options.if_verbose message ("Creating scope "^scope);*)
+- scope_map := Stringmap.add scope empty_scope !scope_map
++ scope_map := Gmap.add scope empty_scope !scope_map
+
+ let find_scope scope =
+- try Stringmap.find scope !scope_map
++ try Gmap.find scope !scope_map
+ with Not_found -> error ("Scope "^scope^" is not declared")
+
+ let check_scope sc = let _ = find_scope sc in ()
+@@ -124,7 +124,7 @@
+ (**********************************************************************)
+ (* Delimiters *)
+
+-let delimiters_map = ref Stringmap.empty
++let delimiters_map = ref Gmap.empty
+
+ let declare_delimiters scope key =
+ let sc = find_scope scope in
+@@ -134,15 +134,15 @@
+ warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+ end;
+ let sc = { sc with delimiters = Some key } in
+- scope_map := Stringmap.add scope sc !scope_map;
+- if Stringmap.mem key !delimiters_map then begin
+- let oldsc = Stringmap.find key !delimiters_map in
++ scope_map := Gmap.add scope sc !scope_map;
++ if Gmap.mem key !delimiters_map then begin
++ let oldsc = Gmap.find key !delimiters_map in
+ Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+ end;
+- delimiters_map := Stringmap.add key scope !delimiters_map
++ delimiters_map := Gmap.add key scope !delimiters_map
+
+ let find_delimiters_scope loc key =
+- try Stringmap.find key !delimiters_map
++ try Gmap.find key !delimiters_map
+ with Not_found ->
+ user_err_loc
+ (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+@@ -229,7 +229,7 @@
+ let find_with_delimiters = function
+ | None -> None
+ | Some scope ->
+- match (Stringmap.find scope !scope_map).delimiters with
++ match (Gmap.find scope !scope_map).delimiters with
+ | Some key -> Some (Some scope, Some key)
+ | None -> None
+
+@@ -257,23 +257,23 @@
+ (* Uninterpreted notation levels *)
+
+ let declare_notation_level ntn level =
+- if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
++ if not !Options.v7 & Gmap.mem ntn !notation_level_map then
+ error ("Notation "^ntn^" is already assigned a level");
+- notation_level_map := Stringmap.add ntn level !notation_level_map
++ notation_level_map := Gmap.add ntn level !notation_level_map
+
+ let level_of_notation ntn =
+- Stringmap.find ntn !notation_level_map
++ Gmap.find ntn !notation_level_map
+
+ (* The mapping between notations and their interpretation *)
+
+ let declare_notation_interpretation ntn scopt pat df pp8only =
+ let scope = match scopt with Some s -> s | None -> default_scope in
+ let sc = find_scope scope in
+- if Stringmap.mem ntn sc.notations && Options.is_verbose () then
++ if Gmap.mem ntn sc.notations && Options.is_verbose () then
+ warning ("Notation "^ntn^" was already used"^
+ (if scopt = None then "" else " in scope "^scope));
+- let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
+- scope_map := Stringmap.add scope sc !scope_map;
++ let sc = { sc with notations = Gmap.add ntn (pat,df,pp8only) sc.notations } in
++ scope_map := Gmap.add scope sc !scope_map;
+ if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
+
+ let declare_uninterpretation rule (metas,c as pat) =
+@@ -292,7 +292,7 @@
+ let rec interp_notation loc ntn scopes =
+ let f sc =
+ let scope = find_scope sc in
+- let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
++ let (pat,df,pp8only) = Gmap.find ntn scope.notations in
+ if pp8only then raise Not_found;
+ pat,(df,if sc = default_scope then None else Some sc) in
+ try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
+@@ -308,7 +308,7 @@
+
+ let availability_of_notation (ntn_scope,ntn) scopes =
+ let f scope =
+- Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
++ Gmap.mem ntn (Gmap.find scope !scope_map).notations in
+ find_without_delimiters f (ntn_scope,Some ntn) scopes
+
+ let rec interp_numeral_gen loc f n = function
+@@ -356,8 +356,8 @@
+ let exists_notation_in_scope scopt ntn r =
+ let scope = match scopt with Some s -> s | None -> default_scope in
+ try
+- let sc = Stringmap.find scope !scope_map in
+- let (r',_,pp8only) = Stringmap.find ntn sc.notations in
++ let sc = Gmap.find scope !scope_map in
++ let (r',_,pp8only) = Gmap.find ntn sc.notations in
+ r' = r, pp8only
+ with Not_found -> false, false
+
+@@ -487,14 +487,14 @@
+
+ let pr_named_scope prraw scope sc =
+ (if scope = default_scope then
+- match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
++ match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+ | 0 -> str "No lonely notation"
+ | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
+ else
+ str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
+ ++ fnl ()
+ ++ pr_scope_classes scope
+- ++ Stringmap.fold
++ ++ Gmap.fold
+ (fun ntn ((_,r),(_,df),_) strm ->
+ pr_notation_info prraw df r ++ fnl () ++ strm)
+ sc.notations (mt ())
+@@ -502,12 +502,12 @@
+ let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+
+ let pr_scopes prraw =
+- Stringmap.fold
++ Gmap.fold
+ (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+ !scope_map (mt ())
+
+ let rec find_default ntn = function
+- | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
++ | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
+ Some scope
+ | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
+ | _::scopes -> find_default ntn scopes
+@@ -531,9 +531,9 @@
+ if String.contains ntn ' ' then (=) ntn
+ else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
+ let l =
+- Stringmap.fold
++ Gmap.fold
+ (fun scope_name sc ->
+- Stringmap.fold (fun ntn ((_,r),df,_) l ->
++ Gmap.fold (fun ntn ((_,r),df,_) l ->
+ if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
+ map [] in
+ let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
+@@ -560,7 +560,7 @@
+
+ let collect_notation_in_scope scope sc known =
+ assert (scope <> default_scope);
+- Stringmap.fold
++ Gmap.fold
+ (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
+ if List.mem ntn known then acc else ((df,r)::l,ntn::known))
+ sc.notations ([],known)
+@@ -578,7 +578,7 @@
+ if List.mem ntn knownntn then (all,knownntn)
+ else
+ let ((_,r),(_,df),_) =
+- Stringmap.find ntn (find_scope default_scope).notations in
++ Gmap.find ntn (find_scope default_scope).notations in
+ let all' = match all with
+ | (s,lonelyntn)::rest when s = default_scope ->
+ (s,(df,r)::lonelyntn)::rest
+@@ -614,13 +614,13 @@
+
+ (* Concrete syntax for symbolic-extension table *)
+ let printing_rules =
+- ref (Stringmap.empty : unparsing_rule Stringmap.t)
++ ref (Gmap.empty : (string, unparsing_rule) Gmap.t)
+
+ let declare_notation_printing_rule ntn unpl =
+- printing_rules := Stringmap.add ntn unpl !printing_rules
++ printing_rules := Gmap.add ntn unpl !printing_rules
+
+ let find_notation_printing_rule ntn =
+- try Stringmap.find ntn !printing_rules
++ try Gmap.find ntn !printing_rules
+ with Not_found -> anomaly ("No printing rule found for "^ntn)
+
+ (**********************************************************************)
+@@ -644,13 +644,13 @@
+ let init () =
+ init_scope_map ();
+ (*
+- scope_stack := Stringmap.empty
++ scope_stack := Gmap.empty
+ arguments_scope := Refmap.empty
+ *)
+- notation_level_map := Stringmap.empty;
+- delimiters_map := Stringmap.empty;
++ notation_level_map := Gmap.empty;
++ delimiters_map := Gmap.empty;
+ notations_key_table := Gmapl.empty;
+- printing_rules := Stringmap.empty;
++ printing_rules := Gmap.empty;
+ class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
+
+ let _ =
+diff -urNad coq-8.0pl3~/tactics/auto.ml coq-8.0pl3/tactics/auto.ml
+--- coq-8.0pl3~/tactics/auto.ml 2005-05-15 12:47:04.000000000 +0000
++++ coq-8.0pl3/tactics/auto.ml 2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (* * GNU Lesser General Public License Version 2.1 *)
+ (************************************************************************)
+
+-(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
++(* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *)
+
+ open Pp
+ open Util
+@@ -134,24 +134,28 @@
+
+ end
+
+-type frozen_hint_db_table = Hint_db.t Stringmap.t
++module Hintdbmap = Gmap
+
+-type hint_db_table = Hint_db.t Stringmap.t ref
++type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t
++
++type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref
+
+ type hint_db_name = string
+
+-let searchtable = (ref Stringmap.empty : hint_db_table)
++let searchtable = (ref Hintdbmap.empty : hint_db_table)
+
+ let searchtable_map name =
+- Stringmap.find name !searchtable
++ Hintdbmap.find name !searchtable
+ let searchtable_add (name,db) =
+- searchtable := Stringmap.add name db !searchtable
++ searchtable := Hintdbmap.add name db !searchtable
++let current_db_names () =
++ Hintdbmap.dom !searchtable
+
+ (**************************************************************************)
+ (* Definition of the summary *)
+ (**************************************************************************)
+
+-let init () = searchtable := Stringmap.empty
++let init () = searchtable := Hintdbmap.empty
+ let freeze () = !searchtable
+ let unfreeze fs = searchtable := fs
+
+@@ -498,7 +502,7 @@
+
+ (* Print all hints associated to head c in any database *)
+ let fmt_hint_list_for_head c =
+- let dbs = stringmap_to_list !searchtable in
++ let dbs = Hintdbmap.to_list !searchtable in
+ let valid_dbs =
+ map_succeed
+ (fun (name,db) -> (name,db,Hint_db.map_all c db))
+@@ -523,7 +527,7 @@
+ | [] -> assert false
+ in
+ let hd = head_of_constr_reference hdc in
+- let dbs = stringmap_to_list !searchtable in
++ let dbs = Hintdbmap.to_list !searchtable in
+ let valid_dbs =
+ if occur_existential cl then
+ map_succeed
+@@ -568,7 +572,7 @@
+
+ (* displays all the hints of all databases *)
+ let print_searchtable () =
+- Stringmap.iter
++ Hintdbmap.iter
+ (fun name db ->
+ msg (str "In the database " ++ str name ++ fnl ());
+ print_hint_db db)
+@@ -693,7 +697,7 @@
+ tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
+
+ let full_trivial gl =
+- let dbnames = stringmap_dom !searchtable in
++ let dbnames = Hintdbmap.dom !searchtable in
+ let dbnames = list_subtract dbnames ["v62"] in
+ let db_list = List.map (fun x -> searchtable_map x) dbnames in
+ tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
+@@ -798,7 +802,7 @@
+ let default_auto = auto !default_search_depth []
+
+ let full_auto n gl =
+- let dbnames = stringmap_dom !searchtable in
++ let dbnames = Hintdbmap.dom !searchtable in
+ let dbnames = list_subtract dbnames ["v62"] in
+ let db_list = List.map (fun x -> searchtable_map x) dbnames in
+ let hyps = pf_hyps gl in
+@@ -911,7 +915,7 @@
+ to_add empty_named_context in
+ let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
+ let db = Hint_db.add_list db0 (make_local_hint_db g) in
+- super_search n [Stringmap.find "core" !searchtable] db argl g
++ super_search n [Hintdbmap.find "core" !searchtable] db argl g
+
+ let superauto n to_add argl =
+ tclTRY (tclCOMPLETE (search_superauto n to_add argl))
+diff -urNad coq-8.0pl3~/tactics/auto.mli coq-8.0pl3/tactics/auto.mli
+--- coq-8.0pl3~/tactics/auto.mli 2005-01-21 16:41:52.000000000 +0000
++++ coq-8.0pl3/tactics/auto.mli 2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (* * GNU Lesser General Public License Version 2.1 *)
+ (************************************************************************)
+
+-(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
++(*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*)
+
+ (*i*)
+ open Util
+@@ -56,12 +56,16 @@
+ val iter : (constr_label -> stored_data list -> unit) -> t -> unit
+ end
+
+-type frozen_hint_db_table = Hint_db.t Stringmap.t
++type frozen_hint_db_table
+
+-type hint_db_table = Hint_db.t Stringmap.t ref
++type hint_db_table
+
+ type hint_db_name = string
+
++val searchtable_map : hint_db_name -> Hint_db.t
++
++val current_db_names : unit -> hint_db_name list
++
+ val add_hints : locality_flag -> hint_db_name list -> hints -> unit
+
+ val print_searchtable : unit -> unit
+diff -urNad coq-8.0pl3~/tactics/eauto.ml4 coq-8.0pl3/tactics/eauto.ml4
+--- coq-8.0pl3~/tactics/eauto.ml4 2004-07-16 19:30:52.000000000 +0000
++++ coq-8.0pl3/tactics/eauto.ml4 2006-02-19 11:28:43.000000000 +0000
+@@ -8,7 +8,7 @@
+
+ (*i camlp4deps: "parsing/grammar.cma" i*)
+
+-(* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *)
++(* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *)
+
+ open Pp
+ open Util
+@@ -391,16 +391,16 @@
+ let db_list =
+ List.map
+ (fun x ->
+- try Stringmap.find x !searchtable
++ try searchtable_map x
+ with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+ ("core"::dbnames)
+ in
+ tclTRY (e_search_auto debug np db_list)
+
+ let full_eauto debug n gl =
+- let dbnames = stringmap_dom !searchtable in
++ let dbnames = current_db_names () in
+ let dbnames = list_subtract dbnames ["v62"] in
+- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
++ let db_list = List.map (fun x -> searchtable_map x) dbnames in
+ let local_db = make_local_hint_db gl in
+ tclTRY (e_search_auto debug n db_list) gl
+
Property changes on: trunk/packages/coq/trunk/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
___________________________________________________________________
Name: svn:executable
+ *
More information about the Pkg-ocaml-maint-commits
mailing list