Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

11 files changed, 176 insertions, 204 deletions

diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 24af3842..a8b7c0d6 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -6,16 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Names
 open Util
 open Tacexpr
 
-type ('constr,'tac) justification =
-  By_tactic of 'tac
-| Automated of 'constr list
-
 type 'it statement = 
     {st_label:name;
      st_it:'it}
@@ -42,8 +38,9 @@ type block_type =
   | B_elim of elim_type
 
 type ('it,'constr,'tac) cut =
-    {cut_stat: 'it statement;
-     cut_by: ('constr,'tac) justification}
+    {cut_stat: 'it;
+     cut_by: 'constr list option;
+     cut_using: 'tac option}
 
 type ('var,'constr) hyp = 
     Hvar of 'var 
@@ -51,14 +48,15 @@ type ('var,'constr) hyp =
 
 type ('constr,'tac) casee = 
     Real of 'constr 
-  | Virtual of ('constr,'constr,'tac) cut
+  | Virtual of ('constr statement,'constr,'tac) cut
 
 type ('hyp,'constr,'pat,'tac) bare_proof_instr =
   | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
   | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
   | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Pcut of ('constr or_thesis,'constr,'tac) cut
-  | Prew of side * ('constr,'constr,'tac) cut
+  | Pcut of ('constr or_thesis statement,'constr,'tac) cut
+  | Prew of side * ('constr statement,'constr,'tac) cut
+  | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
   | Passume of ('hyp,'constr) hyp list
   | Plet of ('hyp,'constr) hyp list
   | Pgiven of ('hyp,'constr) hyp list
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index 094c5625..8d8fb745 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Names
 open Term
@@ -67,11 +67,10 @@ type stack_info =
   | Focus_claim
 
 type pm_info =
-    { pm_last: Names.name (* anonymous if none *);
-      pm_hyps: Idset.t;
-      pm_partial_goal : constr ; (* partial goal construction *)
+    { pm_last: (Names.identifier * bool) option (* anonymous if none *);
+      pm_partial_goal : constr; (* partial goal construction *)
       pm_subgoals : (metavariable*constr) list;
-      pm_stack : stack_info list }
+      pm_stack : stack_info list}
 
 let pm_in,pm_out = Dyn.create "pm_info" 
 
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index 0dd1cb33..81fab168 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Names
 open Term
@@ -56,8 +56,7 @@ type stack_info =
   | Focus_claim
 
 type pm_info =
-    { pm_last: Names.name (* anonymous if none *);
-      pm_hyps: Idset.t;
+    { pm_last: (Names.identifier * bool) option (* anonymous if none *);
       pm_partial_goal : constr ; (* partial goal construction *)
       pm_subgoals : (metavariable*constr) list;
       pm_stack : stack_info list }
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 79f01ba1..132fa2b9 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 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: evar_refiner.ml 9583 2007-02-01 19:35:03Z notin $ *)
 
 open Util
 open Names
@@ -28,9 +28,12 @@ let w_refine ev rawc evd =
   let e_info = Evd.find (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
-    Pretyping.Default.understand_tcc (evars_of evd) env 
-      ~expected_type:e_info.evar_concl rawc in
-  evar_define ev typed_c (evars_reset_evd sigma evd)
+    try Pretyping.Default.understand_tcc (evars_of evd) env 
+      ~expected_type:e_info.evar_concl rawc 
+    with _ -> error ("The term is not well-typed in the environment of " ^
+			string_of_existential ev)
+  in
+    evar_define ev typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e40d1232..92225948 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
+(* $Id: logic.ml 9601 2007-02-06 21:37:59Z herbelin $ *)
 
 open Pp
 open Util
@@ -69,26 +69,10 @@ let with_check = Options.with_option check
 (* The Clear tactic: it scans the context for hypotheses to be removed
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
-let clear_hyps ids gl =
-  let env = Global.env() in
-  let (nhyps,cleared_ids) =
-    let fcheck cleared_ids (id,_,_ as d)  =
-      if !check && cleared_ids<>[] then
-	Idset.iter
-	  (fun id' ->
-            if List.mem id' cleared_ids then
-              error (string_of_id id'^
-		        " is used in hypothesis "^string_of_id id))
-	  (global_vars_set_of_decl env d) in
-      clear_hyps ids fcheck gl.evar_hyps in
-  let ncl = gl.evar_concl in
-    if !check && cleared_ids<>[] then
-      Idset.iter
-	(fun id' ->
-          if List.mem id' cleared_ids then
-            error (string_of_id id'^" is used in conclusion"))
-	(global_vars_set_drop_evar env ncl);
-    mk_goal nhyps ncl gl.evar_extra
+let clear_hyps sigma ids gl =
+  let evd = ref (Evd.create_evar_defs sigma) in
+  let ngl = Evarutil.clear_hyps_in_evi evd gl ids in
+    (ngl, evars_of !evd)
 
 (* The ClearBody tactic *)
 
@@ -216,7 +200,7 @@ let check_forward_dependencies id tail =
 
 let check_goal_dependency id cl =
   let env = Global.env() in
-    if Idset.mem id (global_vars_set_drop_evar env cl) then
+    if Idset.mem id (global_vars_set env cl) then
       error (string_of_id id^" is used in conclusion")
 
 let rename_hyp id1 id2 sign =
@@ -398,6 +382,19 @@ let convert_hyp sign sigma (id,b,bt as d) =
 	 error ("Incorrect change of the body of "^(string_of_id id));
        d)
 
+(* Normalizing evars in a goal. Called by tactic Local_constraints
+   (i.e. when the sigma of the proof tree changes). Detect if the
+   goal is unchanged *)
+let norm_goal sigma gl =
+  let red_fun = Evarutil.nf_evar sigma in
+  let ncl = red_fun gl.evar_concl in
+  let ngl =
+    { gl with 
+	evar_concl = ncl;
+	evar_hyps = map_named_val red_fun gl.evar_hyps } in
+    if Evd.eq_evar_info ngl gl then None else Some ngl
+
+
 
 (************************************************************************)
 (************************************************************************)
@@ -418,13 +415,13 @@ let prim_refiner r sigma goal =
 	       if occur_meta c1 then error_use_instantiate();
 	       let sg = mk_goal (push_named_context_val (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
 	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
 		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
 	
@@ -434,12 +431,12 @@ let prim_refiner r sigma goal =
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,None,c1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
            | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,Some c1,t1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
 	
@@ -449,7 +446,7 @@ let prim_refiner r sigma goal =
         if occur_meta t then error_use_instantiate();
         let sg1 = mk_goal sign (nf_betaiota t) in
         let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in
-        if b then [sg1;sg2] else [sg2;sg1]  
+        if b then ([sg1;sg2],sigma) else ([sg2;sg1], sigma)
 
     | FixRule (f,n,rest) ->
      	let rec check_ind env k cl = 
@@ -478,7 +475,7 @@ let prim_refiner r sigma goal =
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
-	mk_sign sign all
+	  (mk_sign sign all, sigma)
 	
     | Cofix (f,others) ->
      	let rec check_is_coind env cl = 
@@ -505,47 +502,48 @@ e types")
                   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
+	  (mk_sign sign all, sigma)
 
     | Refine c ->
         if not (list_distinct (collect_meta_variables c)) then
           raise (RefinerError (NonLinearProof c));
 	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
-	sgl
+	  (sgl, sigma)
 
     (* Conversion rules *)
     | Convert_concl (cl',_) ->
 	check_typability env sigma cl';
 	if (not !check) || is_conv_leq env sigma cl' cl then
           let sg = mk_goal sign cl' in
-          [sg]
+          ([sg], sigma)
 	else 
 	  error "convert-concl rule passed non-converting term"
 
     | Convert_hyp (id,copt,ty) ->
-	[mk_goal (convert_hyp sign sigma (id,copt,ty)) cl]
+	([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
 
     (* And now the structural rules *)
     | Thin ids -> 
-	[clear_hyps ids goal]
-
+	let (ngl, nsigma) = clear_hyps sigma ids goal in
+	  ([ngl], nsigma)
+	
     | ThinBody ids ->
 	let clear_aux env id =
           let env' = remove_hyp_body env sigma id in
-          if !check then recheck_typability (None,id) env' sigma cl;
-          env'
+            if !check then recheck_typability (None,id) env' sigma cl;
+            env'
 	in
 	let sign' = named_context_val (List.fold_left clear_aux env ids) in
      	let sg = mk_goal sign' cl in
-     	[sg]
+     	  ([sg], sigma)
 
     | Move (withdep, hfrom, hto) ->
   	let (left,right,declfrom,toleft) = 
 	  split_sign hfrom hto (named_context_of_val sign) in
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
-  	[mk_goal hyps' cl]
+  	  ([mk_goal hyps' cl], sigma)
 
     | Rename (id1,id2) ->
         if !check & id1 <> id2 &&
@@ -553,7 +551,12 @@ e types")
           error ((string_of_id id2)^" is already used");
         let sign' = rename_hyp id1 id2 sign in
         let cl' = replace_vars [id1,mkVar id2] cl in
-        [mk_goal sign' cl']
+          ([mk_goal sign' cl'], sigma)
+
+    | Change_evars ->
+        match norm_goal sigma goal with
+	    Some ngl -> ([ngl],sigma)
+          | None -> ([goal], sigma)
 
 (************************************************************************)
 (************************************************************************)
@@ -596,80 +599,83 @@ let proof_variable_index x =
 
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
-  match pft.ref with
-    | Some (Prim (Intro id), [spf]) ->
-	(match kind_of_term (strip_outer_cast cl) with
-	   | Prod (_,ty,_) ->
-	       let cty = subst_proof_vars vl ty in
-	       mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
-	   | LetIn (_,b,ty,_) ->
-	       let cb = subst_proof_vars vl b in
-	       let cty = subst_proof_vars vl ty in
-	       mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	   | _ -> error "incomplete proof!")
-	
-    | Some (Prim (Intro_replacing id),[spf]) ->
-	(match kind_of_term (strip_outer_cast cl) with
-	   | Prod (_,ty,_) ->
-	       let cty = subst_proof_vars vl ty in
-	       mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
-	   | LetIn (_,b,ty,_) ->
-	       let cb = subst_proof_vars vl b in
-	       let cty = subst_proof_vars vl ty in
-	       mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	   | _ -> error "incomplete proof!")
-
-    | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
-        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
-	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
-	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))	
-
-    | Some (Prim (Cofix (f,others)),spfl) ->
-	let all = Array.of_list ((f,cl)::others) 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))
-	  
-    | Some (Prim (Refine c),spfl) ->
-	let mvl = collect_meta_variables c in
-	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
-	let cc = subst_proof_vars vl c in 
-	plain_instance metamap cc
-
-    (* Structural and conversion rules do not produce any proof *)
-    | Some (Prim (Convert_concl (t,k)),[pf]) ->
-	if k = DEFAULTcast then subfun vl pf
-	else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
-    | Some (Prim (Convert_hyp _),[pf]) ->
-	subfun vl pf
-
-    | Some (Prim (Thin _),[pf]) ->
-     (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
-	subfun vl pf
-	
-    | Some (Prim (ThinBody _),[pf]) ->
-	subfun vl pf
-	
-    | Some (Prim (Move _),[pf]) ->
-	subfun vl pf
-
-    | Some (Prim (Rename (id1,id2)),[pf]) ->
-	subfun (rebind id1 id2 vl) pf
-
-    | Some _ -> anomaly "prim_extractor"
-
-    | None-> error "prim_extractor handed incomplete proof"
+    match pft.ref with
+      | Some (Prim (Intro id), [spf]) ->
+	  (match kind_of_term (strip_outer_cast cl) with
+	    | Prod (_,ty,_) ->
+		let cty = subst_proof_vars vl ty in
+		  mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
+	    | LetIn (_,b,ty,_) ->
+		let cb = subst_proof_vars vl b in
+		let cty = subst_proof_vars vl ty in
+		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
+	    | _ -> error "incomplete proof!")
+	    
+      | Some (Prim (Intro_replacing id),[spf]) ->
+	  (match kind_of_term (strip_outer_cast cl) with
+	    | Prod (_,ty,_) ->
+		let cty = subst_proof_vars vl ty in
+		  mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
+	    | LetIn (_,b,ty,_) ->
+		let cb = subst_proof_vars vl b in
+		let cty = subst_proof_vars vl ty in
+		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
+	    | _ -> error "incomplete proof!")
+
+      | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
+          let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+	    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
+	  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))	
+
+      | Some (Prim (Cofix (f,others)),spfl) ->
+	  let all = Array.of_list ((f,cl)::others) 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))
+	      
+      | Some (Prim (Refine c),spfl) ->
+	  let mvl = collect_meta_variables c in
+	  let metamap = List.combine mvl (List.map (subfun vl) spfl) in
+	  let cc = subst_proof_vars vl c in 
+	    plain_instance metamap cc
+
+      (* Structural and conversion rules do not produce any proof *)
+      | Some (Prim (Convert_concl (t,k)),[pf]) ->
+	  if k = DEFAULTcast then subfun vl pf
+	  else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
+      | Some (Prim (Convert_hyp _),[pf]) ->
+	  subfun vl pf
+
+      | Some (Prim (Thin _),[pf]) ->
+	  (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
+	  subfun vl pf
+	    
+      | Some (Prim (ThinBody _),[pf]) ->
+	  subfun vl pf
+	    
+      | Some (Prim (Move _),[pf]) ->
+	  subfun vl pf
+
+      | Some (Prim (Rename (id1,id2)),[pf]) ->
+	  subfun (rebind id1 id2 vl) pf
+
+      | Some (Prim Change_evars, [pf]) ->
+	  subfun vl pf
+
+      | Some _ -> anomaly "prim_extractor"
+
+      | None-> error "prim_extractor handed incomplete proof"
 	  
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ab65b1d5..2b6c6b4a 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: logic.mli 8107 2006-03-01 17:34:36Z herbelin $ i*)
+(*i $Id: logic.mli 9573 2007-01-31 20:18:18Z notin $ i*)
 
 (*i*)
 open Names
@@ -34,7 +34,7 @@ val with_check    : tactic -> tactic
 
 (* The primitive refiner. *)
 
-val prim_refiner : prim_rule -> evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
 type proof_variable
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index abe31624..6f8b0686 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 9244 2006-10-16 17:11:44Z barras $ *)
+(*i $Id: proof_type.ml 9573 2007-01-31 20:18:18Z notin $ *)
 
 (*i*)
 open Environ
@@ -39,6 +39,7 @@ type prim_rule =
   | ThinBody of identifier list
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
+  | Change_evars
 
 type proof_tree = {
   open_subgoals : int;
@@ -50,7 +51,6 @@ and rule =
   | Nested of compound_rule * proof_tree 
   | Decl_proof of bool
   | Daimon
-  | Change_evars
 
 and compound_rule=  
   | Tactic of tactic_expr * bool
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index d87c1298..26d9eb2e 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 9244 2006-10-16 17:11:44Z barras $ i*)
+(*i $Id: proof_type.mli 9573 2007-01-31 20:18:18Z notin $ i*)
 
 (*i*)
 open Environ
@@ -39,6 +39,7 @@ type prim_rule =
   | ThinBody of identifier list
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
+  | Change_evars
 
 (* The type [goal sigma] is the type of subgoal. It has the following form
 \begin{verbatim}
@@ -84,7 +85,6 @@ and rule =
   | Nested of compound_rule * proof_tree 
   | Decl_proof of bool
   | Daimon
-  | Change_evars
 
 and compound_rule= 
   (* the boolean of Tactic tells if the default tactic is used *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 70a0e3db..a1d7e011 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 9261 2006-10-23 10:01:40Z barras $ *)
+(* $Id: refiner.ml 9573 2007-01-31 20:18:18Z notin $ *)
 
 open Pp
 open Util
@@ -68,18 +68,6 @@ let descend n p =
     	else 
 	  error "Too few subproofs"
 
-(* Normalizing evars in a goal. Called by tactic Local_constraints
-   (i.e. when the sigma of the proof tree changes). Detect if the
-   goal is unchanged *)
-let norm_goal sigma gl =
-  let red_fun = Evarutil.nf_evar sigma in
-  let ncl = red_fun gl.evar_concl in
-  let ngl =
-    { gl with 
-	evar_concl = ncl;
-	evar_hyps = map_named_val red_fun gl.evar_hyps } in
-    if Evd.eq_evar_info ngl gl then None else Some ngl
-
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
    gives
@@ -192,11 +180,11 @@ let abstract_operation syntax semantics gls =
   let (sgl_sigma,validation) = semantics gls in
   let hidden_proof = validation (List.map leaf sgl_sigma.it) in
   (sgl_sigma,
-   fun spfl ->
-     assert (check_subproof_connection sgl_sigma.it spfl);
-     { open_subgoals = and_status (List.map pf_status spfl);
-       goal = gls.it;
-       ref = Some(Nested(syntax,hidden_proof),spfl)})
+  fun spfl ->
+    assert (check_subproof_connection sgl_sigma.it spfl);
+    { open_subgoals = and_status (List.map pf_status spfl);
+      goal = gls.it;
+      ref = Some(Nested(syntax,hidden_proof),spfl)})
 
 let abstract_tactic_expr ?(dflt=false) te tacfun gls =
   abstract_operation (Tactic(te,dflt)) tacfun gls	
@@ -210,14 +198,14 @@ let abstract_extended_tactic ?(dflt=false) s args =
 let refiner = function
   | Prim pr as r ->
       let prim_fun = prim_refiner pr in
-      (fun goal_sigma ->
-         let sgl = prim_fun goal_sigma.sigma goal_sigma.it in 
-	 ({it=sgl; sigma = goal_sigma.sigma},
-          (fun spfl ->
-	     assert (check_subproof_connection sgl spfl);
-             { open_subgoals = and_status (List.map pf_status spfl);
-               goal = goal_sigma.it;
-               ref = Some(r,spfl) })))
+	(fun goal_sigma ->
+          let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in 
+	    ({it=sgl; sigma = sigma'},
+            (fun spfl ->
+	      assert (check_subproof_connection sgl spfl);
+              { open_subgoals = and_status (List.map pf_status spfl);
+		goal = goal_sigma.it;
+		ref = Some(r,spfl) })))
 
 
   | Nested (_,_) | Decl_proof _ -> 
@@ -234,44 +222,23 @@ let refiner = function
              goal = gls.it;
              ref = Some(Daimon,[])})
 
-   (* [Local_constraints lc] makes the local constraints be [lc] and
-      normalizes evars *)
-
-  | Change_evars as r ->
-      (fun goal_sigma ->
-         let gl = goal_sigma.it in
-         (match norm_goal goal_sigma.sigma gl with
-             Some ngl ->
-	       ({it=[ngl];sigma=goal_sigma.sigma},
-                (fun spfl -> 
-	          assert (check_subproof_connection [ngl] spfl);
-                  { open_subgoals = (List.hd spfl).open_subgoals;
-                    goal = gl;
-                    ref = Some(r,spfl) }))
-           (* if the evar change does not affect the goal, leave the
-              proof tree unchanged *)
-           | None -> ({it=[gl];sigma=goal_sigma.sigma},
-                      (fun spfl ->
-                        assert (List.length spfl = 1);
-                        List.hd spfl))))
-
-
-let local_Constraints gl = refiner Change_evars gl
+
+let local_Constraints gl = refiner (Prim Change_evars) gl
 
 let norm_evar_tac = local_Constraints
 
 let norm_evar_proof sigma pf =
   let nf_subgoal i sgl =
     let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
-    v (List.map leaf gll.it) in
-  frontier_mapi nf_subgoal pf
+      v (List.map leaf gll.it) in
+    frontier_mapi nf_subgoal pf
 
 (* [extract_open_proof : proof_tree -> constr * (int * constr) list]
-  takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
-  where pfterm is the constr corresponding to the proof
-  and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
-  where the mi are metavariables numbers, and ci are their types.
-  Their proof should be completed in order to complete the initial proof *)
+   takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
+   where pfterm is the constr corresponding to the proof
+   and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
+   where the mi are metavariables numbers, and ci are their types.
+   Their proof should be completed in order to complete the initial proof *)
 
 let extract_open_proof sigma pf =
   let next_meta = 
@@ -291,8 +258,6 @@ let extract_open_proof sigma pf =
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
  
-    | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
-
     | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
 	  
     | {ref=(None|Some(Daimon,[]));goal=goal} ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 0fe21552..0bcc7d16 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacexpr.ml 9267 2006-10-24 12:55:46Z herbelin $ i*)
+(*i $Id: tacexpr.ml 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 open Names
 open Topconstr
@@ -121,6 +121,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacAssumption
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
+  | TacVmCastNoCheck of 'constr
   | TacApply of 'constr with_bindings
   | TacElim of 'constr with_bindings * 'constr with_bindings option
   | TacElimType of 'constr
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b426f75d..baf8c859 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 7682 2005-12-21 15:06:11Z herbelin $ *)
+(* $Id: tacmach.ml 9511 2007-01-22 08:27:31Z herbelin $ *)
 
 open Util
 open Names
@@ -102,6 +102,7 @@ let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_type_of                   = pf_reduce type_of
+let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x                   = pf_reduce is_conv
 let pf_conv_x_leq               = pf_reduce is_conv_leq
@@ -109,7 +110,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
+let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
 let pf_check_type gls c1 c2 = 
   ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))