Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg

8 files changed, 85 insertions, 67 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index 86251254..dc0dec0e 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
+(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *)
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
@@ -199,7 +199,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let ind=destInd h in 
   let types=Inductiveops.arities_of_constructors env ind in
   let lp=Array.length types in
-  let ci=(snd cstr)-1 in
+  let ci=pred (snd cstr) in
   let branch i=
     let ti=Term.prod_appvect types.(i) argv in
     let rc=fst (Sign.decompose_prod_assum ti) in
@@ -247,7 +247,7 @@ let rec proof_tac p gls =
 	and tx2=constr_of_term p2.p_rhs in
 	let typf = pf_type_of gls tf1 in
 	let typx = pf_type_of gls tx1 in
-	let typfx = prod_applist typf [tx1] in
+	let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in
 	let id = pf_get_new_id (id_of_string "f") gls in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 97fa4d77..ffc4b9c4 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cctac.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *)
 
 open Term 
 open Proof_type
 
+val proof_tac: Ccproof.proof -> Proof_type.tactic
+
 val cc_tactic : int -> constr list -> tactic
 
 val cc_fail : tactic
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e31b701c..825b3554 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*)
+(*i $Id: extract_env.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
 
 open Term
 open Declarations
@@ -92,7 +92,8 @@ module Visit : VISIT = struct
   let needed_kn kn = KNset.mem kn v.kn
   let needed_con c = Cset.mem c v.con
   let needed_mp mp = MPset.mem mp v.mp
-  let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
+  let add_mp mp = 
+    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
   let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
   let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
   let add_ref = function 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6fd4a3cc..6982ffc6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*)
+(*i $Id: extraction.ml 10195 2007-10-08 01:47:55Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -31,10 +31,6 @@ open Mlutil
 
 exception I of inductive_info
 
-(* A set of all inductive currently being computed, 
-   to avoid loops in [extract_inductive] *)
-let internal_call = ref KNset.empty
-
 (* A set of all fixpoint functions currently being extracted *)
 let current_fixpoints = ref ([] : constant list)
 
@@ -303,13 +299,15 @@ and extract_type_scheme env db c p =
 (*S Extraction of an inductive type. *)
 
 and extract_ind env kn = (* kn is supposed to be in long form *)
-  try 
-    if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *)
-    else if visible_kn kn then lookup_ind kn (* Standard situation. *)
-    else raise Not_found (* Never trust the table for a internal kn. *)
+  let mib = Environ.lookup_mind kn env in
+  try
+    (* For a same kn, we can get various bodies due to module substitutions.
+       We hence check that the mib has not changed from recording 
+       time to retrieving time. Ideally we should also check the env. *)
+    let (mib0,ml_ind) = lookup_ind kn in 
+    if not (mib = mib0) then raise Not_found; 
+    ml_ind
   with Not_found -> 
-    internal_call := KNset.add kn !internal_call;
-    let mib = Environ.lookup_mind kn env in 
     (* First, if this inductive is aliased via a Module, *)
     (* we process the original inductive. *)
     option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
@@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ip_types = t }) 
 	mib.mind_packets 
     in 
-    add_ind kn 
+    add_ind kn mib
       {ind_info = Standard; 
        ind_nparams = npar; 
        ind_packets = packets; 
@@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ind_packets = packets; 
 	     ind_equiv = mib.mind_equiv}
     in
-    add_ind kn i; 
-    internal_call := KNset.remove kn !internal_call;
+    add_ind kn mib i; 
     i
 
 (*s [extract_type_cons] extracts the type of an inductive 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index b1a3cb31..6d39faee 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: table.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
 
 open Names
 open Term
@@ -60,7 +60,6 @@ let at_toplevel mp =
 let visible_kn kn = at_toplevel (base_mp (modpath kn))
 let visible_con kn = at_toplevel (base_mp (con_modpath kn))
 
-
 (*S The main tables: constants, inductives, records, ... *)
 
 (*s Constants tables. *) 
@@ -77,9 +76,9 @@ let lookup_type kn = Cmap.find kn !types
 
 (*s Inductives table. *)
 
-let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
 let init_inductives () = inductives := KNmap.empty
-let add_ind kn m = inductives := KNmap.add kn m !inductives
+let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
 let lookup_ind kn = KNmap.find kn !inductives
 
 (*s Recursors table. *)
@@ -124,11 +123,24 @@ let reset_tables () =
 
 let id_of_global = function 
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
-  | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
-  | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
+  | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+  | ConstructRef ((kn,i),j) -> 
+      (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
-let pr_global r = pr_id (id_of_global r)
+let pr_global r = 
+ try Printer.pr_global r 
+ with _ -> pr_id (id_of_global r)
+
+(* idem, but with qualification, and only for constants. *)
+
+let pr_long_global r = 
+  try Printer.pr_global r 
+  with _ -> match r with
+    | ConstRef kn -> 
+	let mp,_,l = repr_con kn in 
+	str ((string_of_mp mp)^"."^(string_of_label l))
+    | _ -> assert false
 
 (*S Warning and Error messages. *)
 
@@ -150,13 +162,13 @@ let warning_log_ax r =
 		  spc () ++ str "may lead to incorrect or non-terminating ML terms.")
 
 let check_inside_module () = 
-  try 
-    ignore (Lib.what_is_opened ()); 
-    Options.if_verbose warning
-      ("Extraction inside an opened module is experimental.\n"^
-       "In case of problem, close it first.\n"); 
-    Pp.flush_all ()
-  with Not_found -> ()
+  if Lib.is_modtype () then 
+    err (str "You can't do that within a Module Type." ++ fnl () ++
+	 str "Close it and try again.") 
+  else if Lib.is_module () then 
+    msg_warning
+      (str "Extraction inside an opened module is experimental.\n" ++
+       str "In case of problem, close it first.\n")
 
 let check_inside_section () = 
   if Lib.sections_are_opened () then 
@@ -164,10 +176,10 @@ let check_inside_section () =
 	 str "Close it and try again.")
 
 let error_constant r = 
-  err (Printer.pr_global r ++ str " is not a constant.") 
+  err (pr_global r ++ str " is not a constant.") 
 
 let error_inductive r = 
-  err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+  err (pr_global r ++ spc () ++ str "is not an inductive type.")
 
 let error_nb_cons () = 
   err (str "Not the right number of constructors.")
@@ -187,23 +199,23 @@ let error_scheme () =
   err (str "No Scheme modular extraction available yet.")
 
 let error_not_visible r = 
-  err (Printer.pr_global r ++ str " is not directly visible.\n" ++
+  err (pr_global r ++ str " is not directly visible.\n" ++
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
-let error_unqualified_name s1 s2 = 
-  err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
-	    "in ML from another name sharing the same basename.\n"  ^
-	    "Please do some renaming.\n"))
-
 let error_MPfile_as_mod d = 
   err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
 	    "Extraction cannot currently deal with this situation.\n"))
 
 let error_record r = 
-  err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+  err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
        str "To help extraction, please use an explicit name.") 
 
+let check_loaded_modfile mp = match base_mp mp with 
+  | MPfile dp -> if not (Library.library_is_loaded dp) then 
+      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+  | _ -> ()
+
 (*S The Extraction auxiliary commands *)
 
 (*s Extraction AutoInline *)
@@ -310,7 +322,7 @@ let _ = declare_summary "Extraction Lang"
 	  { freeze_function = (fun () -> !lang_ref);
 	    unfreeze_function = ((:=) lang_ref);
 	    init_function = (fun () -> lang_ref := Ocaml);
-	    survive_module = false;
+	    survive_module = true;
 	    survive_section = true }  
 	  
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
@@ -342,28 +354,21 @@ let (inline_extraction,_) =
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        export_function = (fun x -> Some x); 
        classify_function = (fun (_,o) -> Substitute o); 
-       (*CSC: The following substitution may istantiate a realized parameter.
-         The right solution would be to make the substitution erase the
-         realizer from the table. However, this is not allowed by Coq.
-         In this particular case, though, keeping the realizer is place seems
-         to be harmless since the current code looks for a realizer only
-         when the constant is a parameter. However, if this behaviour changes
-         subtle bugs can happear in the future. *)
        subst_function =
-        (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))}
+        (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
+    }
 
 let _ = declare_summary "Extraction Inline"
 	  { freeze_function = (fun () -> !inline_table);
 	    unfreeze_function = ((:=) inline_table);
 	    init_function = (fun () -> inline_table := empty_inline_table);
-	    survive_module = false;
+	    survive_module = true;
 	    survive_section = true }
 
 (* Grammar entries. *)
 
 let extraction_inline b l =
   check_inside_section (); 
-  check_inside_module ();
   let refs = List.map Nametab.global l in 
   List.iter 
     (fun r -> match r with 
@@ -380,11 +385,11 @@ let print_extraction_inline () =
     (str "Extraction Inline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
+	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
@@ -423,20 +428,23 @@ let (in_customs,_) =
     {(default_object "ML extractions") with 
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       export_function = (fun x -> Some x)}
+       export_function = (fun x -> Some x); 
+       classify_function = (fun (_,o) -> Substitute o); 
+       subst_function =
+        (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
+    }
 
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !customs);
 	    unfreeze_function = ((:=) customs);
 	    init_function = (fun () -> customs := Refmap.empty);
-	    survive_module = false;
+	    survive_module = true;
 	    survive_section = true }
 
 (* Grammar entries. *)
 
 let extract_constant_inline inline r ids s =
   check_inside_section ();
-  check_inside_module ();
   let g = Nametab.global r in 
   match g with 
     | ConstRef kn -> 
@@ -455,7 +463,6 @@ let extract_constant_inline inline r ids s =
 
 let extract_inductive r (s,l) =
   check_inside_section ();
-  check_inside_module ();
   let g = Nametab.global r in 
   match g with
     | IndRef ((kn,i) as ip) ->
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 66662138..c9a4e8da 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*)
+(*i $Id: table.mli 10209 2007-10-09 21:49:37Z letouzey $ i*)
 
 open Names
 open Libnames
 open Miniml
+open Declarations
 
 val id_of_global : global_reference -> identifier
 
@@ -27,11 +28,11 @@ val error_unknown_module : qualid -> 'a
 val error_toplevel : unit -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
-val error_unqualified_name : string -> string -> 'a 
 val error_MPfile_as_mod : dir_path -> 'a
 val error_record : global_reference -> 'a 
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
+val check_loaded_modfile : module_path -> unit
 
 (*s utilities concerning [module_path]. *)
 
@@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl
 val add_type : constant -> ml_schema -> unit
 val lookup_type : constant -> ml_schema
 
-val add_ind : kernel_name -> ml_ind -> unit
-val lookup_ind : kernel_name -> ml_ind
+val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
 
 val add_recursors : Environ.env -> kernel_name -> unit
 val is_recursor : global_reference -> bool 
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index b55c5443..d8bb9eae 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -152,8 +152,15 @@ Ltac ParseRingComponents lemma :=
 
 (* ring tactics *)
 
+Ltac relation_carrier req :=
+  let ty := type of req in
+  match eval hnf in ty with
+   ?R -> _ => R
+  | _ => fail 1000 "Equality has no relation type"
+  end.
+
 Ltac FV_hypo_tac mkFV req lH :=
-  let R := match type of req with ?R -> _ => R end in
+  let R := relation_carrier req in
   let FV_hypo_l_tac h :=
     match h with @mkhypo (req ?pe _) _ => mkFV pe end in
   let FV_hypo_r_tac h :=
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index f963fc9c..134ba1a8 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*)
+(*i $Id: newring.ml4 10047 2007-07-24 17:55:18Z barras $ i*)
 
 open Pp
 open Util
@@ -465,7 +465,8 @@ let op_smorph r add mul req m1 m2 =
 
 let default_ring_equality (r,add,mul,opp,req) =
   let is_setoid = function
-      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
+      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} ->
+        eq_constr req rel (* Qu: use conversion ? *)
     | _ -> false in
   match default_relation_for_carrier ~filter:is_setoid r with
       Leibniz _ ->
@@ -625,6 +626,7 @@ let interp_sign env sign =
        (* Same remark on ill-typed terms ... *)
 
 let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
+  check_required_library (cdir@["Ring_base"]);
   let env = Global.env() in
   let sigma = Evd.empty in
   let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
@@ -986,6 +988,7 @@ let default_field_equality r inv req =
         inv_m.lem
 
 let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
+  check_required_library (cdir@["Field_tac"]);
   let env = Global.env() in
   let sigma = Evd.empty in
   let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =