diff options
Diffstat (limited to 'debian')
| -rw-r--r-- | debian/changelog | 7 | ||||
| -rw-r--r-- | debian/patches/00list | 1 | ||||
| -rwxr-xr-x | debian/patches/coq-8.0pl3-ocaml-3.09.dpatch | 507 |
3 files changed, 515 insertions, 0 deletions
diff --git a/debian/changelog b/debian/changelog index 604ef988..80dde408 100644 --- a/debian/changelog +++ b/debian/changelog @@ -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@debian.org> Sun, 19 Feb 2006 11:33:21 +0000 + coq (8.0pl3-1) unstable; urgency=low * New upstream release. diff --git a/debian/patches/00list b/debian/patches/00list index e69de29b..3804c9ad 100644 --- a/debian/patches/00list +++ b/debian/patches/00list @@ -0,0 +1 @@ +coq-8.0pl3-ocaml-3.09 diff --git a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch new file mode 100755 index 00000000..90b4d583 --- /dev/null +++ b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch @@ -0,0 +1,507 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram <smimram@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 + +@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 + |