Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 2048 insertions, 3 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1ecb29f7e4..d1caa98625 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -192,7 +192,10 @@ let make_exact_entry (c,cty) =
 	   { pri=0; pat=None; code=Give_exact c })
 
 let dummy_goal =
-  {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty};
+  {it={evar_hyps=empty_named_context_val;
+       evar_concl=mkProp;
+       evar_body=Evar_empty;
+       evar_extra=None};
    sigma=Evd.empty}
 
 let make_apply_entry env sigma (eapply,verbose) (c,cty) =
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
new file mode 100644
index 0000000000..8ace0a085b
--- /dev/null
+++ b/tactics/decl_interp.ml
@@ -0,0 +1,429 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util
+open Names
+open Topconstr
+open Tacinterp
+open Tacmach
+open Decl_expr
+open Decl_mode
+open Pretyping.Default
+open Rawterm
+open Term
+open Pp
+
+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_statement intern_it globs st =
+  {st_label=st.st_label;
+   st_it=intern_it globs st.st_it}
+    
+let intern_constr_or_thesis globs = function
+    Thesis n -> Thesis n
+  | This c -> This (intern_constr globs c)
+
+let add_var id globs= 
+  let l1,l2=globs.ltacvars in
+    {globs with ltacvars= (id::l1),(id::l2)}
+
+let add_name nam globs=
+ match nam with 
+     Anonymous -> globs
+   | Name id -> add_var id globs
+
+let intern_hyp iconstr globs = function 
+    Hvar (loc,(id,topt)) -> add_var id globs,
+      Hvar (loc,(id,option_map (intern_constr globs) topt))
+  | Hprop st -> add_name st.st_label globs,
+      Hprop (intern_statement iconstr globs st)
+
+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 intern_casee globs = function 
+    Real c -> Real (intern_constr globs c)
+  | Virtual cut -> Virtual (intern_cut intern_constr globs cut) 
+
+let intern_hyp_list args globs =
+  let intern_one globs (loc,(id,opttyp)) =
+    (add_var id globs),
+    (loc,(id,option_map (intern_constr globs) opttyp)) in
+  list_fold_map intern_one globs args 
+
+let intern_fundecl args body globs= 
+  let nglobs,nargs = intern_hyp_list args globs in
+    nargs,intern_constr nglobs body
+          
+let rec add_vars_of_simple_pattern globs = function
+    CPatAlias (loc,p,id) ->
+      add_vars_of_simple_pattern (add_var id globs) p
+(*      Stdpp.raise_with_loc loc 
+	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
+  | CPatOr (loc, _)->
+      Stdpp.raise_with_loc loc 
+	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+  | CPatDelimiters (_,_,p) ->
+      add_vars_of_simple_pattern globs p
+  | CPatCstr (_,_,pl) | CPatNotation(_,_,pl) ->
+      List.fold_left add_vars_of_simple_pattern globs pl
+  | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
+  |  _  -> globs 
+
+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) 
+  | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
+  | Pcase (params,pat,hyps) -> 
+      let nglobs,nparams = intern_hyp_list params globs in
+      let nnglobs= add_vars_of_simple_pattern nglobs pat in
+      let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in
+	Pcase (nparams,pat,nhyps) 
+  | Ptake witl -> Ptake (List.map (intern_constr globs) witl)
+  | Pconsider (c,hyps) -> Pconsider (intern_constr globs c,
+				      intern_hyps intern_constr globs hyps)
+  | Pper (et,c) -> Pper (et,intern_casee globs c)
+  | Pend bt -> Pend bt
+  | Pescape -> Pescape
+  | Passume hyps -> Passume (intern_hyps intern_constr globs hyps)
+  | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps)
+  | Plet hyps -> Plet (intern_hyps intern_constr globs hyps)
+  | Pclaim st -> Pclaim (intern_statement intern_constr globs st)
+  | Pfocus st -> Pfocus (intern_statement intern_constr globs st)
+  | Pdefine (id,args,body) -> 
+      let nargs,nbody = intern_fundecl args body globs in
+	Pdefine (id,nargs,nbody)
+  | Pcast (id,typ) ->
+      Pcast (id,intern_constr globs typ)
+
+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 
+
+let interp_constr check_sort env sigma c = 
+  if check_sort then 
+    understand_type env sigma (fst c) 
+  else 
+    understand env sigma (fst c)
+
+let special_whd env =
+  let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+
+let decompose_eq env id =
+  let typ = Environ.named_type id env in
+  let whd = special_whd env typ in
+    match kind_of_term whd with
+	App (f,args)->
+	  if eq_constr f _eq && (Array.length args)=3 
+	  then args.(0)
+	  else error "previous step is not an equality"
+      | _ -> error "previous step is not an equality"
+
+let get_eq_typ info env =
+  let last_id = 	    
+    match info.pm_last with
+	Anonymous -> error "no previous equality"
+      | Name 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_statement interp_it env sigma st =
+  {st_label=st.st_label;
+   st_it=interp_it env sigma st.st_it}
+	
+let interp_constr_or_thesis check_sort env sigma = function
+    Thesis n -> Thesis n
+  | This c -> This (interp_constr check_sort env sigma c)
+
+let type_tester_var body typ = 
+  raw_app(dummy_loc,
+       RLambda(dummy_loc,Anonymous,typ,
+	       RSort (dummy_loc,RProp Null)),body)
+
+let abstract_one_hyp inject h raw = 
+  match h with 
+      Hvar (loc,(id,None)) ->  
+	RProd (dummy_loc,Name id, RHole (loc,Evd.BinderType (Name id)), raw)
+    | Hvar (loc,(id,Some typ)) ->  
+	RProd (dummy_loc,Name id,fst typ, 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 rec match_hyps blend names constr = function 
+    [] -> []
+  | hyp::q -> 
+      let (name,typ,body)=destProd constr in
+      let st= {st_label=name;st_it=substl names typ} in
+      let qnames=
+	match name with
+	    Anonymous -> mkMeta 0 :: names
+	  | Name id -> mkVar id :: names in
+      let qhyp = match hyp with
+	  Hprop st' -> Hprop (blend st st')
+	| Hvar _ -> Hvar st in
+	qhyp::(match_hyps blend qnames body q)
+
+let interp_hyps_gen inject blend env sigma hyps = 
+  let constr=understand env sigma (rawconstr_of_hyps inject hyps) in
+    match_hyps blend [] constr hyps
+
+let interp_hyps = interp_hyps_gen fst (fun x _ -> x)
+
+let dummy_prefix= id_of_string "__"
+
+let rec deanonymize ids = 
+  function 
+      PatVar (loc,Anonymous) -> 
+	let (found,known) = !ids in
+	let new_id=Nameops.next_ident_away dummy_prefix known in
+	let _= ids:= (loc,new_id) :: found , new_id :: known in
+	  PatVar (loc,Name new_id)
+    | PatVar (loc,Name id) as pat -> 
+	let (found,known) = !ids in
+	let _= ids:= (loc,id) :: found , known in
+	  pat
+    | PatCstr(loc,cstr,lpat,nam) -> 
+	PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
+
+let rec raw_of_pat =
+  function 
+      PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" 
+    | PatVar (loc,Name id) -> 
+	  RVar (loc,id)
+    | PatCstr(loc,((ind,_) as cstr),lpat,_) -> 
+	let mind= fst (Global.lookup_inductive ind) in
+	let rec add_params n q =
+	  if n<=0 then q else
+	    add_params (pred n) (RHole(dummy_loc,
+				       Evd.TomatchTypeParameter(ind,n))::q) in
+	    let args = List.map raw_of_pat lpat in 
+	      raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr),
+		   add_params mind.Declarations.mind_nparams args) 
+			 
+let prod_one_hyp = function
+    (loc,(id,None)) ->
+      (fun raw ->  
+	 RProd (dummy_loc,Name id, 
+		RHole (loc,Evd.BinderType (Name id)), raw))
+  | (loc,(id,Some typ)) -> 
+      (fun raw ->  
+	 RProd (dummy_loc,Name id,fst typ, raw))
+
+let prod_one_id (loc,id) raw =
+  RProd (dummy_loc,Name id,
+	 RHole (loc,Evd.BinderType (Name id)), raw)
+
+let let_in_one_alias (id,pat) raw =
+  RLetIn (dummy_loc,Name id,raw_of_pat pat, raw)
+
+let rec bind_primary_aliases map pat =
+  match pat with 
+      PatVar (_,_) -> map
+    | PatCstr(loc,_,lpat,nam) ->
+	let map1 =
+	  match nam with 
+	      Anonymous -> map
+	    | Name id -> (id,pat)::map 
+	in
+	  List.fold_left bind_primary_aliases map1 lpat
+
+let bind_secondary_aliases map subst =
+  List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst
+
+let bind_aliases patvars subst patt =
+  let map = bind_primary_aliases [] patt in
+  let map1 = bind_secondary_aliases map subst in
+  List.rev map1
+
+let interp_pattern env pat_expr = 
+  let patvars,pats = Constrintern.intern_pattern env pat_expr in
+    match pats with 
+	[] -> anomaly "empty pattern list"
+      | [subst,patt] ->
+	  (patvars,bind_aliases patvars subst patt,patt)
+      | _  -> anomaly "undetected disjunctive pattern"
+
+let rec match_args dest names constr = function 
+    [] -> [],names,substl names constr
+  | _::q -> 
+      let (name,typ,body)=dest constr in
+      let st={st_label=name;st_it=substl names typ} in
+      let qnames=
+	match name with
+	    Anonymous -> assert  false
+	  | Name id -> mkVar id :: names in
+      let args,bnames,body = match_args dest qnames body q in
+	st::args,bnames,body
+
+let rec match_aliases names constr = function 
+    [] -> [],names,substl names constr
+  | _::q -> 
+      let (name,c,typ,body)=destLetIn constr in
+      let st={st_label=name;st_it=(substl names c,substl names typ)} in
+      let qnames=
+	match name with
+	    Anonymous -> assert false
+	  | Name id -> mkVar id :: names in
+      let args,bnames,body = match_aliases qnames body q in
+	st::args,bnames,body
+
+let detype_ground c = Detyping.detype false [] [] c
+
+let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
+  let et,pinfo =
+    match info.pm_stack with
+	Per(et,pi,_,_)::_ -> et,pi
+      | _ -> error "No proof per cases/induction/inversion in progress." in
+  let mib,oib=Global.lookup_inductive  pinfo.per_ind in
+  let num_params = pinfo.per_nparams in
+  let _ = 
+    let expected = mib.Declarations.mind_nparams - num_params in
+      if List.length params <> expected then
+	errorlabstrm "suppose it is" 
+	  (str "Wrong number of extra arguments : " ++ 
+	     (if expected = 0 then str "none" else int expected) ++ 
+	     str "expected") in
+  let app_ind =
+    let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
+    let rparams = List.map detype_ground pinfo.per_params in 
+    let rparams_rec = 
+      List.map 
+	(fun (loc,(id,_)) -> 
+	   RVar (loc,id)) params in 
+    let dum_args= 
+      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark))
+	oib.Declarations.mind_nrealargs in
+      raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
+  let pat_vars,aliases,patt = interp_pattern env pat in
+  let inject = function
+      Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null)
+    | Thesis (Sub n) ->
+	error "thesis[_] is not allowed here"
+    | Thesis (For rec_occ) ->
+	if not (List.mem rec_occ pat_vars) then 
+	  errorlabstrm "suppose it is" 
+	    (str "Variable " ++ Nameops.pr_id rec_occ ++ 
+	       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 loc_ids,npatt =
+    let rids=ref ([],pat_vars) in
+    let npatt= deanonymize rids patt in 
+      List.rev (fst !rids),npatt in
+  let term2 =
+    RLetIn(dummy_loc,Anonymous,
+	   RCast(dummy_loc,raw_of_pat npatt,
+		 CastConv DEFAULTcast,app_ind),term1) in
+  let term3=List.fold_right let_in_one_alias aliases term2 in  
+  let term4=List.fold_right prod_one_id loc_ids term3 in
+  let term5=List.fold_right prod_one_hyp params term4 in
+  let constr = understand  sigma env term5 in
+  let tparams,nam4,rest4 = match_args destProd [] constr params in
+  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' =
+    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
+    tparams,{pat_vars=tpatvars;
+	     pat_aliases=taliases;
+	     pat_constr=pat_pat;
+	     pat_typ=pat_typ;
+	     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 abstract_one_arg = function
+    (loc,(id,None)) ->
+      (fun raw ->  
+	 RLambda (dummy_loc,Name id, 
+		RHole (loc,Evd.BinderType (Name id)), raw))
+  | (loc,(id,Some typ)) -> 
+      (fun raw ->  
+	 RLambda (dummy_loc,Name id,fst typ, raw))
+
+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
+    match_args destLambda [] constr args
+
+let rec interp_bare_proof_instr info sigma 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) 
+  | Prew (s,c) -> Prew (s,interp_cut 
+			  (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 
+	Pcase (tparams,tpat,thyps)
+  | Ptake witl -> 
+      Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
+  | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
+				     interp_hyps sigma env hyps)
+  | Pper (et,c) -> Pper (et,interp_casee sigma env c)
+  | Pend bt -> Pend bt
+  | Pescape -> Pescape
+  | Passume hyps -> Passume (interp_hyps sigma env hyps)
+  | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps)
+  | Plet hyps -> Plet (interp_hyps sigma env hyps)
+  | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st)
+  | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st)
+  | Pdefine (id,args,body) -> 
+      let nargs,_,nbody = interp_fun sigma env args body in
+	Pdefine (id,nargs,nbody)
+  | Pcast (id,typ) -> 
+      Pcast(id,interp_constr true sigma env typ)
+
+let rec interp_proof_instr info sigma env instr=
+  {emph = instr.emph;
+   instr = interp_bare_proof_instr info sigma env instr.instr}
+ 
+
+
diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli
new file mode 100644
index 0000000000..08d97646e6
--- /dev/null
+++ b/tactics/decl_interp.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Tacinterp
+open Decl_expr
+open Mod_subst
+
+
+val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
+val interp_proof_instr : Decl_mode.pm_info ->
+  Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
new file mode 100644
index 0000000000..26a2bd48e9
--- /dev/null
+++ b/tactics/decl_proof_instr.ml
@@ -0,0 +1,1474 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util
+open Pp
+open Evd
+
+open Refiner
+open Proof_type
+open Proof_trees
+open Tacmach
+open Tacinterp
+open Decl_expr
+open Decl_mode
+open Decl_interp
+open Rawterm
+open Names
+open Declarations
+open Tactics
+open Tacticals
+open Term
+open Termops
+open Reductionops
+open Goptions
+
+(* Strictness option *)
+
+let get_its_info gls = get_info gls.it
+
+let get_strictness,set_strictness = 
+  let strictness = ref false in
+    (fun () -> (!strictness)),(fun b -> strictness:=b)
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "strict mode";
+      optkey   = (SecondaryTable ("Strict","Proofs"));
+      optread  = get_strictness;
+      optwrite = set_strictness }
+
+let tcl_change_info_gen info_gen = 
+  (fun gls ->
+  let gl =sig_it gls in  
+    {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, 
+  function 
+      [pftree] ->
+	{pftree with
+	   goal=gl;
+	   ref=Some (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
+
+let tcl_erase_info gls =  tcl_change_info_gen None gls
+
+let special_whd gl=
+  let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let special_nf gl=
+  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
+    (fun t -> Closure.norm_val infos (Closure.inject t))
+
+let is_good_inductive env ind =
+  let mib,oib = Inductive.lookup_mind_specif env ind in
+    oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
+
+let check_not_per pts =
+  if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then
+    match get_stack pts with
+	Per (_,_,_,_)::_ -> 
+	  error "You are inside a proof per cases/induction.\n\
+Please \"suppose\" something or \"end\" it now."
+      | _ -> ()
+
+let get_thesis gls0 = 
+ let info = get_its_info gls0 in  
+    match info.pm_subgoals with
+	[m,thesis] -> thesis
+      | _ -> error "Thesis is split"
+
+let mk_evd metalist gls =
+  let evd0= create_evar_defs (sig_sig gls) in
+  let add_one (meta,typ) evd = 
+    meta_declare meta typ evd in
+    List.fold_right add_one metalist evd0
+	  
+(* start a proof *)
+
+let start_proof_tac gls=
+  let gl=sig_it gls in
+  let info={pm_last=Anonymous;
+	    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}, 
+  function 
+      [pftree] ->
+	{pftree with
+	   goal=gl;
+	   ref=Some (Decl_proof true,[pftree])} 
+    | _ -> anomaly "Dem : Wrong number of subtrees"
+
+let go_to_proof_mode () = 
+  Pfedit.mutate 
+    (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts))
+
+(* closing gaps *)
+
+let daimon_tac gls =
+  set_daimon_flag ();
+  ({it=[];sigma=sig_sig gls}, 
+   function 
+       [] ->
+	 {open_subgoals=0;
+	    goal=sig_it gls;
+	    ref=Some (Daimon,[])} 
+     | _ -> anomaly "Daimon: Wrong number of subtrees")
+    
+let daimon _ pftree =
+  set_daimon_flag ();
+  {pftree with
+     open_subgoals=0;
+     ref=Some (Daimon,[])}
+
+let daimon_subtree = map_pftreestate (fun _ ->  frontier_mapi daimon )
+
+(* marking closed blocks *)
+
+let rec is_focussing_instr = function
+    Pthus i | Pthen i | Phence i -> is_focussing_instr i
+  | Pescape | Pper _ | Pclaim _ | Pfocus _ 
+  | Psuppose _ | Pcase (_,_,_)  -> true
+  | _ -> false
+
+let mark_rule_as_done = function
+    Decl_proof true -> Decl_proof false
+  | Decl_proof false ->
+      anomaly "already marked as done"
+  | Nested(Proof_instr (lock_focus,instr),spfl) -> 
+      if lock_focus then
+	Nested(Proof_instr (false,instr),spfl)
+      else
+	anomaly "already marked as done"
+  | _ -> anomaly "mark_rule_as_done"
+
+let mark_proof_tree_as_done pt =
+  match pt.ref with
+      None -> anomaly "mark_proof_tree_as_done"
+    | Some (r,spfl) -> 
+	{pt with ref= Some (mark_rule_as_done r,spfl)}
+
+let mark_as_done pts = 
+  map_pftreestate 
+    (fun _ -> mark_proof_tree_as_done) 
+    (traverse 0 pts) 
+
+(* post-instruction focus management *)
+
+let goto_current_focus pts = up_until_matching_rule is_focussing_command pts
+
+let goto_current_focus_or_top pts = 
+  try 
+    up_until_matching_rule is_focussing_command pts
+  with Not_found -> top_of_tree pts
+
+(* return *)
+
+let close_tactic_mode pts =
+    let pts1=  
+      try goto_current_focus pts 
+      with Not_found -> 
+	error "\"return\" cannot be used outside of Declarative Proof Mode" in
+    let pts2 = daimon_subtree pts1 in
+    let pts3 = mark_as_done pts2 in 
+      goto_current_focus pts3 
+	  
+let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode
+
+(* end proof/claim *)
+
+let close_block bt pts =
+  let stack =
+    if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then
+      get_top_stack pts
+    else
+      get_stack pts in
+    match bt,stack with
+	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> 
+	  daimon_subtree (goto_current_focus pts)
+      | _, Claim::_ -> 
+	  error "\"end claim\" expected" 
+      | _, Focus_claim::_ -> 
+	  error "\"end focus\" expected" 
+      | _, [] ->
+ 	  error "\"end proof\" expected" 
+      | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
+	  begin
+	    match et with
+		ET_Case_analysis -> error "\"end cases\" expected"
+	      | ET_Induction ->  error "\"end induction\" expected"
+	  end
+      | _,_ -> anomaly "lonely suppose on stack"
+
+(* utility for suppose / suppose it is *)
+
+let close_previous_case pts = 
+  if 
+    Proof_trees.is_complete_proof (proof_of_pftreestate pts) 
+  then
+    match get_top_stack pts with
+	Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..."  
+      | Suppose_case :: Per (et,_,_,_) :: _ -> 
+	  goto_current_focus (mark_as_done pts)
+      | _ -> error "Not inside a proof per cases or induction."   
+  else
+    match get_stack pts with
+	Per (et,_,_,_) :: _ -> pts 
+      | Suppose_case :: Per (et,_,_,_) :: _ ->
+	  goto_current_focus (mark_as_done (daimon_subtree pts))
+      | _ -> error "Not inside a proof per cases or induction."
+
+(* Proof instructions *)
+
+(* automation *)
+
+let filter_hyps f gls =
+  let filter_aux (id,_,_) = 
+    if f id then 
+      tclIDTAC
+    else 
+      tclTRY (clear [id])  in
+    tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls
+
+let local_hyp_prefix = id_of_string "___"
+
+let add_justification_hyps keep items gls =
+  let add_aux c gls=
+    match kind_of_term c with 
+	Var id -> 
+	  keep:=Idset.add id !keep;
+	  tclIDTAC gls 
+      | _ -> 
+	  let id=pf_get_new_id local_hyp_prefix gls in 
+	    keep:=Idset.add id !keep; 
+	    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 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
+
+let my_automation_tac = ref 
+  (fun gls -> anomaly "No automation registered")
+
+let register_automation_tac tac = my_automation_tac:= tac
+
+let automation_tac gls = !my_automation_tac gls
+
+let justification tac gls= 
+    tclORELSE 
+      (tclSOLVE [tac]) 
+      (fun gls -> 
+	 if get_strictness () then 
+	   error "insufficient justification" 
+	 else
+	   begin
+	     msgnl (str "Warning: insufficient justification");  
+	     daimon_tac gls
+	   end) gls
+
+let default_justification items gls=
+  justification (apply_to_prepared_goal items automation_tac) gls
+
+(* code for have/then/thus/hence *)
+
+type stackd_elt =
+{se_meta:metavariable;
+ se_type:types;
+ se_last_meta:metavariable;
+ se_meta_list:(metavariable*types) list;
+ se_evd: evar_defs}
+
+let rec replace_in_list m l = function
+    [] -> raise Not_found
+  | c::q -> if m=fst c then l@q else c::replace_in_list m l q
+
+let enstack_subsubgoals env se stack gls=
+  let hd,params = decompose_app (special_whd gls se.se_type) in
+    match kind_of_term hd with
+	Ind ind when is_good_inductive env ind ->
+	  let mib,oib=
+	    Inductive.lookup_mind_specif env ind in
+          let gentypes=
+            Inductive.arities_of_constructors ind (mib,oib) in
+	  let process i gentyp = 
+	    let constructor = mkConstruct(ind,succ i) 
+	      (* constructors numbering*) in
+	    let appterm = applist (constructor,params) in
+	    let apptype = Term.prod_applist gentyp params in
+	    let rc,_ = Reduction.dest_prod env apptype in
+	    let rec meta_aux last lenv = function 
+		[] -> (last,lenv,[])
+	      | (nam,_,typ)::q ->
+		  let nlast=succ last in
+		  let (llast,holes,metas) =
+		    meta_aux nlast (mkMeta nlast :: lenv) q in
+		    (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
+	    let (nlast,holes,nmetas) = 
+		meta_aux se.se_last_meta [] (List.rev rc) in
+	    let refiner = applist (appterm,List.rev holes) in
+	    let evd = meta_assign se.se_meta refiner se.se_evd in
+	    let ncreated = replace_in_list 
+	      se.se_meta nmetas se.se_meta_list in
+	    let evd0 = List.fold_left 
+	      (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in  
+	      List.iter (fun (m,typ) -> 
+			   Stack.push 
+			     {se_meta=m;
+			      se_type=typ;
+			      se_evd=evd0;
+			      se_meta_list=ncreated;
+			      se_last_meta=nlast} stack) (List.rev nmetas) 
+	  in
+	    Array.iteri process gentypes
+      | _ -> ()
+
+let find_subsubgoal env c ctyp skip evd metas gls =
+  let stack = Stack.create () in
+  let max_meta = 
+    List.fold_left (fun a (m,_) -> max a m) 0 metas in
+  let _ = 
+    List.iter (fun (m,typ) -> 
+		 Stack.push 
+		   {se_meta=m;
+		    se_type=typ;
+		    se_last_meta=max_meta;
+		    se_meta_list=metas;
+		    se_evd=evd} stack) (List.rev metas) in
+  let rec dfs n = 
+    let se = Stack.pop stack in
+      try 
+	let unifier = 
+	  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}	  
+	  else
+	      dfs (pred n)
+      with _ -> 
+	begin
+	  enstack_subsubgoals env se stack gls;
+	  dfs n
+	end in
+  let nse= try dfs skip with Stack.Empty -> raise Not_found in
+    nse.se_meta_list,nse.se_evd
+
+let rec nf_list evd = 
+  function
+      [] -> []  
+    | (m,typ)::others -> 
+	if meta_defined evd m then 
+	    nf_list evd others
+	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
+       	begin
+	  meta_one:= Some c;
+          mkMeta 1
+	end
+     else
+       try
+	 map_constr (max_linear_context meta_one) c
+       with Not_found -> 
+	 begin
+	   meta_one:= Some c;
+           mkMeta 1
+	 end
+  else   
+    if isMeta c then 
+      raise Not_found
+    else
+      map_constr (max_linear_context meta_one) c
+
+let thus_tac c ctyp gls =  
+  let info = get_its_info gls in
+  let evd0 = mk_evd info.pm_subgoals gls in
+  let list,evd = 
+    try
+      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls
+    with Not_found -> 
+      error "I could not relate this statement to the thesis" in
+  let nflist = nf_list evd list in
+  let nfgoal = nf_meta evd info.pm_partial_goal in
+(*  let _ = msgnl (str "Partial goal : " ++ 
+		   print_constr_env (pf_env gls) nfgoal) in *)
+  let rgl = ref None in
+  let refiner = max_linear_context rgl nfgoal in
+    match !rgl with
+	None -> exact_check refiner gls
+      | Some pgl when not (isMeta refiner) ->
+	  let ninfo={info with
+		       pm_partial_goal = pgl;
+		       pm_subgoals = nflist} in
+	    tclTHEN
+	      (Tactics.refine refiner)
+	      (tcl_change_info ninfo) 
+	      gls
+      | _ -> 
+	  let ninfo={info with
+		       pm_partial_goal = nfgoal;
+		       pm_subgoals = nflist} in
+	    tcl_change_info ninfo gls
+
+let anon_id_base = id_of_string "__" 
+
+
+let mk_stat_or_thesis info = function  
+    This c -> c
+  | Thesis (For _ ) -> 
+      error "\"thesis for ...\" is not applicable here" 
+  | Thesis (Sub n) ->
+      begin
+	try List.assoc n info.pm_subgoals 
+	with Not_found -> error "No such part in thesis."
+      end
+  | Thesis Plain ->   
+      match info.pm_subgoals with
+	  [_,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 = 
+    match cut.cut_by with
+        Automated l ->	
+	  let elems = 
+	    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 
+      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
+  let thus_tac gls= 
+    if _thus then 
+      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
+
+(* iterated equality *)
+let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+
+let decompose_eq id gls =
+  let typ = pf_get_hyp_typ gls id in
+  let whd =  (special_whd gls typ) in
+    match kind_of_term whd with
+	App (f,args)->
+	  if eq_constr f _eq && (Array.length args)=3 
+	  then (args.(0),
+		args.(1), 
+		args.(2)) 
+	  else error "previous step is not an equality"
+      | _ -> error "previous step is not an equality"
+	  
+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
+  let typ,lhs,rhs = decompose_eq last_id gls0 in  
+  let just_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 
+      Anonymous -> 
+	pf_get_new_id (id_of_string "_eq") gls0 
+    | Name id -> id in
+  let ninfo = {info with pm_last=Name c_id} in
+  let thus_tac new_eq gls= 
+    if _thus then 
+      thus_tac (mkVar c_id) new_eq gls
+    else tclIDTAC gls in
+    match rew_side with 
+	Lhs ->
+	  let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
+	    tclTHENS (internal_cut c_id new_eq) 
+	      [tclTHEN tcl_erase_info 
+		 (tclTHENS (transitivity lhs) 
+		    [just_tac;exact_check (mkVar last_id)]);
+	       tclTHEN (tcl_change_info ninfo) (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
+	      
+
+
+(* tactics for claim/focus *)
+
+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 thus_tac gls= 
+    if _thus then 
+      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
+
+(* tactics for assume *)
+
+let reset_concl gls =
+  let info = get_its_info gls in
+    tcl_change_info 
+      {info with 
+	 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
+    match info.pm_subgoals with
+	[(_,typ)] -> 
+	  tclTHEN (intro_mustbe_force id) reset_concl gls
+      | _ -> error "Goal is split"
+
+let push_intro_tac coerce nam gls = 
+      let hid =
+	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
+	tclTHENLIST 
+	  [intro_pm hid;
+	   coerce hid;
+	   mark_id]
+	  gls 
+
+let assume_tac hyps gls = 
+  List.fold_right 
+    (fun (Hvar st | Hprop st) -> 
+       tclTHEN 
+	 (push_intro_tac 
+	    (fun id -> 
+	       convert_hyp (id,None,st.st_it)) st.st_label))
+	 hyps tclIDTAC gls 
+
+let assume_hyps_or_theses hyps gls = 
+  List.fold_right 
+    (function 
+	 (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> 
+	   tclTHEN 
+	     (push_intro_tac 
+		(fun id -> 
+		   convert_hyp (id,None,c)) nam)
+       | Hprop {st_label=nam;st_it=Thesis (tk)} -> 
+	   tclTHEN 
+	     (push_intro_tac 
+		(fun id -> tclIDTAC) nam))
+    hyps tclIDTAC gls 
+
+let assume_st hyps gls = 
+  List.fold_right 
+    (fun st -> 
+       tclTHEN 
+	 (push_intro_tac 
+	    (fun id -> convert_hyp (id,None,st.st_it)) st.st_label))
+	 hyps tclIDTAC gls 
+
+let assume_st_letin hyps gls = 
+  List.fold_right 
+    (fun st -> 
+       tclTHEN 
+	 (push_intro_tac 
+	    (fun id -> 
+	       convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
+	 hyps tclIDTAC gls 
+
+(* tactics for consider/given *)
+
+let update_goal_info gls =
+  let info = get_its_info gls in
+    match info.pm_subgoals with
+	[m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls
+      | _ -> error "thesis is split"
+
+let conjunction_arity id gls =
+  let typ = pf_get_hyp_typ gls id  in
+  let hd,params = decompose_app (special_whd gls typ) in
+  let env =pf_env gls in 
+    match kind_of_term hd with
+	Ind ind when is_good_inductive env ind ->
+	  let mib,oib=
+	    Inductive.lookup_mind_specif env ind in
+          let gentypes=
+            Inductive.arities_of_constructors ind (mib,oib) in
+	  let _ = if Array.length gentypes <> 1 then raise Not_found in
+	  let apptype = Term.prod_applist gentypes.(0) params in
+	  let rc,_ = Reduction.dest_prod env apptype in
+	    List.length rc
+      | _ -> raise Not_found
+
+let rec intron_then n ids ltac gls = 
+  if n<=0 then 
+    tclTHEN
+    (fun gls -> 
+       if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids  then 
+	 update_goal_info gls
+       else 
+	 tclIDTAC gls)
+    (ltac ids)
+      gls
+  else  
+    let id = pf_get_new_id (id_of_string "_tmp") gls in 
+      tclTHEN 
+	(intro_mustbe_force id) 
+	(intron_then (pred n) (id::ids) ltac) gls 
+
+let pm_rename_hyp id hid gls =
+  if occur_id [] id (pf_concl gls) then
+    tclTHEN (rename_hyp id hid) update_goal_info gls
+  else
+    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 -> 
+	if may_intro then
+	  begin
+ 	    let id = pf_get_new_id (id_of_string "_tmp") gls in
+	      tclIFTHENELSE 
+		(intro_pm id)
+		(consider_match true [] [id] hyps) 
+		(fun _ -> 
+		   error "not enough sub-hypotheses to match statements")
+		gls 
+          end
+	else
+	  error "not enough sub-hypotheses to match statements" 
+	    (* should tell which ones *)
+    | id::rest_ids,(Hvar st | Hprop st)::rest ->
+	tclIFTHENELSE (convert_hyp (id,None,st.st_it))
+	  begin
+	    match st.st_label with 
+		Anonymous -> 
+		  consider_match may_intro (id::introduced) rest_ids rest
+	      | Name hid -> 
+		  tclTHENLIST 
+		    [pm_rename_hyp id hid;
+		     consider_match may_intro (hid::introduced) rest_ids rest]
+	  end
+	  begin
+	    (fun gls -> 
+	       let nhyps =
+		 try conjunction_arity id gls with 
+		     Not_found -> error "matching hypothesis not found" in 
+		 tclTHENLIST 
+		   [general_case_analysis (mkVar id,NoBindings);
+		    intron_then nhyps []
+		      (fun l -> consider_match may_intro introduced 
+			 (List.rev_append l rest_ids) expected)] gls)
+	  end
+	  gls
+	  
+let consider_tac c hyps gls =
+  match kind_of_term (strip_outer_cast c) with
+      Var id ->
+	consider_match false [] [id] hyps gls 
+    | _ -> 
+	let id = pf_get_new_id (id_of_string "_tmp") gls in
+	tclTHEN 
+	  (forward None (Genarg.IntroIdentifier id) c)
+ 	  (consider_match false [] [id] hyps) gls 
+	  
+
+let given_tac hyps gls =
+  consider_match true [] [] hyps gls
+
+(* tactics for take *)
+
+let rec take_tac wits gls =
+  match wits with
+      [] -> tclIDTAC gls
+    | wit::rest ->  
+	let typ = pf_type_of gls wit in  
+	  tclTHEN (thus_tac wit typ) (take_tac rest)  gls
+
+
+(* tactics for define *)
+
+let rec build_function args body =
+  match args with 
+      st::rest -> 
+	let pfun= lift 1 (build_function rest body) in
+	let id = match st.st_label with
+	    Anonymous -> assert false
+	  | Name id -> id in
+	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
+    | [] -> body 
+
+let define_tac id args body gls =
+  let t = build_function args body in
+    letin_tac true (Name id) t Tacexpr.nowhere gls
+
+(* tactics for reconsider *)
+
+let cast_tac id_or_thesis typ gls = 
+  let info = get_its_info gls in
+  match id_or_thesis with
+      This id ->
+	let (_,body,_) = pf_get_hyp gls id in
+	  convert_hyp (id,body,typ) gls
+    | Thesis (For _ ) -> 
+	error "\"thesis for ...\" is not applicable here" 
+    | Thesis (Sub n) ->
+	begin
+	  let old_typ = 
+	    try List.assoc n info.pm_subgoals 
+	    with Not_found -> error "No such part in thesis." in
+	  if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then
+	    let new_sg = List.merge  
+	      (fun (n,_) (p,_) -> Pervasives.compare n p) 
+	      [n,typ] (List.remove_assoc n info.pm_subgoals) in
+	      tcl_change_info {info with pm_subgoals=new_sg} gls
+	  else 
+	    error "not convertible"
+	end
+    | Thesis Plain ->   
+	match info.pm_subgoals with 
+	    [m,c] -> 
+	      tclTHEN 
+		(convert_concl typ DEFAULTcast) 
+	        (tcl_change_info {info with pm_subgoals= [m,typ]}) gls
+	  | _ -> error 
+	      "\"thesis\" is split, please specify which part you refer to."
+  
+      
+(* per cases *)
+
+let start_tree env ind = 
+  let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in
+    Split (Idset.empty,ind,Array.map (fun _ -> None) constrs)
+
+let build_per_info etype casee gls = 
+  let concl=get_thesis gls in
+  let env=pf_env gls in
+  let ctyp=pf_type_of gls casee in
+  let is_dep = dependent casee concl in 
+  let hd,args = decompose_app (special_whd gls ctyp) in
+  let ind = 
+    try
+      destInd hd 
+    with _ -> 
+      error "Case analysis must be done on an inductive object" in
+  let nparams =
+    let mind = fst (Global.lookup_inductive ind) in
+     match etype with
+	 ET_Induction -> mind.mind_nparams_rec
+       | _ -> mind.mind_nparams in
+  let params,real_args = list_chop nparams args in
+  let abstract_obj body c = 
+    let typ=pf_type_of gls c in 
+      lambda_create env (typ,subst_term c body) in
+  let pred= List.fold_left abstract_obj    
+    (lambda_create env (ctyp,subst_term casee concl)) real_args in
+    is_dep,
+  {per_casee=casee;
+   per_ctype=ctyp;
+   per_ind=ind;
+   per_pred=pred;
+   per_args=real_args;
+   per_params=params;
+   per_nparams=nparams}
+
+let per_tac etype casee gls=
+  let env=pf_env gls in
+  let info = get_its_info gls in
+    match casee with
+	Real c ->
+	  let is_dep,per_info = build_per_info etype c gls in
+	  let ek = 
+	    if is_dep then
+	      EK_dep (start_tree env per_info.per_ind)
+	    else EK_unknown in
+	    tcl_change_info 
+	      {info with 
+		 pm_stack=
+		  Per(etype,per_info,ek,[])::info.pm_stack} gls
+      | Virtual cut ->
+	  assert (cut.cut_stat.st_label=Anonymous);
+	  let id = pf_get_new_id (id_of_string "_matched") gls in
+	  let c = mkVar id in
+	  let modified_cut = 
+	    {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
+	    tclTHEN 
+	      (instr_cut (fun _ c -> c) false false modified_cut)
+	      (fun gls0 ->
+		 let is_dep,per_info = build_per_info etype c gls0 in
+		   assert (not is_dep);
+		   tcl_change_info 
+		     {info with pm_stack=
+			 Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
+	      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
+	match ek with
+	    EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
+	  | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
+	  | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"."
+      end
+  | _ -> anomaly "wrong stack state"
+
+let suppose_tac hyps gls0 = 
+  let info = get_its_info gls0 in
+  let thesis = get_thesis gls0 in
+  let id = pf_get_new_id (id_of_string "_subcase") gls0 in
+  let clause = build_product hyps thesis in
+  let ninfo1 = {info with 
+		  pm_stack=Suppose_case::info.pm_stack;
+		  pm_partial_goal=mkMeta 1;
+		  pm_subgoals = [1,clause]} in
+  let old_clauses,stack = register_nodep_subcase id info.pm_stack in
+  let ninfo2 = {info with 
+		  pm_stack=stack} in
+    tclTHENS (internal_cut id clause) 
+      [tclTHENLIST [tcl_change_info ninfo1;
+		    assume_tac hyps;
+		    clear old_clauses];
+       tcl_change_info ninfo2] gls0
+
+(* suppose it is ... *) 
+
+(* pattern matching compiling *)
+
+let rec nb_prod_after n c=
+  match kind_of_term c with
+    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
+	1+(nb_prod_after 0 b)
+    | _ -> 0
+
+let constructor_arities env ind =
+  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+  let constr_types = Inductiveops.arities_of_constructors env ind in 
+  let hyp = nb_prod_after nparams in	
+    Array.map hyp constr_types
+
+let rec n_push rest ids n = 
+  if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) 
+
+let explode_branches ids env ind rest=
+  Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind)
+
+let rec tree_of_pats env ((id,_) as cpl) pats =
+  match pats with 
+      [] -> End_of_branch cpl
+    | args::stack ->
+	match args with
+	    [] -> Pop (tree_of_pats env cpl stack)
+	  | patt :: rest_args ->
+	      match patt with
+		  PatVar (_,v) -> 
+		    Push (Idset.singleton id,
+			  tree_of_pats env cpl (rest_args::stack))
+		|  PatCstr (_,(ind,cnum),args,nam) ->
+		     let _,mind = Inductive.lookup_mind_specif env ind in
+		     let br= Array.map (fun _ -> None) mind.mind_consnames in
+		       br.(pred cnum) <- 
+			 Some (Idset.singleton id,
+			       tree_of_pats env cpl (args::rest_args::stack));
+		       Split(Idset.empty,ind,br)
+
+let rec add_branch env ((id,_) as cpl) pats tree=
+  match pats with 
+      [] -> 
+	begin
+	  match tree with
+	      End_of_branch cpl0 -> End_of_branch cpl0 
+		(* this ensures precedence *) 
+	    | _ -> anomaly "tree is expected to end here"
+	end
+    | args::stack ->
+	match args with 
+	    [] ->
+	      begin
+		match tree with 
+		    Pop t -> Pop (add_branch env cpl stack t)
+		  | _ -> anomaly "we should pop here" 
+	      end
+	  | patt :: rest_args ->
+	      match patt with
+		  PatVar (_,v) ->
+		    begin
+		      match tree with 
+			  Push (ids,t) -> 
+			    Push (Idset.add id ids,
+				  add_branch env cpl (rest_args::stack) t)
+			| Split (ids,ind,br) ->
+			    Split (Idset.add id ids,
+				   ind,array_map2 
+				     (append_branch env cpl 1 
+					(rest_args::stack)) 
+				     (constructor_arities env ind) br)
+			| _ -> anomaly "No pop/stop expected here"  
+		    end
+		| PatCstr (_,(ind,cnum),args,nam) ->
+		    match tree with
+			Push (ids,t) ->
+			  let br = explode_branches ids env ind t in
+			  let _ =
+			    br.(pred cnum)<- 
+			      option_map
+			      (fun (ids,tree) -> 
+				 Idset.add id ids,
+				 add_branch env cpl 
+				   (args::rest_args::stack) tree) 
+			      br.(pred cnum) in
+			    Split (ids,ind,br)
+		      | Split (ids,ind0,br0) ->
+			  assert (ind=ind0);
+			  let br=Array.copy br0 in
+			  let ca = constructor_arities env ind in
+			  let _= br.(pred cnum)<-
+			    append_branch env cpl 0 (args::rest_args::stack) 
+			    ca.(pred cnum) br.(pred cnum) in 
+			    Split (ids,ind,br)
+		      | _ -> anomaly "No pop/stop expected here"
+and append_branch env ((id,_) as cpl) depth pats nargs = function
+    Some (ids,tree) -> 
+      Some (Idset.add id ids,append_tree env cpl depth pats tree)
+  | None ->
+      Some (* (n_push (tree_of_pats env cpl pats) 
+	      (Idset.singleton id) nargs) *)
+	   (Idset.singleton id,tree_of_pats env cpl pats)
+and append_tree env ((id,_) as cpl) depth pats tree =
+  if depth<=0 then add_branch env cpl pats tree
+  else match tree with
+      Pop t -> Pop (append_tree env cpl (pred depth) pats t)
+    | Push (ids,t) -> Push (Idset.add id ids,
+				   append_tree env cpl depth pats t)
+    | End_of_branch _ -> anomaly "Premature end of branch"
+    | Split (ids,ind,branches) -> 
+	Split (Idset.add id ids,ind,
+	       array_map2 
+		 (append_branch env cpl (succ depth) pats) 
+		 (constructor_arities env ind)
+		 branches)
+
+(* suppose it is *)
+
+let rec st_assoc id = function
+    [] -> raise Not_found
+  | st::_ when st.st_label = id  -> st.st_it
+  | _ :: rest -> st_assoc id rest
+
+let thesis_for obj typ per_info env=
+  let rc,hd1=decompose_prod typ in
+  let cind,all_args=decompose_app typ in
+  let ind = destInd cind in
+  let _ = if ind <> per_info.per_ind then
+    errorlabstrm "thesis_for" 
+      ((Printer.pr_constr_env env obj) ++ spc () ++ 
+	 str "cannot give an induction hypothesis (wrong inductive type)") in  
+  let params,args = list_chop per_info.per_nparams all_args in
+  let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
+    errorlabstrm "thesis_for" 
+      ((Printer.pr_constr_env env obj) ++ spc () ++ 
+	 str "cannot give an induction hypothesis (wrong parameters)") in
+  let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
+    compose_prod rc (whd_beta hd2)
+
+let rec build_product_dep pat_info per_info args body gls =
+  match args with 
+      (Hprop {st_label=nam;st_it=This c} 
+      | Hvar {st_label=nam;st_it=c})::rest -> 
+	let pprod= 
+	  lift 1 (build_product_dep pat_info per_info rest body gls) in
+	let lbody =
+	  match nam with
+	      Anonymous -> body
+	    | Name id -> subst_var id pprod in
+	  mkProd (nam,c,lbody)
+    | Hprop ({st_it=Thesis tk} as st)::rest ->
+	let pprod= 
+	  lift 1 (build_product_dep pat_info per_info rest body gls) in
+	let lbody =
+	  match st.st_label with
+	      Anonymous -> body
+	    | Name id -> subst_var id pprod in
+	let ptyp =
+	  match tk with
+	      For id ->
+		let obj = mkVar id in
+		let typ = 
+		  try st_assoc (Name id) pat_info.pat_vars 
+		  with Not_found -> 
+		    snd (st_assoc (Name id) pat_info.pat_aliases) in
+		  thesis_for obj typ per_info (pf_env gls)
+	    | Plain -> get_thesis gls 
+	    | Sub n -> anomaly "Subthesis in cases" in
+	  mkProd (st.st_label,ptyp,lbody)
+    | [] -> body 
+
+let build_dep_clause params pat_info per_info hyps gls =
+  let concl=
+    thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in
+  let open_clause =
+    build_product_dep pat_info per_info hyps concl gls in
+  let prod_one st body =
+    match st.st_label with
+	Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body)
+      | Name id -> mkNamedProd id st.st_it (lift 1 body) in
+  let let_one_in st body =
+    match st.st_label with
+	Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body)
+      | Name id -> 
+	  mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in
+  let aliased_clause = 
+    List.fold_right let_one_in pat_info.pat_aliases open_clause in
+    List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause
+
+let rec register_dep_subcase id env per_info pat = function
+    EK_nodep -> error  "Only \"suppose it is\" can be used here."
+  | EK_unknown -> 
+      register_dep_subcase id env per_info pat
+	(EK_dep (start_tree env per_info.per_ind))
+  | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree)
+  
+let case_tac params pat_info hyps gls0 =
+  let info = get_its_info gls0 in
+  let id = pf_get_new_id (id_of_string "_subcase") gls0 in
+  let et,per_info,ek,old_clauses,rest =
+    match info.pm_stack with
+	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) 
+      | _ -> anomaly "wrong place for cases" in
+  let clause = build_dep_clause params pat_info per_info hyps gls0 in
+  let ninfo1 = {info with 
+		  pm_stack=Suppose_case::info.pm_stack;
+		  pm_partial_goal=mkMeta 1;
+		  pm_subgoals = [1,clause]} in
+  let nek = 
+    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info 
+      pat_info.pat_pat ek in  
+  let ninfo2 = {info with 
+		  pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
+    tclTHENS (internal_cut id clause) 
+      [tclTHENLIST 
+	 [tcl_change_info ninfo1; 
+	  assume_st (params@pat_info.pat_vars);
+	  assume_st_letin pat_info.pat_aliases;
+	  assume_hyps_or_theses hyps;
+	  clear old_clauses];
+       tcl_change_info ninfo2] gls0
+
+(* end cases *)
+
+type instance_stack =
+    (constr option*bool*(constr list) list) list
+
+let initial_instance_stack ids =
+  List.map (fun id -> id,[None,false,[]]) ids
+
+let push_one_arg arg = function 
+    [] -> anomaly "impossible"
+  | (head,is_rec,args) :: ctx -> 
+      ((head,is_rec,(arg::args)) :: ctx)
+
+let push_arg arg stacks =
+  List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks
+  
+
+let push_one_head c is_rec ids (id,stack) = 
+  let head = if Idset.mem id ids then Some c else None in
+    id,(head,is_rec,[]) :: stack
+
+let push_head c is_rec ids stacks =
+  List.map (push_one_head c is_rec ids) stacks
+
+let pop_one rec_flag (id,stack) =  
+  let nstack=
+    match stack with
+	[] -> anomaly "impossible"
+      | [c] as l -> l
+      | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx ->
+	  let arg = applist (head,(List.rev args)) in
+	    rec_flag:= !rec_flag || is_rec;
+	    (head0,is_rec0,(arg::args0))::ctx
+     | (None,is_rec,args)::(head0,is_rec0,args0)::ctx ->
+	 rec_flag:= !rec_flag || is_rec;
+	 (head0,is_rec0,(args@args0))::ctx
+  in id,nstack
+
+let pop_stacks stacks =
+  let rec_flag= ref false in 
+  let nstacks = List.map (pop_one rec_flag) stacks in
+    !rec_flag , nstacks
+
+let patvar_base = id_of_string "__"
+
+let test_fun (str:string) = ()
+
+let hrec_for obj_id fix_id per_info gls=
+  let obj=mkVar obj_id in
+  let typ=pf_get_hyp_typ gls obj_id in
+  let rc,hd1=decompose_prod typ in
+  let cind,all_args=decompose_app typ in
+    match kind_of_term cind with
+	Ind ind when ind=per_info.per_ind ->
+	  let params,args= list_chop per_info.per_nparams all_args in 
+	    if try 
+	      (List.for_all2 eq_constr params per_info.per_params)
+	    with Invalid_argument _ -> false then
+	      let hd2 = applist (mkVar fix_id,args@[obj]) in
+		Some (compose_lam rc (whd_beta hd2))
+	    else None
+      | _ -> None
+
+let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
+  match tree with
+      Pop t ->  
+	let is_rec,nstacks =  pop_stacks stacks in
+	  if is_rec then
+	    let _ = test_fun "is_rec=true" in
+	     let c_id = pf_get_new_id (id_of_string "_hrec") gls in
+	       tclTHEN 
+		 (intro_mustbe_force c_id)
+		 (execute_cases false fix_name per_info kont0 nstacks t) gls
+	  else
+	    execute_cases false fix_name per_info kont0 nstacks t gls
+    | Push (_,t) -> 
+	let id = pf_get_new_id patvar_base gls in
+	let nstacks = push_arg (mkVar id) stacks in
+	let kont = execute_cases false fix_name per_info kont0 nstacks t in
+	  tclTHEN
+	    (intro_mustbe_force id)
+	    begin
+	      match fix_name with
+		  Anonymous -> kont
+		| Name fix_id ->  
+		    (fun gls -> 
+		       if at_top then
+			 kont gls
+		       else
+			 match hrec_for id fix_id per_info gls with
+			     None -> kont gls
+			   | Some c_obj ->
+			       let c_id = 
+				 pf_get_new_id (id_of_string "_hrec") gls in
+				 tclTHENLIST 
+				   [generalize [c_obj];
+				    intro_mustbe_force c_id;
+				    kont] gls)
+	    end gls
+    | Split(ids,ind,br) ->
+	let (_,typ,_)=destProd (pf_concl gls) in
+	let hd,args=decompose_app (special_whd gls typ) in
+	let _ = assert (ind = destInd hd) in
+	let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+	let params = list_firstn nparams args in
+	let constr i =applist (mkConstruct(ind,succ i),params) in
+	let next_tac is_rec i = function
+	    Some (sub_ids,tree) ->
+	      let br_stacks =
+		List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in
+	      let p_stacks = 
+		push_head (constr i) is_rec ids br_stacks in
+		execute_cases false fix_name per_info kont0 p_stacks tree 
+	  | None -> 
+	      msgnl (str "Warning : missing case");
+	      kont0 (mkMeta 1) 
+	in
+	let id = pf_get_new_id patvar_base gls in
+	let kont is_rec = 			
+	  tclTHENSV
+	    (general_case_analysis (mkVar id,NoBindings))
+	    (Array.mapi (next_tac is_rec) br) in
+	  tclTHEN 
+	    (intro_mustbe_force id)
+	    begin
+	      match fix_name with
+		  Anonymous -> kont false
+		| Name fix_id ->  
+		    (fun gls -> 
+		       if at_top then
+			 kont false gls
+		       else
+			 match hrec_for id fix_id per_info gls with
+			     None -> kont false gls
+			   | Some c_obj ->
+			       tclTHENLIST 
+				 [generalize [c_obj];
+				  kont true] gls)
+	    end gls
+    | End_of_branch (id,nhyps) -> 
+	  match List.assoc id stacks with
+	      [None,_,args] -> 
+		let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+		  kont0 (applist (mkVar id,List.rev_append args metas)) gls
+	    | _ -> anomaly "wrong stack size"
+
+let end_tac et2 gls =
+  let info = get_its_info gls in
+  let et1,pi,ek,clauses = 
+    match info.pm_stack with
+	Suppose_case::_ -> 
+	  anomaly "This case should already be trapped"
+      | Claim::_ ->  
+	  error "\"end claim\" expected."
+      | Focus_claim::_ ->
+	  error "\"end focus\" expected."
+      | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) 
+      | [] -> 
+	  anomaly "This case should already be trapped" in
+  let et = 
+    if et1 <> et2 then
+      match et1 with 
+	  ET_Case_analysis -> 
+	    error "\"end cases\" expected."
+	| ET_Induction ->
+	    error "\"end induction\" expected."
+    else et1 in
+    tclTHEN 
+      tcl_erase_info
+      begin
+	match et,ek with
+	    _,EK_unknown -> 
+	      tclSOLVE [simplest_elim pi.per_casee]	
+	  | ET_Case_analysis,EK_nodep ->
+	      tclTHEN 
+		(general_case_analysis (pi.per_casee,NoBindings))
+		(default_justification (List.map mkVar clauses))
+	  | ET_Induction,EK_nodep ->
+	      tclTHENLIST
+		[generalize (pi.per_args@[pi.per_casee]); 
+		 simple_induct (AnonHyp (succ (List.length pi.per_args)));
+		 default_justification (List.map mkVar clauses)]
+	  | ET_Case_analysis,EK_dep tree ->
+	      tclTHENLIST 
+		[generalize (pi.per_args@[pi.per_casee]);
+		 execute_cases true Anonymous pi 
+		   (fun c -> tclTHENLIST 
+		      [refine c;
+		       clear clauses;
+		       justification assumption])
+		   (initial_instance_stack clauses) tree]	
+	  | ET_Induction,EK_dep tree ->
+	      tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+		begin
+		  fun gls0 -> 
+		    let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in
+		      tclTHEN 
+			(fix (Some fix_id) (succ (List.length pi.per_args))) 
+			(execute_cases true (Name fix_id) pi 
+			   (fun c ->
+			      tclTHENLIST 
+				[clear [fix_id];
+				 refine c;
+				 clear clauses;
+				 justification assumption
+				 (* justification automation_tac *)])
+			   (initial_instance_stack clauses) tree) gls0
+		end	
+      end gls
+
+(* escape *)
+
+let rec abstract_metas n avoid head = function
+    [] -> 1,head,[]
+  | (meta,typ)::rest -> 
+      let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in
+      let p,term,args = abstract_metas (succ n) (id::avoid) head rest in 
+	succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term),
+      (mkMeta n)::args 
+
+let build_refining_context gls =
+  let info = get_its_info gls in
+  let avoid=pf_ids_of_hyps gls in
+  let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in
+    applist (fn,args)
+    
+let escape_command pts =
+  let pts1 = nth_unproven 1 pts in
+  let gls = top_goal_of_pftreestate pts1 in
+  let term = build_refining_context gls in
+  let tac = tclTHEN 
+    (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info)
+    (Tactics.refine term) in
+    traverse 1 (solve_pftreestate tac pts1)
+
+(* General instruction engine *)
+
+let rec do_proof_instr_gen _thus _then instr = 
+  match instr with 
+      Pthus i -> 
+	assert (not _thus);
+	do_proof_instr_gen true _then i
+    | Pthen i -> 	
+	assert (not _then);
+	do_proof_instr_gen _thus true i
+    | Phence i -> 
+	assert (not (_then || _thus));
+	do_proof_instr_gen true true i
+    | Pcut c ->
+	instr_cut mk_stat_or_thesis _thus _then c
+    | Prew (s,c) ->
+	assert (not _then);
+	instr_rew _thus s c
+    | Pconsider (c,hyps)    -> consider_tac c hyps
+    | Pgiven hyps            -> given_tac hyps
+    | Passume hyps           -> assume_tac hyps
+    | Plet hyps              -> assume_tac hyps
+    | Pclaim st              -> instr_claim false st 
+    | Pfocus st              -> instr_claim true st
+    | Ptake witl             -> take_tac witl
+    | Pdefine (id,args,body) -> define_tac id args body
+    | Pcast (id,typ)         -> cast_tac id typ 
+    | Pper (et,cs)           -> per_tac et cs 
+    | Psuppose hyps      -> suppose_tac hyps
+    | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
+    | Pend (B_elim et) -> end_tac et
+    | Pend _ | Pescape -> anomaly "Not applicable"
+ 
+let eval_instr {instr=instr} =
+  do_proof_instr_gen false false instr   
+
+let rec preprocess pts instr =
+  match instr with
+    Phence i |Pthus i | Pthen i -> preprocess pts i
+  | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
+  | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ 
+  | Pdefine (_,_,_) | Pper _ | Prew _ ->
+      check_not_per pts;
+      true,pts
+  | Pescape -> 
+      check_not_per pts;
+      false,pts
+  | Pcase _ | Psuppose _ | Pend (B_elim _) -> 
+      true,close_previous_case pts
+  | Pend bt -> 
+      false,close_block bt pts 
+      
+let rec postprocess pts instr = 
+  match instr with
+      Phence i | Pthus i | Pthen i -> postprocess pts i
+    | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
+    | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
+    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
+    | Pescape ->
+	escape_command pts
+    | Pend _ -> 
+	goto_current_focus_or_top (mark_as_done pts)
+
+let do_instr raw_instr pts =
+  let has_tactic,pts1 = preprocess pts raw_instr.instr in
+  let pts2 = 
+    if has_tactic then
+      let gl = nth_goal_of_pftreestate 1 pts1 in
+      let env=  pf_env gl in
+      let sigma= project gl in
+      let ist = {ltacvars = ([],[]); ltacrecvars = []; 
+		 gsigma = sigma; genv = env} in
+      let glob_instr = intern_proof_instr ist raw_instr in
+      let instr = 
+	interp_proof_instr (get_its_info gl) sigma env glob_instr in
+      let lock_focus = is_focussing_instr instr.instr in
+      let marker= Proof_instr (lock_focus,instr) in
+	solve_nth_pftreestate 1 
+	  (abstract_operation marker (eval_instr instr)) pts1
+    else pts1 in
+      postprocess pts2 raw_instr.instr
+
+let proof_instr raw_instr =
+  Pfedit.mutate (do_instr raw_instr)
+
+(*
+
+(* STUFF FOR ITERATED RELATIONS *)
+let decompose_bin_app t= 
+  let hd,args = destApp 
+
+let identify_transitivity_lemma c =
+  let varx,tx,c1 = destProd c in
+  let vary,ty,c2 = destProd (pop c1) in
+  let varz,tz,c3 = destProd (pop c2) in
+  let _,p1,c4 = destProd (pop c3) in
+  let _,lp2,lp3 = destProd (pop c4) in
+  let p2=pop lp2 in
+  let p3=pop lp3 in
+*)
+    
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
new file mode 100644
index 0000000000..ba8dc7b668
--- /dev/null
+++ b/tactics/decl_proof_instr.mli
@@ -0,0 +1,118 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Refiner
+open Names
+open Term
+open Tacmach
+
+val go_to_proof_mode: unit -> unit
+val return_from_tactic_mode: unit -> unit
+
+val register_automation_tac: tactic -> unit
+
+val automation_tac : tactic
+
+val daimon_subtree: pftreestate -> pftreestate
+
+val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate
+val proof_instr: Decl_expr.raw_proof_instr -> unit
+
+val tcl_change_info : Decl_mode.pm_info -> tactic
+
+val mark_proof_tree_as_done : Proof_type.proof_tree -> Proof_type.proof_tree
+
+val mark_as_done : pftreestate -> pftreestate
+
+val execute_cases : bool ->
+    Names.name ->
+    Decl_mode.per_info ->
+    (Term.constr -> Proof_type.tactic) ->
+    (Names.Idset.elt * (Term.constr option * bool * Term.constr list) list) 
+      list ->
+    Decl_mode.split_tree -> Proof_type.tactic
+
+val tree_of_pats :
+    Environ.env ->
+    Names.Idset.elt * int ->
+    Rawterm.cases_pattern list list -> Decl_mode.split_tree
+val add_branch :
+    Environ.env ->
+    Names.Idset.elt * int ->
+    Rawterm.cases_pattern list list ->
+    Decl_mode.split_tree -> Decl_mode.split_tree
+val append_branch :
+    Environ.env ->
+    Names.Idset.elt * int ->
+    int ->
+    Rawterm.cases_pattern list list ->
+    int ->
+    (Names.Idset.t * Decl_mode.split_tree) option ->
+    (Names.Idset.t * Decl_mode.split_tree) option
+
+val append_tree :   Environ.env ->
+    Names.Idset.elt * int ->
+    int ->
+    Rawterm.cases_pattern list list ->
+    Decl_mode.split_tree -> Decl_mode.split_tree
+
+val build_dep_clause :   Term.types Decl_expr.statement list ->
+    Decl_expr.proof_pattern ->
+    Decl_mode.per_info ->
+    (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis)
+    Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
+
+val register_dep_subcase :    
+    Names.identifier * int ->
+    Environ.env ->
+    Decl_mode.per_info ->
+    Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
+
+val thesis_for :     Term.constr ->
+    Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr
+
+val close_previous_case : pftreestate -> pftreestate
+
+val test_fun : string -> unit
+
+
+val pop_stacks :
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list ->
+  bool * 
+    (Names.identifier * 
+       (Term.constr option * bool * Term.constr list) list) list
+
+
+val push_head :   Term.constr ->
+  bool ->
+  Names.Idset.t ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list
+
+val push_arg : Term.constr ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list
+
+val hrec_for: 
+    Names.identifier ->
+    Names.identifier ->
+    Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> Term.constr option
+
+val consider_match :
+   bool ->
+    Names.Idset.elt list ->
+    Names.Idset.elt list ->
+    (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
+    Proof_type.tactic
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d01cd8ca25..6339ed5363 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -51,7 +51,7 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine (pf_env gl) ev rawc (create_evar_defs sigma)  in
+    let evd' = w_refine ev rawc (create_evar_defs sigma)  in
     Refiner.tclEVARS (evars_of evd') gl
 	
 (*
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e78731f57f..a0ff76968a 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     (str"Computed inversion goal was not closed in initial signature");
   *)
   let invSign = named_context_val invEnv in
-  let pfs = mk_pftreestate (mk_goal invSign invGoal) in
+  let pfs = mk_pftreestate (mk_goal invSign invGoal None) in
   let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
   let global_named_context = Global.named_context () in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index bccdd39439..fea10de7f8 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -84,6 +84,9 @@ val interp_genarg :
 val intern_genarg :
   glob_sign -> raw_generic_argument -> glob_generic_argument
 
+val intern_tactic : 
+  glob_sign -> raw_tactic_expr -> glob_tactic_expr
+
 val intern_constr :
   glob_sign -> constr_expr -> rawconstr_and_expr