Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

8 files changed, 51 insertions, 35 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f5204be5..769a9572 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenvtac.ml 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: clenvtac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Pp
 open Util
@@ -25,7 +25,6 @@ open Logic
 open Reduction
 open Reductionops
 open Tacmach
-open Evar_refiner
 open Rawterm
 open Pattern
 open Tacexpr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d19d81e0..f4613f8d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Util
 open Names
@@ -15,6 +15,7 @@ open Evd
 open Sign
 open Proof_trees
 open Refiner
+open Pretyping
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -22,21 +23,21 @@ open Refiner
 
 (* w_tactic pour instantiate *) 
 
-let w_refine evk rawc evd =
+let w_refine evk (ltac_vars,rawc) evd =
   if Evd.is_defined (evars_of evd) evk then 
     error "Instantiate called on already-defined evar";
   let e_info = Evd.find (evars_of evd) evk in
   let env = Evd.evar_env e_info in
-  let sigma,typed_c =
-    try Pretyping.Default.understand_tcc ~resolve_classes:false
-      (evars_of evd) env ~expected_type:e_info.evar_concl rawc
+  let evd',typed_c =
+    try Pretyping.Default.understand_ltac 
+      (evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
       user_err_loc 
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-    evar_define evk typed_c (evars_reset_evd sigma evd)
+    evar_define evk typed_c (evars_reset_evd (evars_of evd') evd)
 
 (* vernac command Existential *)
 
@@ -55,5 +56,5 @@ let instantiate_pf_com n com pfts =
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_goal_evar_defs sigma in
-  let evd' = w_refine evk rawc evd in
+  let evd' = w_refine evk (([],[]),rawc) evd in
     change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index baa6b19a..a42b11a4 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_refiner.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: evar_refiner.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -14,11 +14,14 @@ open Term
 open Environ
 open Evd
 open Refiner
+open Pretyping
+open Rawterm
 (*i*)
 
 (* Refinement of existential variables. *)
 
-val w_refine : evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
+val w_refine : evar -> (var_map * unbound_ltac_var_map) * rawconstr -> 
+  evar_defs -> evar_defs
 
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3e758eb6..caf6f56b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -517,7 +517,7 @@ let prim_refiner r sigma goal =
         let sg2 = mk_goal sign cl in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
-    | FixRule (f,n,rest) ->
+    | FixRule (f,n,rest,j) ->
      	let rec check_ind env k cl = 
           match kind_of_term (strip_outer_cast cl) with 
             | Prod (na,c1,b) -> 
@@ -531,7 +531,8 @@ let prim_refiner r sigma goal =
             | _ -> error "Not enough products."
 	in
 	let (sp,_) = check_ind env n cl in
-	let all = (f,n,cl)::rest in
+	let firsts,lasts = list_chop j rest in
+	let all = firsts@(f,n,cl)::lasts in
      	let rec mk_sign sign = function 
 	  | (f,n,ar)::oth ->
 	      let (sp',_)  = check_ind env n ar in 
@@ -539,14 +540,15 @@ let prim_refiner r sigma goal =
 		error ("Fixpoints should be on the same " ^ 
 		       "mutual inductive declaration.");
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error "Name already used in the environment";
+		error
+		  ("Name "^string_of_id f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
 	  (mk_sign sign all, sigma)
 	
-    | Cofix (f,others) ->
+    | Cofix (f,others,j) ->
      	let rec check_is_coind env cl = 
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
@@ -558,7 +560,8 @@ let prim_refiner r sigma goal =
 		  error ("All methods must construct elements " ^
 			  "in coinductive types.")
 	in
-	let all = (f,cl)::others in
+	let firsts,lasts = list_chop j others in
+	let all = firsts@(f,cl)::lasts in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
         let rec mk_sign sign = function 
           | (f,ar)::oth ->
@@ -687,24 +690,26 @@ let prim_extractor subfun vl pft =
 	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
                     subfun (add_proof_var id vl) spf2)
 
-      | Some (Prim (FixRule (f,n,others)),spfl) ->
-	  let all = Array.of_list ((f,n,cl)::others) in
+      | Some (Prim (FixRule (f,n,others,j)),spfl) ->
+	  let firsts,lasts = list_chop j others in
+	  let all = Array.of_list (firsts@(f,n,cl)::lasts) in
 	  let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
 	  let names = Array.map (fun (f,_,_) -> Name f) all in
 	  let vn = Array.map (fun (_,n,_) -> n-1) all in
 	  let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
             (add_proof_var f vl) others in
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkFix ((vn,0),(names,lcty,lfix))	
+	    mkFix ((vn,j),(names,lcty,lfix))	
 
-      | Some (Prim (Cofix (f,others)),spfl) ->
-	  let all = Array.of_list ((f,cl)::others) in
+      | Some (Prim (Cofix (f,others,j)),spfl) ->
+	  let firsts,lasts = list_chop j others in
+	  let all = Array.of_list (firsts@(f,cl)::lasts) in
 	  let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
 	  let names  = Array.map (fun (f,_) -> Name f) all in
 	  let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
             (add_proof_var f vl) others in 
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkCoFix (0,(names,lcty,lfix))
+	    mkCoFix (j,(names,lcty,lfix))
 	      
       | Some (Prim (Refine c),spfl) ->
 	  let mvl = collect_meta_variables c in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 1e673853..150fb89f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(*i $Id: proof_type.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
 
 (*i*)
 open Environ
@@ -29,8 +29,8 @@ open Pattern
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list
-  | Cofix of identifier * (identifier * constr) list
+  | FixRule of identifier * int * (identifier * int * constr) list * int
+  | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
   | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 21cd8b28..c80e126f 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: proof_type.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
 
 (*i*)
 open Environ
@@ -29,8 +29,8 @@ open Pattern
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list
-  | Cofix of identifier * (identifier * constr) list
+  | FixRule of identifier * int * (identifier * int * constr) list * int
+  | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
   | Convert_concl of types * cast_kind 
   | Convert_hyp of named_declaration
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6c4f7b5e..b740baa8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tacmach.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -211,11 +211,15 @@ let rec rename_hyp_no_check l gl = match l with
       tclTHEN (refiner (Prim (Rename (id1,id2)))) 
 	(rename_hyp_no_check l) gl
 
-let mutual_fix f n others gl = 
-  with_check (refiner (Prim (FixRule (f,n,others)))) gl
+let mutual_fix_with_index f n others j gl =
+  with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
 
-let mutual_cofix f others gl = 
-  with_check (refiner (Prim (Cofix (f,others)))) gl
+let mutual_fix f n others = mutual_fix_with_index f n others 0
+
+let mutual_cofix_with_index f others j gl =
+  with_check (refiner (Prim (Cofix (f,others,j)))) gl
+
+let mutual_cofix f others = mutual_cofix_with_index f others 0
     
 (* Versions with consistency checks *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cdcb8bfd..37acf850 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacmach.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: tacmach.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -137,6 +137,10 @@ val order_hyps : identifier list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val mutual_fix_with_index :
+  identifier -> int -> (identifier * int * constr) list -> int -> tactic
+val mutual_cofix_with_index : 
+  identifier -> (identifier * constr) list -> int -> tactic
 
 (*s The most primitive tactics with consistency and type checking *)