Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

12 files changed, 367 insertions, 209 deletions

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 8ace0a08..f341580e 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -20,16 +20,23 @@ open Rawterm
 open Term
 open Pp
 
+(* INTERN *)
+
 let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
 
-let intern_justification globs = function
-    Automated l -> Automated (List.map (intern_constr globs) l)
-  | By_tactic tac -> By_tactic (intern_tactic globs tac) 
+let intern_justification_items globs = 
+  option_map (List.map (intern_constr globs))
+
+let intern_justification_method globs = 
+  option_map (intern_tactic globs)
 
 let intern_statement intern_it globs st =
   {st_label=st.st_label;
    st_it=intern_it globs st.st_it}
     
+let intern_no_bind intern_it globs x =
+  globs,intern_it globs x
+
 let intern_constr_or_thesis globs = function
     Thesis n -> Thesis n
   | This c -> This (intern_constr globs c)
@@ -53,12 +60,15 @@ let intern_hyps iconstr globs hyps =
   snd (list_fold_map (intern_hyp iconstr) globs hyps)
 
 let intern_cut intern_it globs cut=
- {cut_stat=intern_statement intern_it globs cut.cut_stat;
-  cut_by=intern_justification globs cut.cut_by}
+  let nglobs,nstat=intern_it globs cut.cut_stat in
+    {cut_stat=nstat;
+     cut_by=intern_justification_items nglobs cut.cut_by;
+     cut_using=intern_justification_method nglobs cut.cut_using}
 
 let intern_casee globs = function 
     Real c -> Real (intern_constr globs c)
-  | Virtual cut -> Virtual (intern_cut intern_constr globs cut) 
+  | Virtual cut -> Virtual 
+      (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut) 
 
 let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
@@ -66,6 +76,10 @@ let intern_hyp_list args globs =
     (loc,(id,option_map (intern_constr globs) opttyp)) in
   list_fold_map intern_one globs args 
 
+let intern_suffices_clause globs (hyps,c) = 
+  let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
+    nglobs,(nhyps,intern_constr_or_thesis nglobs c) 
+
 let intern_fundecl args body globs= 
   let nglobs,nargs = intern_hyp_list args globs in
     nargs,intern_constr nglobs body
@@ -89,8 +103,14 @@ let rec intern_bare_proof_instr globs = function
     Pthus i -> Pthus (intern_bare_proof_instr globs i)
   | Pthen i -> Pthen (intern_bare_proof_instr globs i)
   | Phence i -> Phence (intern_bare_proof_instr globs i)
-  | Pcut c -> Pcut (intern_cut intern_constr_or_thesis globs c) 
-  | Prew (s,c) -> Prew (s,intern_cut intern_constr globs c) 
+  | Pcut c -> Pcut 
+      (intern_cut 
+	 (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c)
+  | Psuffices c -> 
+      Psuffices (intern_cut intern_suffices_clause globs c)
+  | Prew (s,c) -> Prew 
+      (s,intern_cut 
+	 (intern_no_bind  (intern_statement intern_constr)) globs c) 
   | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
   | Pcase (params,pat,hyps) -> 
       let nglobs,nparams = intern_hyp_list params globs in
@@ -118,16 +138,16 @@ let rec intern_proof_instr globs instr=
   {emph = instr.emph;
    instr = intern_bare_proof_instr globs instr.instr}
 
-let interp_justification env sigma  = function
-    Automated l -> 
-      Automated (List.map (fun c ->understand env sigma (fst c)) l)
-  | By_tactic tac -> By_tactic tac 
+(* INTERP *)
 
-let interp_constr check_sort env sigma c = 
+let interp_justification_items sigma env =
+    option_map (List.map (fun c ->understand sigma env (fst c)))
+
+let interp_constr check_sort sigma env c = 
   if check_sort then 
-    understand_type env sigma (fst c) 
+    understand_type sigma env (fst c) 
   else 
-    understand env sigma (fst c)
+    understand sigma env (fst c)
 
 let special_whd env =
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
@@ -148,21 +168,21 @@ let decompose_eq env id =
 let get_eq_typ info env =
   let last_id = 	    
     match info.pm_last with
-	Anonymous -> error "no previous equality"
-      | Name id -> id in
+	None -> error "no previous equality"
+      | Some (id,_) -> id in
   let typ = decompose_eq env last_id in  
     typ
 
-let interp_constr_in_type typ env sigma c =
-  understand env sigma (fst c) ~expected_type:typ
+let interp_constr_in_type typ sigma env c =
+  understand sigma env (fst c) ~expected_type:typ
 
-let interp_statement interp_it env sigma st =
+let interp_statement interp_it sigma env st =
   {st_label=st.st_label;
-   st_it=interp_it env sigma st.st_it}
+   st_it=interp_it sigma env st.st_it}
 	
-let interp_constr_or_thesis check_sort env sigma = function
+let interp_constr_or_thesis check_sort sigma env = function
     Thesis n -> Thesis n
-  | This c -> This (interp_constr check_sort env sigma c)
+  | This c -> This (interp_constr check_sort sigma env c)
 
 let type_tester_var body typ = 
   raw_app(dummy_loc,
@@ -178,11 +198,13 @@ let abstract_one_hyp inject h raw =
     | Hprop st -> 
 	RProd (dummy_loc,st.st_label,inject st.st_it, raw)
 
-let rawconstr_of_hyps inject hyps = 
-  List.fold_right (abstract_one_hyp inject) hyps (RSort (dummy_loc,RProp Null))
+let rawconstr_of_hyps inject hyps head = 
+  List.fold_right (abstract_one_hyp inject) hyps head
+
+let raw_prop = RSort (dummy_loc,RProp Null)
   
 let rec match_hyps blend names constr = function 
-    [] -> []
+    [] -> [],substl names constr
   | hyp::q -> 
       let (name,typ,body)=destProd constr in
       let st= {st_label=name;st_it=substl names typ} in
@@ -193,13 +215,14 @@ let rec match_hyps blend names constr = function
       let qhyp = match hyp with
 	  Hprop st' -> Hprop (blend st st')
 	| Hvar _ -> Hvar st in
-	qhyp::(match_hyps blend qnames body q)
+      let rhyps,head = match_hyps blend qnames body q in
+	qhyp::rhyps,head
 
-let interp_hyps_gen inject blend env sigma hyps = 
-  let constr=understand env sigma (rawconstr_of_hyps inject hyps) in
+let interp_hyps_gen inject blend sigma env hyps head = 
+  let constr=understand sigma env (rawconstr_of_hyps inject hyps head) in
     match_hyps blend [] constr hyps
 
-let interp_hyps = interp_hyps_gen fst (fun x _ -> x)
+let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps raw_prop)
 
 let dummy_prefix= id_of_string "__"
 
@@ -301,7 +324,7 @@ let rec match_aliases names constr = function
 
 let detype_ground c = Detyping.detype false [] [] c
 
-let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
+let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
     match info.pm_stack with
 	Per(et,pi,_,_)::_ -> et,pi
@@ -338,7 +361,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	       str " does not occur in pattern.");
 	Rawterm.RSort(dummy_loc,RProp Null)
     | This (c,_) -> c in
-  let term1 = rawconstr_of_hyps inject hyps in
+  let term1 = rawconstr_of_hyps inject hyps raw_prop in
   let loc_ids,npatt =
     let rids=ref ([],pat_vars) in
     let npatt= deanonymize rids patt in 
@@ -355,11 +378,11 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
   let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
   let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
-  let blend  st st' =
+  let blend st st' =
     match st'.st_it with 
 	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} 
       | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
-  let thyps = match_hyps blend nam2 (Termops.pop rest1) hyps in
+  let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in
     tparams,{pat_vars=tpatvars;
 	     pat_aliases=taliases;
 	     pat_constr=pat_pat;
@@ -367,13 +390,35 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	     pat_pat=patt;
 	     pat_expr=pat},thyps
 
-let interp_cut interp_it env sigma cut=
- {cut_stat=interp_statement interp_it env sigma cut.cut_stat;
-  cut_by=interp_justification env sigma cut.cut_by}
-
-let interp_casee env sigma = function 
-    Real c -> Real (understand env sigma (fst c))
-  | Virtual cut -> Virtual (interp_cut (interp_constr true) env sigma cut) 
+let interp_cut interp_it sigma env cut=
+  let nenv,nstat = interp_it sigma env cut.cut_stat in
+    {cut with 
+       cut_stat=nstat;
+       cut_by=interp_justification_items sigma nenv cut.cut_by}
+
+let interp_no_bind interp_it sigma env x =
+  env,interp_it sigma env x
+
+let interp_suffices_clause sigma env (hyps,cot)=
+  let (locvars,_) as res =
+    match cot with
+	This (c,_) -> 
+	  let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in
+	  nhyps,This nc
+      | Thesis (Plain| Sub _) as th  -> interp_hyps sigma env hyps,th
+      | Thesis (For n) -> error "\"thesis for\" is not applicable here" in
+  let push_one hyp env0 =
+    match hyp with
+	(Hprop st | Hvar st) ->
+	  match st.st_label with
+	      Name id -> Environ.push_named (id,None,st.st_it) env0
+	    | _ -> env in
+  let nenv = List.fold_right push_one locvars env in 
+    nenv,res 
+	  
+let interp_casee sigma env = function 
+    Real c -> Real (understand sigma env (fst c))
+  | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut) 
 
 let abstract_one_arg = function
     (loc,(id,None)) ->
@@ -387,21 +432,28 @@ let abstract_one_arg = function
 let rawconstr_of_fun args body = 
   List.fold_right abstract_one_arg args (fst body)
 
-let interp_fun env sigma args body = 
-  let constr=understand env sigma (rawconstr_of_fun args body) in
+let interp_fun sigma env args body = 
+  let constr=understand sigma env (rawconstr_of_fun args body) in
     match_args destLambda [] constr args
 
-let rec interp_bare_proof_instr info sigma env = function
+let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function
     Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
   | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
   | Phence i -> Phence (interp_bare_proof_instr info sigma env i)
-  | Pcut c -> Pcut (interp_cut (interp_constr_or_thesis true) sigma env c) 
+  | Pcut c -> Pcut (interp_cut 
+		      (interp_no_bind (interp_statement 
+					 (interp_constr_or_thesis true))) 
+		      sigma env c) 
+  | Psuffices c ->  
+      Psuffices (interp_cut interp_suffices_clause sigma env c)
   | Prew (s,c) -> Prew (s,interp_cut 
-			  (interp_constr_in_type (get_eq_typ info env))
+			  (interp_no_bind (interp_statement 
+			     (interp_constr_in_type (get_eq_typ info env))))
 			  sigma env c) 
+
   | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
   | Pcase (params,pat,hyps) -> 
-      let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in 
+      let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in 
 	Pcase (tparams,tpat,thyps)
   | Ptake witl -> 
       Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli
index 08d97646..bd085938 100644
--- a/tactics/decl_interp.mli
+++ b/tactics/decl_interp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Tacinterp
 open Decl_expr
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index e7acd6d6..b19d8c04 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Util
 open Pp
@@ -54,7 +54,7 @@ let tcl_change_info_gen info_gen =
       [pftree] ->
 	{pftree with
 	   goal=gl;
-	   ref=Some (Change_evars,[pftree])} 
+	   ref=Some (Prim Change_evars,[pftree])} 
     | _ -> anomaly "change_info : Wrong number of subtrees")
 
 let tcl_change_info info gls =  tcl_change_info_gen (Some (pm_in info)) gls
@@ -92,18 +92,29 @@ let mk_evd metalist gls =
   let add_one (meta,typ) evd = 
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
+
+let set_last cpl gls = 
+  let info = get_its_info gls in
+    tclTHEN 
+      begin 
+	match info.pm_last with 
+	    Some (lid,false) when 
+	      not (occur_id [] lid info.pm_partial_goal) -> 
+		tclTRY (clear [lid])
+	  | _ -> tclIDTAC
+      end
+      begin
+	tcl_change_info 
+	  {info with 
+	    pm_last=Some cpl }
+      end gls
 	  
 (* start a proof *)
 
 let start_proof_tac gls=
   let gl=sig_it gls in
-  let info={pm_last=Anonymous;
+  let info={pm_last=None;
 	    pm_partial_goal=mkMeta 1; 
-	    pm_hyps= 
-      begin
-	let hyps = pf_ids_of_hyps gls in
-	  List.fold_right Idset.add hyps Idset.empty
-      end; 
 	    pm_subgoals= [1,gl.evar_concl];
 	    pm_stack=[]} in
     {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, 
@@ -259,13 +270,12 @@ let add_justification_hyps keep items gls =
 	    letin_tac false (Names.Name id) c Tacexpr.nowhere gls in 
     tclMAP add_aux items gls   
 
-let apply_to_prepared_goal items kont gls =
+let prepare_goal items gls =
   let tokeep = ref Idset.empty in
   let auxres = add_justification_hyps tokeep items gls in
    tclTHENLIST
      [ (fun _ -> auxres);
-       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep);
-       kont ] gls
+       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls
 
 let my_automation_tac = ref 
   (fun gls -> anomaly "No automation registered")
@@ -276,7 +286,7 @@ let automation_tac gls = !my_automation_tac gls
 
 let justification tac gls= 
     tclORELSE 
-      (tclSOLVE [tac]) 
+      (tclSOLVE [tclTHEN tac assumption]) 
       (fun gls -> 
 	 if get_strictness () then 
 	   error "insufficient justification" 
@@ -286,8 +296,8 @@ let justification tac gls=
 	     daimon_tac gls
 	   end) gls
 
-let default_justification items gls=
-  justification (apply_to_prepared_goal items automation_tac) gls
+let default_justification elems gls=
+  justification (tclTHEN (prepare_goal elems) automation_tac) gls
 
 (* code for have/then/thus/hence *)
 
@@ -342,10 +352,11 @@ let enstack_subsubgoals env se stack gls=
 	    Array.iteri process gentypes
       | _ -> ()
 
-let find_subsubgoal env c ctyp skip evd metas gls =
+let find_subsubgoal env c ctyp skip evd metas submetas gls =
   let stack = Stack.create () in
   let max_meta = 
-    List.fold_left (fun a (m,_) -> max a m) 0 metas in
+    let tmp = List.fold_left (fun a (m,_) -> max a m) 0 metas in
+      List.fold_left (fun a (m,_) -> max a m) tmp submetas in
   let _ = 
     List.iter (fun (m,typ) -> 
 		 Stack.push 
@@ -361,7 +372,10 @@ let find_subsubgoal env c ctyp skip evd metas gls =
 	  Unification.w_unify true env Reduction.CUMUL 
 	    ctyp se.se_type se.se_evd in
 	  if n <= 0 then 
-	      {se with se_evd=meta_assign se.se_meta c unifier}	  
+	    {se with 
+	       se_evd=meta_assign se.se_meta c unifier;
+	       se_meta_list=replace_in_list 
+		se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
       with _ -> 
@@ -381,7 +395,6 @@ let rec nf_list evd =
 	else
 	  (m,nf_meta evd typ)::nf_list evd others
 
-
 let rec max_linear_context meta_one c =
   if !meta_one = None then
      if isMeta c then
@@ -403,12 +416,12 @@ let rec max_linear_context meta_one c =
     else
       map_constr (max_linear_context meta_one) c
 
-let thus_tac c ctyp gls =  
+let thus_tac c ctyp submetas gls =  
   let info = get_its_info gls in
-  let evd0 = mk_evd info.pm_subgoals gls in
+  let evd0 = mk_evd (info.pm_subgoals@submetas) gls in
   let list,evd = 
     try
-      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls
+      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals submetas gls
     with Not_found -> 
       error "I could not relate this statement to the thesis" in
   let nflist = nf_list evd list in
@@ -450,34 +463,44 @@ let mk_stat_or_thesis info = function
 	  [_,c] -> c
 	| _ -> error 
 	    "\"thesis\" is split, please specify which part you refer to."
-			
-let instr_cut mkstat _thus _then cut gls0 = 
-  let info = get_its_info gls0 in  
-  let just_tac gls = 
+
+let just_tac _then cut info gls0 =
+  let items_tac gls =
     match cut.cut_by with
-        Automated l ->	
-	  let elems = 
+	None -> tclIDTAC gls
+      | Some items -> 
+	  let items_ = 
 	    if _then then
 	      match info.pm_last with
-		  Anonymous -> l
-		| Name id -> (mkVar id) ::l
-	    else l in
-	    default_justification elems gls
-      | By_tactic t -> 
-	  justification (Tacinterp.eval_tactic t) gls in
-  let c_id = match cut.cut_stat.st_label with 
+		  None -> error "no previous statement to use"
+		| Some (id,_) -> (mkVar id)::items
+	    else items
+	  in prepare_goal items_ gls in
+  let method_tac gls = 
+    match cut.cut_using with
+        None ->	
+	  automation_tac gls
+      | Some tac -> 
+	  (Tacinterp.eval_tactic tac) gls in
+    justification (tclTHEN items_tac method_tac) gls0
+			
+let instr_cut mkstat _thus _then cut gls0 = 
+  let info = get_its_info gls0 in 
+  let stat = cut.cut_stat in
+  let (c_id,_) as cpl = match stat.st_label with 
       Anonymous -> 
-	pf_get_new_id (id_of_string "_fact") gls0 
-    | Name id -> id in
-  let c_stat = mkstat info cut.cut_stat.st_it in
+	pf_get_new_id (id_of_string "_fact") gls0,false 
+    | Name id -> id,true in
+  let c_stat = mkstat info stat.st_it in
   let thus_tac gls= 
     if _thus then 
-      thus_tac (mkVar c_id) c_stat gls
+      thus_tac (mkVar c_id) c_stat [] gls
     else tclIDTAC gls in
-  let ninfo = {info with pm_last=Name c_id} in
     tclTHENS (internal_cut c_id c_stat) 
-      [tclTHEN tcl_erase_info just_tac;
-       tclTHEN (tcl_change_info ninfo) thus_tac] gls0
+      [tclTHEN tcl_erase_info (just_tac _then cut info);
+       tclTHEN (set_last cpl) thus_tac] gls0
+
+
 
 (* iterated equality *)
 let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
@@ -498,24 +521,28 @@ let instr_rew _thus rew_side cut gls0 =
   let info = get_its_info gls0 in
   let last_id = 	    
     match info.pm_last with
-	Anonymous -> error "no previous equality"
-      | Name id -> id in
+	None -> error "no previous equality"
+      | Some (id,_) -> id in
   let typ,lhs,rhs = decompose_eq last_id gls0 in  
-  let just_tac gls = 
+  let items_tac gls =
     match cut.cut_by with
-        Automated l ->	
-	  let elems = (mkVar last_id) :: l in
-	    default_justification elems gls
-      | By_tactic t -> 
-	  justification (Tacinterp.eval_tactic t) gls in
-  let c_id = match cut.cut_stat.st_label with 
+	None -> tclIDTAC gls
+      | Some items -> prepare_goal items gls in
+  let method_tac gls = 
+    match cut.cut_using with
+        None ->	
+	  automation_tac gls
+      | Some tac -> 
+	  (Tacinterp.eval_tactic tac) gls in
+  let just_tac gls =
+    justification (tclTHEN items_tac method_tac) gls in
+  let (c_id,_) as cpl = match cut.cut_stat.st_label with 
       Anonymous -> 
-	pf_get_new_id (id_of_string "_eq") gls0 
-    | Name id -> id in
-  let ninfo = {info with pm_last=Name c_id} in
+	pf_get_new_id (id_of_string "_eq") gls0,false 
+    | Name id -> id,true in
   let thus_tac new_eq gls= 
     if _thus then 
-      thus_tac (mkVar c_id) new_eq gls
+      thus_tac (mkVar c_id) new_eq [] gls
     else tclIDTAC gls in
     match rew_side with 
 	Lhs ->
@@ -524,14 +551,14 @@ let instr_rew _thus rew_side cut gls0 =
 	      [tclTHEN tcl_erase_info 
 		 (tclTHENS (transitivity lhs) 
 		    [just_tac;exact_check (mkVar last_id)]);
-	       tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0
+	       tclTHEN (set_last cpl) (thus_tac new_eq)] gls0
       | Rhs ->
 	  let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
 	    tclTHENS (internal_cut c_id new_eq) 
 	      [tclTHEN tcl_erase_info 
 		 (tclTHENS (transitivity rhs) 
 		    [exact_check (mkVar last_id);just_tac]);
-	       tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0
+	       tclTHEN (set_last cpl) (thus_tac new_eq)] gls0
 	      
 
 
@@ -539,22 +566,21 @@ let instr_rew _thus rew_side cut gls0 =
 
 let instr_claim _thus st gls0 = 
   let info = get_its_info gls0 in  
-  let id = match st.st_label with 
-      Anonymous -> pf_get_new_id (id_of_string "_claim") gls0 
-    | Name id -> id in
+  let (id,_) as cpl = match st.st_label with 
+      Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false 
+    | Name id -> id,true in
   let thus_tac gls= 
     if _thus then 
-      thus_tac (mkVar id) st.st_it gls
+      thus_tac (mkVar id) st.st_it [] gls
     else tclIDTAC gls in
   let ninfo1 = {info with 
 		  pm_stack=
       (if _thus then Focus_claim else Claim)::info.pm_stack;
 		  pm_partial_goal=mkMeta 1;
 	          pm_subgoals = [1,st.st_it]} in
-  let ninfo2 = {info with pm_last=Name id} in
     tclTHENS (internal_cut id st.st_it) 
       [tcl_change_info ninfo1;
-       tclTHEN (tcl_change_info ninfo2) thus_tac] gls0
+       tclTHEN (set_last cpl) thus_tac] gls0
 
 (* tactics for assume *)
 
@@ -565,11 +591,6 @@ let reset_concl gls =
 	 pm_partial_goal=mkMeta 1;
 	 pm_subgoals= [1,gls.it.evar_concl]} gls
 
-let set_last id gls = 
-  let info = get_its_info gls in
-    tcl_change_info 
-      {info with 
-	 pm_last=Name id} gls
 
 let intro_pm id gls=
   let info = get_its_info gls in
@@ -579,20 +600,14 @@ let intro_pm id gls=
       | _ -> error "Goal is split"
 
 let push_intro_tac coerce nam gls = 
-      let hid =
+      let (hid,_) as cpl =
 	match nam with 
-	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls 
-	  | Name id -> id in
-      let mark_id gls0 =
-	let info = get_its_info gls0 in
-	let ninfo = {info with 
-		       pm_last = Name hid;
-		       pm_hyps = Idset.add hid info.pm_hyps } in
-	  tcl_change_info ninfo gls0 in
+	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false 
+	  | Name id -> id,true in
 	tclTHENLIST 
 	  [intro_pm hid;
 	   coerce hid;
-	   mark_id]
+	   set_last cpl]
 	  gls 
 
 let assume_tac hyps gls = 
@@ -635,6 +650,56 @@ let assume_st_letin hyps gls =
 	       convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
 	 hyps tclIDTAC gls 
 
+(* suffices *)
+
+let free_meta info = 
+  let max_next (i,_) j  = if j <= i then succ i else j in
+  List.fold_right max_next info.pm_subgoals 1
+
+let rec metas_from n hyps = 
+  match hyps with
+      _ :: q -> n :: metas_from (succ n) q
+    | [] -> []
+ 
+let rec build_product args body =
+  match args with 
+      (Hprop st| Hvar st )::rest -> 
+	let pprod= lift 1 (build_product rest body) in
+	let lbody =
+	  match st.st_label with
+	      Anonymous -> pprod
+	    | Name id -> subst_term (mkVar id) pprod in
+	  mkProd (st.st_label, st.st_it, lbody)
+    | [] -> body 
+
+let rec build_applist prod = function
+    [] -> [],prod
+  | n::q -> 
+      let (_,typ,_) = destProd prod in
+      let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
+	(n,typ)::ctx,head
+
+let instr_suffices _then cut gls0 = 
+  let info = get_its_info gls0 in 
+  let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in 
+  let ctx,hd = cut.cut_stat in
+  let c_stat = build_product ctx (mk_stat_or_thesis info hd) in
+  let metas = metas_from (free_meta info) ctx in
+  let c_ctx,c_head = build_applist c_stat metas in
+  let c_term = applist (mkVar c_id,List.map mkMeta metas) in  
+  let thus_tac gls= 
+    thus_tac c_term c_head c_ctx gls in
+   tclTHENS (internal_cut c_id c_stat) 
+     [tclTHENLIST 
+	 [ tcl_change_info 
+	     {info with 
+	       pm_partial_goal=mkMeta 1;
+	       pm_subgoals=[1,c_stat]};
+	   assume_tac ctx;   
+	   tcl_erase_info;
+	   just_tac _then cut info];
+      tclTHEN (set_last (c_id,false)) thus_tac] gls0
+
 (* tactics for consider/given *)
 
 let update_goal_info gls =
@@ -684,14 +749,7 @@ let pm_rename_hyp id hid gls =
 let rec consider_match may_intro introduced available expected gls =
   match available,expected with 
       [],[] ->
-	if not may_intro then 
 	  set_last (List.hd introduced) gls
-	else
-	  let info = get_its_info gls in 
-	  let nameset=List.fold_right Idset.add introduced info.pm_hyps in
-	    tcl_change_info {info with 
-			       pm_last = Name (List.hd introduced);
-			       pm_hyps = nameset} gls
     | _,[] -> error "last statements do not match a complete hypothesis" 
 	(* should tell which ones *)
     | [],hyps -> 
@@ -704,7 +762,7 @@ let rec consider_match may_intro introduced available expected gls =
 		(fun _ -> 
 		   error "not enough sub-hypotheses to match statements")
 		gls 
-          end
+          end 
 	else
 	  error "not enough sub-hypotheses to match statements" 
 	    (* should tell which ones *)
@@ -713,11 +771,11 @@ let rec consider_match may_intro introduced available expected gls =
 	  begin
 	    match st.st_label with 
 		Anonymous -> 
-		  consider_match may_intro (id::introduced) rest_ids rest
+		  consider_match may_intro ((id,false)::introduced) rest_ids rest
 	      | Name hid -> 
 		  tclTHENLIST 
 		    [pm_rename_hyp id hid;
-		     consider_match may_intro (hid::introduced) rest_ids rest]
+		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
 	  end
 	  begin
 	    (fun gls -> 
@@ -753,7 +811,7 @@ let rec take_tac wits gls =
       [] -> tclIDTAC gls
     | wit::rest ->  
 	let typ = pf_type_of gls wit in  
-	  tclTHEN (thus_tac wit typ) (take_tac rest)  gls
+	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
 (* tactics for define *)
@@ -874,17 +932,6 @@ let per_tac etype casee gls=
 
 (* suppose *)
 
-let rec build_product args body =
-  match args with 
-      (Hprop st| Hvar st )::rest -> 
-	let pprod= lift 1 (build_product rest body) in
-	let lbody =
-	  match st.st_label with
-	      Anonymous -> body
-	    | Name id -> subst_term (mkVar id) pprod in
-	  mkProd (st.st_label, st.st_it, lbody)
-    | [] -> body 
-
 let register_nodep_subcase id= function
     Per(et,pi,ek,clauses)::s ->
       begin
@@ -1201,6 +1248,30 @@ let hrec_for obj_id fix_id per_info gls=
 	    else None
       | _ -> None
 
+
+(* custom elim performs the case analysis of hypothesis id from the local 
+context, 
+
+- generalizing hypotheses below id
+- computing the elimination predicate (abstract inductive predicate) 
+- build case analysis term 
+- generalize rec_calls (use wf_paths)
+- vector of introduced identifiers per branch 
+
+match id in t return p with
+ C1 ... => ?1 
+|C2 ... => ?2
+...
+end*)
+
+
+    
+
+
+
+
+
+
 let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
   match tree with
       Pop t ->  
@@ -1388,6 +1459,8 @@ let rec do_proof_instr_gen _thus _then instr =
 	do_proof_instr_gen true true i
     | Pcut c ->
 	instr_cut mk_stat_or_thesis _thus _then c
+    | Psuffices c ->
+	instr_suffices _then c 
     | Prew (s,c) ->
 	assert (not _then);
 	instr_rew _thus s c
@@ -1412,7 +1485,7 @@ let eval_instr {instr=instr} =
 let rec preprocess pts instr =
   match instr with
     Phence i |Pthus i | Pthen i -> preprocess pts i
-  | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
+  | Psuffices _ | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
   | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ 
   | Pdefine (_,_,_) | Pper _ | Prew _ ->
       check_not_per pts;
@@ -1428,11 +1501,23 @@ let rec preprocess pts instr =
 let rec postprocess pts instr = 
   match instr with
       Phence i | Pthus i | Pthen i -> postprocess pts i
-    | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
+    | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
     | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
-    | Pescape ->
-	escape_command pts
+    | Pescape -> escape_command pts
+    | Pend (B_elim ET_Induction) ->
+  	begin
+	  let pf = proof_of_pftreestate pts in
+	  let (pfterm,_) = extract_open_pftreestate pts in
+	  let env =  Evd.evar_env (goal_of_proof pf) in
+	    try 
+	      Inductiveops.control_only_guard env pfterm;
+	      goto_current_focus_or_top (mark_as_done pts)
+ 	    with 
+		Type_errors.TypeError(env,
+				      Type_errors.IllFormedRecBody(_,_,_)) ->
+		  anomaly "\"end induction\" generated an ill-formed fixpoint"
+	end
     | Pend _ -> 
 	goto_current_focus_or_top (mark_as_done pts)
 
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index ba8dc7b6..642f2755 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Refiner
 open Names
@@ -112,7 +112,15 @@ val hrec_for:
 
 val consider_match :
    bool ->
-    Names.Idset.elt list ->
+    (Names.Idset.elt*bool) list ->
     Names.Idset.elt list ->
     (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
     Proof_type.tactic
+
+val thus_tac : constr -> constr -> (metavariable * types) list ->
+  tactic
+
+val build_applist :    Term.types ->
+    Term.metavariable list ->
+    (Term.metavariable * Term.types) list * Term.types
+
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2526c84e..754aec1c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 9211 2006-10-05 12:38:33Z letouzey $ *)
+(* $Id: equality.ml 9521 2007-01-23 14:31:21Z notin $ *)
 
 open Pp
 open Util
@@ -282,7 +282,7 @@ let find_positions env sigma t1 t2 =
 	  let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
-	  if sp1 = sp2 then
+	  if is_conv env sigma hd1 hd2 then
 	    let nrealargs = constructor_nrealargs env sp1 in
 	    let rargs1 = list_lastn nrealargs args1 in
 	    let rargs2 = list_lastn nrealargs args2 in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a8204665..d6de2666 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 9266 2006-10-24 09:03:15Z herbelin $ *)
+(* $Id: extratactics.ml4 9430 2006-12-12 08:25:19Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -285,7 +285,7 @@ open Evar_tactics
 (* evar creation *)
 
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" constr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 76014955..4133a3f6 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hiddentac.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: hiddentac.ml 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 open Term
 open Proof_type
@@ -29,6 +29,8 @@ let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
 let h_assumption     = abstract_tactic TacAssumption assumption
 let h_exact c        = abstract_tactic (TacExact c) (exact_check c)
 let h_exact_no_check c = abstract_tactic (TacExactNoCheck c) (exact_no_check c)
+let h_vm_cast_no_check c = 
+  abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
 let h_apply cb       = abstract_tactic (TacApply cb) (apply_with_bindings cb)
 let h_elim cb cbo    = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo)
 let h_elim_type c    = abstract_tactic (TacElimType c) (elim_type c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index df1dfde0..1456601b 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hiddentac.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
+(*i $Id: hiddentac.mli 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (*i*)
 open Names
@@ -30,6 +30,7 @@ val h_intros_until    : quantified_hypothesis -> tactic
 val h_assumption      : tactic
 val h_exact           : constr -> tactic
 val h_exact_no_check  : constr -> tactic
+val h_vm_cast_no_check  : constr -> tactic
 
 val h_apply           : constr with_bindings -> tactic
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 712e1f81..5b162729 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refine.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: refine.ml 9364 2006-11-11 11:59:42Z herbelin $ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
@@ -89,7 +89,7 @@ and pp_sg sg =
  *  meta_map correspond à celui des buts qui seront engendrés par le refine.
  *)
 
-let replace_by_meta env = function
+let replace_by_meta env sigma = function
   | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
   | (TH (c,mm,_)) as th ->
       let n = Evarutil.new_meta() in
@@ -101,7 +101,7 @@ let replace_by_meta env = function
 	| Lambda (Anonymous,c1,c2) when isCast c2 ->
 	    let _,_,t = destCast c2 in mkArrow c1 t
 	| _ -> (* (App _ | Case _) -> *)
-	    Retyping.get_type_of_with_meta env Evd.empty mm c
+	    Retyping.get_type_of_with_meta env sigma mm c
 	(*
 	| Fix ((_,j),(v,_,_)) ->
 	    v.(j) (* en pleine confiance ! *)
@@ -112,12 +112,12 @@ let replace_by_meta env = function
 
 exception NoMeta
 
-let replace_in_array keep_length env a =
+let replace_in_array keep_length env sigma a =
   if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
     raise NoMeta;
   let a' = Array.map (function
 			| (TH (c,mm,[])) when not keep_length -> c,mm,[]
-			| th -> replace_by_meta env th) a 
+			| th -> replace_by_meta env sigma th) a 
   in
   let v' = Array.map pi1 a' in
   let mm = Array.fold_left (@) [] (Array.map pi2 a') in
@@ -128,7 +128,7 @@ let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_" in
   next_global_ident_away true id (ids_of_named_context (named_context env))
 
-let rec compute_metamap env c = match kind_of_term c with
+let rec compute_metamap env sigma c = match kind_of_term c with
   (* le terme est directement une preuve *)
   | (Const _ | Evar _ | Ind _ | Construct _ |
     Sort _ | Var _ | Rel _) -> 
@@ -148,12 +148,12 @@ let rec compute_metamap env c = match kind_of_term c with
   | Lambda (name,c1,c2) ->
       let v = fresh env name in
       let env' = push_named (v,None,c1) env in
-      begin match compute_metamap env' (subst1 (mkVar v) c2) with
+      begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
 	(* terme de preuve incomplet *)    
 	| th ->
-	    let m,mm,sgp = replace_by_meta env' th in
+	    let m,mm,sgp = replace_by_meta env' sigma th in
 	    TH (mkLambda (Name v,c1,m), mm, sgp)
       end
 
@@ -162,21 +162,21 @@ let rec compute_metamap env c = match kind_of_term c with
 	error "Refine: body of let-in cannot contain existentials";
       let v = fresh env name in
       let env' = push_named (v,Some c1,t1) env in
-      begin match compute_metamap env' (subst1 (mkVar v) c2) with
+      begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
 	(* terme de preuve incomplet *)    
 	| th ->
-	    let m,mm,sgp = replace_by_meta env' th in
+	    let m,mm,sgp = replace_by_meta env' sigma th in
 	    TH (mkLetIn (Name v,c1,t1,m), mm, sgp)
       end
 
   (* 4. Application *)
   | App (f,v) ->
-      let a = Array.map (compute_metamap env) (Array.append [|f|] v) in
+      let a = Array.map (compute_metamap env sigma) (Array.append [|f|] v) in
       begin
 	try
-	  let v',mm,sgp = replace_in_array false env a in
+	  let v',mm,sgp = replace_in_array false env sigma a in
           let v'' = Array.sub v' 1 (Array.length v) in
           TH (mkApp(v'.(0), v''),mm,sgp)
 	with NoMeta ->
@@ -187,10 +187,10 @@ let rec compute_metamap env c = match kind_of_term c with
       (* bof... *)
       let nbr = Array.length v in
       let v = Array.append [|p;cc|] v in
-      let a = Array.map (compute_metamap env) v in
+      let a = Array.map (compute_metamap env sigma) v in
       begin
 	try
-	  let v',mm,sgp = replace_in_array false env a in
+	  let v',mm,sgp = replace_in_array false env sigma a in
 	  let v'' = Array.sub v' 2 nbr in
 	  TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
 	with NoMeta ->
@@ -204,12 +204,12 @@ let rec compute_metamap env c = match kind_of_term c with
       let fi' = Array.map (fun id -> Name id) vi in
       let env' = push_named_rec_types (fi',ai,v) env in
       let a = Array.map
-		(compute_metamap env')
+		(compute_metamap env' sigma)
 		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
       in
       begin
 	try
-	  let v',mm,sgp = replace_in_array true env' a in
+	  let v',mm,sgp = replace_in_array true env' sigma a in
 	  let fix = mkFix ((ni,i),(fi',ai,v')) in
 	  TH (fix,mm,sgp)
 	with NoMeta ->
@@ -217,7 +217,7 @@ let rec compute_metamap env c = match kind_of_term c with
       end
 	      
   (* Cast. Est-ce bien exact ? *)
-  | Cast (c,_,t) -> compute_metamap env c
+  | Cast (c,_,t) -> compute_metamap env sigma c
       (*let TH (c',mm,sgp) = compute_metamap sign c in
 	TH (mkCast (c',t),mm,sgp) *)
       
@@ -234,12 +234,12 @@ let rec compute_metamap env c = match kind_of_term c with
       let fi' = Array.map (fun id -> Name id) vi in
       let env' = push_named_rec_types (fi',ai,v) env in
       let a = Array.map
-		(compute_metamap env')
+		(compute_metamap env' sigma)
 		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
       in
       begin
 	try
-	  let v',mm,sgp = replace_in_array true env' a in
+	  let v',mm,sgp = replace_in_array true env' sigma a in
 	  let cofix = mkCoFix (i,(fi',ai,v')) in
 	  TH (cofix,mm,sgp)
 	with NoMeta ->
@@ -341,5 +341,5 @@ let refine oc gl =
   let (sigma,c) = Evarutil.evars_to_metas sigma oc in
   (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
      complicated to update meta types when passing through a binder *)
-  let th = compute_metamap (pf_env gl) c in
+  let th = compute_metamap (pf_env gl) sigma c in
   tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1e8c55ef..29150c27 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 9302 2006-10-27 21:21:17Z barras $ *)
+(* $Id: tacinterp.ml 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 open Constrintern
 open Closure
@@ -626,6 +626,7 @@ let rec intern_atomic lf ist x =
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
   | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
   | TacElim (cb,cbo) ->
       TacElim (intern_constr_with_bindings ist cb,
@@ -1992,6 +1993,7 @@ and interp_atomic ist gl = function
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
+  | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
   | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
   | TacElim (cb,cbo) ->
       h_elim (interp_constr_with_bindings ist gl cb)
@@ -2320,6 +2322,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacAssumption as x -> x
   | TacExact c -> TacExact (subst_rawconstr subst c)
   | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
   | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
   | TacElim (cb,cbo) ->
       TacElim (subst_raw_with_bindings subst cb,
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f77814de..cb98ec18 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 9281 2006-10-26 07:52:31Z herbelin $ *)
+(* $Id: tactics.ml 9605 2007-02-07 12:19:19Z notin $ *)
 
 open Pp
 open Util
@@ -603,6 +603,7 @@ let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
     match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
+	  let c2 = refresh_universes c2 in
 	  tclTHENLAST
 	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
 	    (apply_term c [mkMeta (new_meta())]) gl
@@ -622,6 +623,11 @@ let exact_check c gl =
 
 let exact_no_check = refine_no_check
 
+let vm_cast_no_check c gl = 
+  let concl = pf_concl gl in
+  refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
+
+
 let exact_proof c gl =
   (* on experimente la synthese d'ise dans exact *)
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
@@ -954,7 +960,7 @@ let true_cut = assert_tac true
 (**************************)
 
 let generalize_goal gl c cl =
-  let t = pf_type_of gl c in
+  let t = refresh_universes (pf_type_of gl c) in
   match kind_of_term c with
     | Var id ->
 	(* The choice of remembering or not a non dependent name has an impact
@@ -2448,40 +2454,40 @@ let abstract_subproof name tac gls =
   let sign,secsign = 
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) -> 
-	 if mem_named_context id current_sign &
-           interpretable_as_section_decl (Sign.lookup_named id current_sign) d
-         then (s1,push_named_context_val d s2)
-	 else (add_named_decl d s1,s2)) 
+	if mem_named_context id current_sign &
+          interpretable_as_section_decl (Sign.lookup_named id current_sign) d
+        then (s1,push_named_context_val d s2)
+	else (add_named_decl d s1,s2)) 
       global_sign (empty_named_context,empty_named_context_val) in
   let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
-  if occur_existential concl then
-    error "\"abstract\" cannot handle existentials";
-  let lemme =
-    start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
-    let _,(const,kind,_) =
-      try
-	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
-	let r = cook_proof () in 
-	delete_current_proof (); r
-      with e when catchable_exception e -> 
-	(delete_current_proof(); raise e)
-    in   (* Faudrait un peu fonctionnaliser cela *)
-    let cd = Entries.DefinitionEntry const in
-    let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
-    constr_of_global (ConstRef con)
-  in
-  exact_no_check 
-    (applist (lemme, 
-              List.rev (Array.to_list (instance_from_named_context sign))))
-    gls
+    if occur_existential concl then
+      error "\"abstract\" cannot handle existentials";
+    let lemme =
+      start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
+      let _,(const,kind,_) =
+	try
+	  by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
+	  let r = cook_proof () in 
+	    delete_current_proof (); r
+	with e -> 
+	  (delete_current_proof(); raise e)
+      in   (* Faudrait un peu fonctionnaliser cela *)
+      let cd = Entries.DefinitionEntry const in
+      let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
+	constr_of_global (ConstRef con)
+    in
+      exact_no_check 
+	(applist (lemme, 
+		 List.rev (Array.to_list (instance_from_named_context sign))))
+	gls
 
 let tclABSTRACT name_op tac gls = 
   let s = match name_op with 
     | Some s -> s 
     | None   -> add_suffix (get_current_proof_name ()) "_subproof" 
   in  
-  abstract_subproof s tac gls
+    abstract_subproof s tac gls
 
 
 let admit_as_an_axiom gls =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 48b9f432..aece3231 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactics.mli 9266 2006-10-24 09:03:15Z herbelin $ i*)
+(*i $Id: tactics.mli 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (*i*)
 open Names
@@ -106,6 +106,7 @@ val intros_pattern    : identifier option -> intro_pattern_expr list -> tactic
 
 val assumption       : tactic
 val exact_no_check   : constr -> tactic
+val vm_cast_no_check : constr -> tactic
 val exact_check      : constr -> tactic
 val exact_proof      : Topconstr.constr_expr -> tactic