Imported Upstream version 8.0pl1upstream/8.0pl1

21 files changed, 5794 insertions, 0 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
new file mode 100644
index 00000000..423350d7
--- /dev/null
+++ b/proofs/clenv.ml
@@ -0,0 +1,1175 @@
+(************************************************************************)
+(*  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: clenv.ml,v 1.97.2.3 2004/07/16 19:30:48 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Instantiate
+open Environ
+open Evd
+open Proof_type
+open Refiner
+open Proof_trees
+open Logic
+open Reductionops
+open Tacmach
+open Evar_refiner
+open Rawterm
+open Pattern
+open Tacexpr
+
+(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
+   gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
+
+let abstract_scheme env c l lname_typ =
+  List.fold_left2 
+    (fun t (locc,a) (na,_,ta) ->
+       let na = match kind_of_term a with Var id -> Name id | _ -> na in
+       if occur_meta ta then error "cannot find a type for the generalisation"
+       else if occur_meta a then lambda_name env (na,ta,t)
+       else lambda_name env (na,ta,subst_term_occ locc a t))
+    c
+    (List.rev l)
+    lname_typ
+
+let abstract_list_all env sigma typ c l =
+  let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in
+  let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in 
+  try 
+    if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p
+    else error "abstract_list_all"
+  with UserError _ ->
+    raise (RefinerError (CannotGeneralize typ))
+
+(* Generator of metavariables *)
+let new_meta =
+  let meta_ctr = ref 0 in
+  fun () -> incr meta_ctr; !meta_ctr
+
+(* replaces a mapping of existentials into a mapping of metas.
+   Problem if an evar appears in the type of another one (pops anomaly) *)
+let exist_to_meta sigma (emap, c) =
+  let metamap = ref [] in
+  let change_exist evar =
+    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+    let n = new_meta() in
+    metamap := (n, ty) :: !metamap;
+    mkMeta n in
+  let rec replace c =
+    match kind_of_term c with
+        Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
+      | _ -> map_constr replace c in
+  (!metamap, replace c)
+
+module Metaset = Intset
+
+module Metamap = Intmap
+
+let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false
+
+let metamap_in_dom x m =
+  try let _ = Metamap.find x m in true with Not_found -> false
+
+let metamap_to_list m =
+  Metamap.fold (fun n v l -> (n,v)::l) m []
+
+let metamap_inv m b = 
+  Metamap.fold (fun n v l -> if v = b then n::l else l) m []
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Metaset.t }
+
+(* collects all metavar occurences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c = 
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Meta mv -> mv::acc
+      | _         -> fold_constr collrec acc c
+  in
+  List.rev (collrec [] c)
+
+let metavars_of c =  
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Meta mv -> Metaset.add mv acc
+      | _         -> fold_constr collrec acc c
+  in 
+  collrec Metaset.empty c
+
+let mk_freelisted c =
+  { rebus = c; freemetas = metavars_of c }
+
+
+(* Clausal environments *)
+
+type clbinding = 
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Metamap.t;
+  env : clbinding Metamap.t;
+  hook : 'a }
+
+type wc = named_context sigma
+
+
+(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
+ * mv0, or if one of the free vars on mv1's freelist mentions
+ * mv0 *)
+
+let mentions clenv mv0 = 
+  let rec menrec mv1 =
+    try
+     (match Metamap.find mv1 clenv.env with
+	 | Clval (b,_) -> 
+	     Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas
+	 | Cltyp _ -> false)
+    with Not_found -> 
+      false
+  in 
+  menrec
+
+(* Creates a new clause-environment, whose template has a given
+ * type, CTY.  This is not all that useful, since not very often
+ * does one know the type of the clause - one usually only has
+ * a clause which one wants to backchain thru. *)
+
+let mk_clenv wc cty =
+  let mv = new_meta () in
+  let cty_fls = mk_freelisted cty in 
+  { templval = mk_freelisted (mkMeta mv);
+    templtyp = cty_fls;
+    namenv = Metamap.empty;
+    env =  Metamap.add mv (Cltyp cty_fls) Metamap.empty ;
+    hook = wc }
+  
+let clenv_environments bound c =
+  let rec clrec (ne,e,metas) n c =
+    match n, kind_of_term c with
+      | (Some 0, _) -> (ne, e, List.rev metas, c)
+      | (n, Cast (c,_)) -> clrec (ne,e,metas) n c
+      | (n, Prod (na,c1,c2)) ->
+	  let mv = new_meta () in
+	  let dep = dependent (mkRel 1) c2 in
+	  let ne' =
+	    if dep then
+              match na with
+		| Anonymous -> ne
+		| Name id ->
+		    if metamap_in_dom mv ne then begin
+		      warning ("Cannot put metavar "^(string_of_meta mv)^
+			       " in name-environment twice");
+		      ne
+		    end else 
+		      Metamap.add mv id ne
+            else 
+	      ne 
+	  in
+	  let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in 
+	  clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
+	    (if dep then (subst1 (mkMeta mv) c2) else c2)
+      | (n, LetIn (na,b,_,c)) ->
+	  clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c)
+      | (n, _) -> (ne, e, List.rev metas, c)
+  in 
+  clrec (Metamap.empty,Metamap.empty,[]) bound c
+
+let mk_clenv_from_n wc n (c,cty) =
+  let (namenv,env,args,concl) = clenv_environments n cty in
+  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
+    templtyp = mk_freelisted concl;
+    namenv = namenv;
+    env = env;
+    hook = wc }
+
+let mk_clenv_from wc = mk_clenv_from_n wc None
+
+let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+
+let map_clb f = function
+  | Cltyp cfl -> Cltyp (map_fl f cfl)
+  | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2)
+
+let subst_clenv f sub clenv = 
+  { templval = map_fl (subst_mps sub) clenv.templval;
+    templtyp = map_fl (subst_mps sub) clenv.templtyp;
+    namenv = clenv.namenv;
+    env = Metamap.map (map_clb (subst_mps sub)) clenv.env;
+    hook = f sub clenv.hook }
+
+let connect_clenv wc clenv = { clenv with hook = wc }
+
+(* Was used in wcclausenv.ml
+(* Changes the head of a clenv with (templ,templty) *)
+let clenv_change_head (templ,templty) clenv =
+  { templval = mk_freelisted templ;
+    templtyp = mk_freelisted templty;
+    namenv   = clenv.namenv;
+    env      = clenv.env;
+    hook     = clenv.hook }
+*)
+
+let mk_clenv_hnf_constr_type_of wc t =
+  mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
+
+let mk_clenv_rename_from wc (c,t) = 
+  mk_clenv_from wc (c,rename_bound_var (w_env wc) [] t)
+
+let mk_clenv_rename_from_n wc n (c,t) = 
+  mk_clenv_from_n wc n (c,rename_bound_var (w_env wc) [] t)
+    
+let mk_clenv_rename_type_of wc t =
+  mk_clenv_from wc (t,rename_bound_var (w_env wc) [] (w_type_of wc t))
+    
+let mk_clenv_rename_hnf_constr_type_of wc t =
+  mk_clenv_from wc
+    (t,rename_bound_var (w_env wc) [] (w_hnf_constr wc (w_type_of wc t)))
+
+let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
+			      
+let clenv_assign mv rhs clenv =
+  let rhs_fls = mk_freelisted rhs in 
+  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
+    error "clenv__assign: circularity in unification";
+  try
+    (match Metamap.find mv clenv.env with
+       | Clval (fls,ty) ->
+	   if not (eq_constr fls.rebus rhs) then
+	     try 
+	       (* Streams are lazy, force evaluation of id to catch Not_found*)
+	       let id = Metamap.find mv clenv.namenv in
+	       errorlabstrm "clenv_assign"
+		 (str "An incompatible instantiation has already been found for " ++ 
+		    pr_id id)
+	     with Not_found ->
+	       anomaly "clenv_assign: non dependent metavar already assigned"
+	   else
+	     clenv
+       | Cltyp bty -> 
+	   { templval = clenv.templval;
+	     templtyp = clenv.templtyp;
+	     namenv = clenv.namenv;
+	     env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env;
+	     hook = clenv.hook })
+  with Not_found -> 
+    error "clenv_assign"
+
+let clenv_val_of clenv mv = 
+  let rec valrec mv =
+    try
+      (match Metamap.find mv clenv.env with
+	 | Cltyp _ -> mkMeta mv
+	 | Clval(b,_) ->
+	     instance (List.map (fun mv' -> (mv',valrec mv')) 
+			       (Metaset.elements b.freemetas)) b.rebus)
+    with Not_found -> 
+      mkMeta mv
+  in 
+  valrec mv
+
+let clenv_instance clenv b =
+  let c_sigma =
+    List.map 
+      (fun mv -> (mv,clenv_val_of clenv mv)) (Metaset.elements b.freemetas)
+  in 
+  instance c_sigma b.rebus
+    
+let clenv_instance_term clenv c =
+  clenv_instance clenv (mk_freelisted c)
+
+
+(* This function put casts around metavariables whose type could not be
+ * infered by the refiner, that is head of applications, predicates and
+ * subject of Cases.
+ * Does check that the casted type is closed. Anyway, the refiner would
+ * fail in this case... *)
+
+let clenv_cast_meta clenv = 
+  let rec crec u =
+    match kind_of_term u with
+      | App _ | Case _ -> crec_hd u
+      | Cast (c,_) when isMeta c -> u
+      | _  -> map_constr crec u
+	    
+  and crec_hd u =
+    match kind_of_term (strip_outer_cast u) with
+      | Meta mv ->
+	  (try 
+	     match Metamap.find mv clenv.env with
+               | Cltyp b ->
+		   let b' = clenv_instance clenv b in 
+		   if occur_meta b' then u else mkCast (mkMeta mv, b')
+	       | Clval(_) -> u
+	   with Not_found -> 
+	     u)
+      | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+      | Case(ci,p,c,br) ->
+	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+      | _ -> u
+  in 
+  crec
+
+
+(* [clenv_pose (na,mv,cty) clenv]
+ * returns a new clausenv which has added to it the metavar MV,
+ * with type CTY.  the name NA, if it is not ANONYMOUS, will
+ * be entered into the name-map, as a way of accessing the new
+ * metavar. *)
+
+let clenv_pose (na,mv,cty) clenv =
+  { templval = clenv.templval;
+    templtyp = clenv.templtyp;
+    env = Metamap.add mv (Cltyp (mk_freelisted cty)) clenv.env;
+    namenv = (match na with
+		| Anonymous -> clenv.namenv
+		| Name id -> Metamap.add mv id clenv.namenv);
+    hook = clenv.hook }
+
+let clenv_defined clenv mv =
+  match Metamap.find mv clenv.env with
+    | Clval _ -> true
+    | Cltyp _ -> false
+
+let clenv_value clenv mv =
+  match Metamap.find mv clenv.env with
+    | Clval(b,_) -> b
+    | Cltyp _ -> failwith "clenv_value"
+	  
+let clenv_type clenv mv =
+  match Metamap.find mv clenv.env with
+    | Cltyp b -> b
+    | Clval(_,b) -> b
+	  
+let clenv_template clenv = clenv.templval
+
+let clenv_template_type clenv = clenv.templtyp
+
+let clenv_instance_value clenv mv =
+  clenv_instance clenv (clenv_value clenv mv)
+    
+let clenv_instance_type clenv mv =
+  clenv_instance clenv (clenv_type clenv mv)
+    
+let clenv_instance_template clenv =
+  clenv_instance clenv (clenv_template clenv)
+    
+let clenv_instance_template_type clenv =
+  clenv_instance clenv (clenv_template_type clenv)
+    
+let clenv_wtactic wt clenv =
+  { templval = clenv.templval;
+    templtyp = clenv.templtyp;
+    namenv = clenv.namenv;
+    env = clenv.env;
+    hook = wt clenv.hook }
+
+let clenv_type_of ce c =
+  let metamap =
+    List.map 
+      (function
+	 | (n,Clval(_,typ)) -> (n,typ.rebus)
+         | (n,Cltyp typ)    -> (n,typ.rebus))
+      (metamap_to_list ce.env)
+  in
+    Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c
+
+let clenv_instance_type_of ce c =
+  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
+
+
+
+(* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes:
+
+   metasubst:(int*constr)list    récolte les instances des (Meta k)
+   evarsubst:(constr*constr)list récolte les instances des (Const "?k")
+
+   Attention : pas d'unification entre les différences instances d'une
+   même meta ou evar, il peut rester des doublons *)
+
+(* Unification order: *)
+(* Left to right: unifies first argument and then the other arguments *)
+(*let unify_l2r x = List.rev x
+(* Right to left: unifies last argument and then the other arguments *)
+let unify_r2l x = x
+
+let sort_eqns = unify_r2l
+*)
+
+let unify_0 cv_pb wc m n =
+  let env = w_env wc
+  and sigma = w_Underlying wc in
+  let trivial_unify pb substn m n =
+    if (not(occur_meta m)) & is_fconv pb env sigma m n then substn
+    else error_cannot_unify (m,n) in
+  let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
+    let cM = Evarutil.whd_castappevar sigma m
+    and cN = Evarutil.whd_castappevar sigma n in 
+    match (kind_of_term cM,kind_of_term cN) with
+      | Meta k1, Meta k2 ->
+	  if k1 < k2 then (k1,cN)::metasubst,evarsubst
+	  else if k1 = k2 then substn
+	  else (k2,cM)::metasubst,evarsubst
+      | Meta k, _    -> (k,cN)::metasubst,evarsubst
+      | _, Meta k    -> (k,cM)::metasubst,evarsubst
+      | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
+      | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+
+      | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+	  unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
+      | Prod (_,t1,c1), Prod (_,t2,c2) ->
+	  unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
+      | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
+      | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
+
+      | App (f1,l1), App (f2,l2) ->
+	  let len1 = Array.length l1
+	  and len2 = Array.length l2 in
+          let (f1,l1,f2,l2) =
+	    if len1 = len2 then (f1,l1,f2,l2)
+	    else if len1 < len2 then
+              let extras,restl2 = array_chop (len2-len1) l2 in 
+              (f1, l1, appvect (f2,extras), restl2)
+	    else 
+	      let extras,restl1 = array_chop (len1-len2) l1 in 
+              (appvect (f1,extras), restl1, f2, l2) in
+          (try
+            array_fold_left2 (unirec_rec CONV)
+	      (unirec_rec CONV substn f1 f2) l1 l2
+	  with ex when catchable_exception ex ->
+            trivial_unify pb substn cM cN)
+      | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
+          array_fold_left2 (unirec_rec CONV)
+	    (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
+
+      | _ -> trivial_unify pb substn cM cN
+
+  in
+  if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then 
+    ([],[])
+  else 
+    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
+    ((*sort_eqns*) mc, (*sort_eqns*) ec)
+
+
+(* Unification
+ *
+ * Procedure:
+ * (1) The function [unify mc wc M N] produces two lists:
+ *     (a) a list of bindings Meta->RHS
+ *     (b) a list of bindings EVAR->RHS
+ *
+ * The Meta->RHS bindings cannot themselves contain
+ * meta-vars, so they get applied eagerly to the other
+ * bindings.  This may or may not close off all RHSs of
+ * the EVARs.  For each EVAR whose RHS is closed off,
+ * we can just apply it, and go on.  For each which
+ * is not closed off, we need to do a mimick step -
+ * in general, we have something like:
+ *
+ *      ?X == (c e1 e2 ... ei[Meta(k)] ... en)
+ *
+ * so we need to do a mimick step, converting ?X
+ * into
+ *
+ *      ?X -> (c ?z1 ... ?zn)
+ *
+ * of the proper types.  Then, we can decompose the
+ * equation into
+ *
+ *      ?z1 --> e1
+ *          ...
+ *      ?zi --> ei[Meta(k)]
+ *          ...
+ *      ?zn --> en
+ *
+ * and keep on going.  Whenever we find that a R.H.S.
+ * is closed, we can, as before, apply the constraint
+ * directly.  Whenever we find an equation of the form:
+ *
+ *      ?z -> Meta(n)
+ *
+ * we can reverse the equation, put it into our metavar
+ * substitution, and keep going.
+ *
+ * The most efficient mimick possible is, for each
+ * Meta-var remaining in the term, to declare a
+ * new EVAR of the same type.  This is supposedly
+ * determinable from the clausale form context -
+ * we look up the metavar, take its type there,
+ * and apply the metavar substitution to it, to
+ * close it off.  But this might not always work,
+ * since other metavars might also need to be resolved. *)
+
+let applyHead n c wc = 
+  let rec apprec n c cty wc =
+    if n = 0 then 
+      (wc,c)
+    else 
+      match kind_of_term (w_whd_betadeltaiota wc cty) with
+        | Prod (_,c1,c2) ->
+	    let evar = Evarutil.new_evar_in_sign (w_env wc) in
+            let (evar_n, _) = destEvar evar in
+	    (compose 
+	       (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
+	       (w_Declare evar_n c1))
+	    wc
+	| _ -> error "Apply_Head_Then"
+  in 
+  apprec n c (w_type_of wc c) wc
+
+let is_mimick_head f =
+  match kind_of_term f with
+      (Const _|Var _|Rel _|Construct _|Ind _) -> true
+    | _ -> false
+
+let rec mimick_evar hdc nargs sp wc =
+  let evd = Evd.map wc.sigma sp in
+  let wc' = extract_decl sp wc in
+  let (wc'', c) = applyHead nargs hdc wc' in
+  let (mc,ec) = unify_0 CONV wc'' (w_type_of wc'' c) (evd.evar_concl) in
+  let (wc''',_) = w_resrec mc ec wc'' in
+    if wc'== wc'''
+    then w_Define sp c wc
+    else  
+      let wc'''' = restore_decl sp evd wc''' in
+	w_Define sp (Evarutil.nf_evar wc''''.sigma c) {it = wc.it ; sigma = wc''''.sigma}
+
+and w_Unify cv_pb m n wc =
+  let (mc',ec') = unify_0 cv_pb wc m n in 
+  w_resrec mc' ec' wc
+
+and w_resrec metas evars wc =
+  match evars with
+    | [] -> (wc,metas)
+
+    | (lhs,rhs) :: t ->
+    match kind_of_term rhs with
+
+      | Meta k -> w_resrec ((k,lhs)::metas) t wc
+
+      | krhs ->
+      match kind_of_term lhs with
+
+	| Evar (evn,_) ->
+	    if w_defined_evar wc evn then
+	      let (wc',metas') = w_Unify CONV rhs lhs wc in 
+	      w_resrec (metas@metas') t wc'
+	    else
+	      (try 
+		 w_resrec metas t (w_Define evn rhs wc)
+               with ex when catchable_exception ex ->
+		 (match krhs with
+             	    | App (f,cl) when is_mimick_head f ->
+			let wc' = mimick_evar f (Array.length cl) evn wc in
+			w_resrec metas evars wc'
+		    | _ -> raise ex (*error "w_Unify" *)))
+	| _ -> anomaly "w_resrec"
+
+
+(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
+   particulier ne semblent pas vérifier que des instances différentes
+   d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
+   provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
+
+(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
+let unifyTerms m n gls = 
+  tclIDTAC {it = gls.it; 
+	    sigma = (get_gc (fst (w_Unify CONV m n (Refiner.project_with_focus gls))))}
+
+let unify m gls =
+  let n = pf_concl gls in unifyTerms m n gls
+
+(* [clenv_merge b metas evars clenv] merges common instances in metas
+   or in evars, possibly generating new unification problems; if [b]
+   is true, unification of types of metas is required *)
+
+let clenv_merge with_types metas evars clenv =
+  let ty_metas = ref [] in
+  let ty_evars = ref [] in
+  let rec clenv_resrec metas evars clenv =
+    match (evars,metas) with
+      | ([], []) -> clenv
+
+      | ((lhs,rhs)::t, metas) ->
+      (match kind_of_term rhs with
+
+	| Meta k -> clenv_resrec ((k,lhs)::metas) t clenv
+
+	| krhs ->
+        (match kind_of_term lhs with
+
+	  | Evar (evn,_) ->
+    	      if w_defined_evar clenv.hook evn then
+		let (metas',evars') = unify_0 CONV clenv.hook rhs lhs in
+		clenv_resrec (metas'@metas) (evars'@t) clenv
+    	      else begin
+		let rhs' = 
+		  if occur_meta rhs then subst_meta metas rhs else rhs 
+		in
+		if occur_evar evn rhs' then error "w_Unify";
+		try 
+		  clenv_resrec metas t 
+		    (clenv_wtactic (w_Define evn rhs') clenv) 
+		with ex when catchable_exception ex ->
+		  (match krhs with
+		     | App (f,cl) when is_mimick_head f ->
+			 clenv_resrec metas evars 
+			   (clenv_wtactic
+			      (mimick_evar f (Array.length cl) evn)
+			      clenv)
+           	     | _ -> raise ex (********* error "w_Unify" *))
+	      end
+
+	  | _ -> anomaly "clenv_resrec"))
+
+      | ([], (mv,n)::t) ->
+    	  if clenv_defined clenv mv then
+            let (metas',evars') =
+              unify_0 CONV clenv.hook (clenv_value clenv mv).rebus n in
+            clenv_resrec (metas'@t) evars' clenv
+    	  else
+            begin
+	      if with_types (* or occur_meta mvty *) then
+	        (let mvty = clenv_instance_type clenv mv in
+		try 
+		  let nty = clenv_type_of clenv 
+			      (clenv_instance clenv (mk_freelisted n)) in
+		  let (mc,ec) = unify_0 CUMUL clenv.hook nty mvty in
+                  ty_metas := mc @ !ty_metas;
+                  ty_evars := ec @ !ty_evars
+		with e when Logic.catchable_exception e -> ());
+	      clenv_resrec t [] (clenv_assign mv n clenv)
+            end in
+  (* merge constraints *)
+  let clenv' = clenv_resrec metas evars clenv in
+  if with_types then
+    (* merge constraints about types: if they fail, don't worry *)
+    try clenv_resrec !ty_metas !ty_evars clenv'
+    with e when Logic.catchable_exception e -> clenv'
+  else clenv'
+
+(* [clenv_unify M N clenv]
+   performs a unification of M and N, generating a bunch of
+   unification constraints in the process.  These constraints
+   are processed, one-by-one - they may either generate new
+   bindings, or, if there is already a binding, new unifications,
+   which themselves generate new constraints.  This continues
+   until we get failure, or we run out of constraints.
+   [clenv_typed_unify M N clenv] expects in addition that expected
+   types of metavars are unifiable with the types of their instances    *)
+
+let clenv_unify_core_0 with_types cv_pb m n clenv =
+  let (mc,ec) = unify_0 cv_pb clenv.hook m n in 
+  clenv_merge with_types mc ec clenv
+
+let clenv_unify_0 = clenv_unify_core_0 false
+let clenv_typed_unify = clenv_unify_core_0 true
+
+
+(* takes a substitution s, an open term op and a closed term cl
+   try to find a subterm of cl which matches op, if op is just a Meta
+   FAIL because we cannot find a binding *)
+
+let iter_fail f a =
+  let n = Array.length a in 
+  let rec ffail i =
+    if i = n then error "iter_fail" 
+    else
+      try f a.(i) 
+      with ex when catchable_exception ex -> ffail (i+1)
+  in ffail 0
+
+(* Tries to find an instance of term [cl] in term [op].
+   Unifies [cl] to every subterm of [op] until it finds a match.
+   Fails if no match is found *)
+let unify_to_subterm clause (op,cl) =
+  let rec matchrec cl =
+    let cl = strip_outer_cast cl in
+    (try 
+       if closed0 cl 
+       then clenv_unify_0 CONV op cl clause,cl
+       else error "Bound 1"
+     with ex when catchable_exception ex ->
+       (match kind_of_term cl with 
+	  | App (f,args) ->
+	      let n = Array.length args in
+	      assert (n>0);
+	      let c1 = mkApp (f,Array.sub args 0 (n-1)) in
+	      let c2 = args.(n-1) in
+	      (try 
+		 matchrec c1
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+          | Case(_,_,c,lf) -> (* does not search in the predicate *)
+	       (try 
+		 matchrec c
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec lf)
+	  | LetIn(_,c1,_,c2) -> 
+	       (try 
+		 matchrec c1
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+
+	  | Fix(_,(_,types,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+	
+	  | CoFix(_,(_,types,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+
+          | Prod (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when catchable_exception ex -> 
+		 matchrec c)
+          | Lambda (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when catchable_exception ex -> 
+		 matchrec c)
+          | _ -> error "Match_subterm")) 
+  in 
+  try matchrec cl
+  with ex when catchable_exception ex ->
+    raise (RefinerError (NoOccurrenceFound op))
+
+let unify_to_subterm_list allow_K clause oplist t = 
+  List.fold_right 
+    (fun op (clause,l) ->
+      if isMeta op then
+	if allow_K then (clause,op::l)
+	else error "Match_subterm"
+      else if occur_meta op then
+        let (clause',cl) =
+          try 
+	    (* This is up to delta for subterms w/o metas ... *)
+	    unify_to_subterm clause (strip_outer_cast op,t)
+          with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op)
+        in 
+	(clause',cl::l)
+      else if not allow_K & not (dependent op t) then
+	(* This is not up to delta ... *)
+	raise (RefinerError (NoOccurrenceFound op))
+      else
+	(clause,op::l))
+    oplist 
+    (clause,[])
+
+let secondOrderAbstraction allow_K typ (p, oplist) clause =
+  let env = w_env clause.hook in
+  let sigma = w_Underlying clause.hook in
+  let (clause',cllist) = unify_to_subterm_list allow_K clause oplist typ in
+  let typp = clenv_instance_type clause' p in 
+  let pred = abstract_list_all env sigma typp typ cllist in
+  clenv_unify_0 CONV (mkMeta p) pred clause'
+
+let clenv_unify2 allow_K cv_pb ty1 ty2 clause =
+  let c1, oplist1 = whd_stack ty1 in
+  let c2, oplist2 = whd_stack ty2 in
+  match kind_of_term c1, kind_of_term c2 with
+    | Meta p1, _ ->
+        (* Find the predicate *)
+	let clause' =
+          secondOrderAbstraction allow_K ty2 (p1,oplist1) clause in 
+        (* Resume first order unification *)
+	clenv_unify_0 cv_pb (clenv_instance_term clause' ty1) ty2 clause'
+    | _, Meta p2 ->
+        (* Find the predicate *)
+	let clause' =
+          secondOrderAbstraction allow_K ty1 (p2, oplist2) clause in 
+        (* Resume first order unification *)
+	clenv_unify_0 cv_pb ty1 (clenv_instance_term clause' ty2) clause'
+    | _ -> error "clenv_unify2"
+
+
+(* The unique unification algorithm works like this: If the pattern is
+   flexible, and the goal has a lambda-abstraction at the head, then
+   we do a first-order unification.
+
+   If the pattern is not flexible, then we do a first-order
+   unification, too.
+
+   If the pattern is flexible, and the goal doesn't have a
+   lambda-abstraction head, then we second-order unification. *)
+
+(* We decide here if first-order or second-order unif is used for Apply *)
+(* We apply a term of type (ai:Ai)C and try to solve a goal C'          *)
+(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve    *)
+
+(* 3-4-99 [HH] New fo/so choice heuristic :
+   In case we have to unify (Meta(1) args) with ([x:A]t args')
+   we first try second-order unification and if it fails first-order.
+   Before, second-order was used if the type of Meta(1) and [x:A]t was
+   convertible and first-order otherwise. But if failed if e.g. the type of
+   Meta(1) had meta-variables in it. *)
+let clenv_unify allow_K cv_pb ty1 ty2 clenv =
+  let hd1,l1 = whd_stack ty1 in
+  let hd2,l2 = whd_stack ty2 in
+  match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
+    (* Pattern case *)
+    | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
+      when List.length l1 = List.length l2 ->
+	(try 
+	   clenv_typed_unify cv_pb ty1 ty2 clenv
+	 with ex when catchable_exception ex -> 
+	   try 
+	     clenv_unify2 allow_K cv_pb ty1 ty2 clenv
+	   with RefinerError (NoOccurrenceFound c) as e -> raise e
+	     | ex when catchable_exception ex -> 
+	     error "Cannot solve a second-order unification problem")
+
+     (* Second order case *)
+     | (Meta _, true, _, _ | _, _, Meta _, true) -> 
+	(try 
+	   clenv_unify2 allow_K cv_pb ty1 ty2 clenv
+	with RefinerError (NoOccurrenceFound c) as e -> raise e
+	  | ex when catchable_exception ex -> 
+          try 
+	     clenv_typed_unify cv_pb ty1 ty2 clenv
+          with ex when catchable_exception ex -> 
+             error "Cannot solve a second-order unification problem")
+
+     (* General case: try first order *)
+     | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv
+
+
+(* [clenv_bchain mv clenv' clenv]
+ *
+ * Resolves the value of "mv" (which must be undefined) in clenv to be
+ * the template of clenv' be the value "c", applied to "n" fresh
+ * metavars, whose types are chosen by destructing "clf", which should
+ * be a clausale forme generated from the type of "c".  The process of
+ * resolution can cause unification of already-existing metavars, and
+ * of the fresh ones which get created.  This operation is a composite
+ * of operations which pose new metavars, perform unification on
+ * terms, and make bindings.  *)
+
+let clenv_bchain mv subclenv clenv =
+  (* Add the metavars of [subclenv] to [clenv], with their name-environment *)
+  let clenv' =
+    { templval = clenv.templval;
+      templtyp = clenv.templtyp;
+      namenv =
+	List.fold_left (fun ne (mv,id) ->
+			  if clenv_defined subclenv mv then 
+			    ne
+			  else if metamap_in_dom mv ne then begin
+			    warning ("Cannot put metavar "^(string_of_meta mv)^
+				     " in name-environment twice");
+			    ne
+			  end else 
+			    Metamap.add mv id ne)
+          clenv.namenv (metamap_to_list subclenv.namenv);
+      env = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
+	       clenv.env (metamap_to_list subclenv.env);
+      hook = clenv.hook } 
+  in
+  (* unify the type of the template of [subclenv] with the type of [mv] *)
+  let clenv'' =
+    clenv_unify true CUMUL
+      (clenv_instance clenv' (clenv_template_type subclenv))
+      (clenv_instance_type clenv' mv)
+      clenv' 
+  in
+  (* assign the metavar *)
+  let clenv''' =
+    clenv_assign mv (clenv_instance clenv' (clenv_template subclenv)) clenv''
+  in 
+  clenv'''
+
+
+(* swaps the "hooks" in [clenv1] and [clenv2], so we can then use
+   backchain to hook them together *)
+
+let clenv_swap clenv1 clenv2 =
+  let clenv1' = { templval = clenv1.templval;
+		  templtyp = clenv1.templtyp;
+		  namenv = clenv1.namenv;
+		  env = clenv1.env;
+		  hook = clenv2.hook} 
+  and clenv2' = { templval = clenv2.templval;
+		  templtyp = clenv2.templtyp;
+		  namenv = clenv2.namenv;
+		  env = clenv2.env;
+		  hook = clenv1.hook}
+  in 
+  (clenv1',clenv2')
+
+let clenv_fchain mv nextclenv clenv =
+  let (clenv',nextclenv') = clenv_swap clenv nextclenv in 
+  clenv_bchain mv clenv' nextclenv'
+
+let clenv_refine kONT clenv gls =
+  tclTHEN
+    (kONT clenv.hook) 
+    (refine (clenv_instance_template clenv)) gls
+
+let clenv_refine_cast kONT clenv gls =
+  tclTHEN
+    (kONT clenv.hook) 
+    (refine (clenv_cast_meta clenv (clenv_instance_template clenv)))
+    gls
+
+(* [clenv_metavars clenv mv]
+ * returns a list of the metavars which appear in the type of
+ * the metavar mv.  The list is unordered. *)
+
+let clenv_metavars clenv mv =
+  match Metamap.find mv clenv.env with
+    | Clval(_,b) -> b.freemetas
+    | Cltyp b -> b.freemetas
+
+let clenv_template_metavars clenv = clenv.templval.freemetas
+
+(* [clenv_dependent hyps_only clenv]
+ * returns a list of the metavars which appear in the template of clenv,
+ * and which are dependent, This is computed by taking the metavars in cval,
+ * in right-to-left order, and collecting the metavars which appear
+ * in their types, and adding in all the metavars appearing in the
+ * type of clenv.
+ * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
+
+let dependent_metas clenv mvs conclmetas =
+  List.fold_right
+    (fun mv deps ->
+       Metaset.union deps (clenv_metavars clenv mv))
+    mvs conclmetas
+
+let clenv_dependent hyps_only clenv =
+  let mvs = collect_metas (clenv_instance_template clenv) in
+  let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  List.filter
+    (fun mv -> Metaset.mem mv deps && not (hyps_only && Metaset.mem mv ctyp_mvs))
+    mvs
+
+let clenv_missing c = clenv_dependent true c
+
+(* [clenv_independent clenv]
+ * returns a list of metavariables which appear in the term cval,
+ * and which are not dependent.  That is, they do not appear in
+ * the types of other metavars which are in cval, nor in the type
+ * of cval, ctyp. *)
+
+let clenv_independent clenv =
+  let mvs = collect_metas (clenv_instance_template clenv) in
+  let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
+
+let w_coerce wc c ctyp target =
+  let j = make_judge c ctyp in
+  let env = w_env wc in
+  let isevars = Evarutil.create_evar_defs (w_Underlying wc) in
+  let j' = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
+  (* faire quelque chose avec isevars ? *)
+  j'.uj_val
+
+let clenv_constrain_dep_args hyps_only clause = function
+  | [] -> clause 
+  | mlist ->
+      let occlist = clenv_dependent hyps_only clause in
+      if List.length occlist = List.length mlist then
+	List.fold_left2
+          (fun clenv k c ->
+	    let wc = clause.hook in
+	    try
+	      let k_typ = w_hnf_constr wc (clenv_instance_type clause k) in
+	      let c_typ = w_hnf_constr wc (w_type_of wc c) in
+	      let c' = w_coerce wc c c_typ k_typ in
+	      clenv_unify true CONV (mkMeta k) c' clenv
+	    with _ ->
+              clenv_unify true CONV (mkMeta k) c clenv)
+          clause occlist mlist
+      else 
+	error ("Not the right number of missing arguments (expected "
+	       ^(string_of_int (List.length occlist))^")")
+
+let clenv_constrain_missing_args mlist clause =
+  clenv_constrain_dep_args true clause mlist
+
+let clenv_lookup_name clenv id =
+  match metamap_inv clenv.namenv id with
+    | []  -> 
+	errorlabstrm "clenv_lookup_name"
+          (str"No such bound variable " ++ pr_id id)
+    | [n] -> 
+	n
+    |  _  -> 
+	 anomaly "clenv_lookup_name: a name occurs more than once in clause"
+
+let clenv_match_args s clause =
+  let mvs = clenv_independent clause in 
+  let rec matchrec clause = function
+    | [] -> clause
+    | (loc,b,c)::t ->
+	let k =
+	  match b with
+            | NamedHyp s ->
+		if List.exists (fun (_,b',_) -> b=b') t then 
+		  errorlabstrm "clenv_match_args" 
+		    (str "The variable " ++ pr_id s ++ 
+		    str " occurs more than once in binding")
+		else
+		  clenv_lookup_name clause s
+	    | AnonHyp n ->
+		if List.exists (fun (_,b',_) -> b=b') t then
+		  errorlabstrm "clenv_match_args"
+		    (str "The position " ++ int n ++
+		    str " occurs more than once in binding");
+		try 
+		  List.nth mvs (n-1)
+		with (Failure _|Invalid_argument _) ->
+                  errorlabstrm "clenv_match_args" (str "No such binder")
+	in
+	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
+	(* nf_betaiota was before in type_of - useful to reduce types like *)
+	(* (x:A)([x]P u) *)
+	and c_typ = w_hnf_constr clause.hook
+          (nf_betaiota (w_type_of clause.hook c)) in
+	let cl =
+	  (* Try to infer some Meta/Evar from the type of [c] *)
+	  try 
+            clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
+	  with _ ->
+	  (* Try to coerce to the type of [k]; cannot merge with the
+	     previous case because Coercion does not handle Meta *)
+          let c' = w_coerce clause.hook c c_typ k_typ in
+	  try clenv_unify true CONV (mkMeta k) c' clause
+	  with RefinerError (CannotUnify (m,n)) ->
+	    Stdpp.raise_with_loc loc
+ 	      (RefinerError (CannotUnifyBindingType (m,n)))
+	in matchrec cl t
+  in 
+  matchrec clause s
+
+type arg_bindings = (int * constr) list
+
+let clenv_constrain_with_bindings bl clause =
+  if bl = [] then 
+    clause 
+  else 
+    let all_mvs = collect_metas (clenv_template clause).rebus in
+    let rec matchrec clause = function
+      | []       -> clause
+      | (n,c)::t ->
+          let k = 
+            (try
+              if n > 0 then 
+		List.nth all_mvs (n-1)
+              else if n < 0 then 
+		List.nth (List.rev all_mvs) (-n-1)
+              else error "clenv_constrain_with_bindings" 
+            with Failure _ ->
+              errorlabstrm "clenv_constrain_with_bindings"
+                (str"Clause did not have " ++ int n ++ str"-th" ++
+                str" absolute argument")) in
+	  let env = Global.env () in
+	  let sigma = Evd.empty in
+	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
+	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
+	  matchrec
+            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
+    in 
+    matchrec clause bl
+
+
+(* [clenv_pose_dependent_evars clenv]
+ * For each dependent evar in the clause-env which does not have a value,
+ * pose a value for it by constructing a fresh evar.  We do this in
+ * left-to-right order, so that every evar's type is always closed w.r.t.
+ * metas. *)
+
+let clenv_pose_dependent_evars clenv =
+  let dep_mvs = clenv_dependent false clenv in
+  List.fold_left
+    (fun clenv mv ->
+       let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
+       let (evar_n,_) = destEvar evar in
+       let tY = clenv_instance_type clenv mv in
+       let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
+       clenv_assign mv evar clenv')
+    clenv
+    dep_mvs
+
+(***************************)
+
+let clenv_unique_resolver allow_K clause gl =
+  clenv_unify allow_K CUMUL
+    (clenv_instance_template_type clause) (pf_concl gl) clause 
+
+let res_pf kONT clenv gls =
+  clenv_refine kONT (clenv_unique_resolver false clenv gls) gls
+    
+let res_pf_cast kONT clenv gls =
+  clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls
+
+let elim_res_pf kONT clenv allow_K gls =
+  clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls
+
+let elim_res_pf_THEN_i kONT clenv tac gls =  
+  let clenv' = (clenv_unique_resolver true clenv gls) in
+  tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
+
+let e_res_pf kONT clenv gls =
+  clenv_refine kONT
+    (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
+
+(* Clausal environment for an application *)
+
+let make_clenv_binding_gen n wc (c,t) = function
+  | ImplicitBindings largs ->
+      let clause = mk_clenv_from_n wc n (c,t) in
+      clenv_constrain_dep_args (n <> None) clause largs
+  | ExplicitBindings lbind ->
+      let clause = mk_clenv_rename_from_n wc n (c,t) in
+      clenv_match_args lbind clause
+  | NoBindings ->
+      mk_clenv_from_n wc n (c,t)
+
+let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
+let make_clenv_binding = make_clenv_binding_gen None
+
+open Printer
+
+let pr_clenv clenv =
+  let pr_name mv =
+    try 
+      let id = Metamap.find mv clenv.namenv in
+      (str"[" ++ pr_id id ++ str"]")
+    with Not_found -> (mt ())
+  in
+  let pr_meta_binding = function
+    | (mv,Cltyp b) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ())
+    | (mv,Clval(b,_)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ())
+  in
+  (str"TEMPL: " ++ prterm clenv.templval.rebus ++
+     str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++
+     (prlist pr_meta_binding (metamap_to_list clenv.env)))
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
new file mode 100644
index 00000000..10e0004e
--- /dev/null
+++ b/proofs/clenv.mli
@@ -0,0 +1,142 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: clenv.mli,v 1.32.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Proof_type
+(*i*)
+
+(* [new_meta] is a generator of unique meta variables *)
+val new_meta : unit -> metavariable
+
+(* [exist_to_meta] generates new metavariables for each existential
+   and performs the replacement in the given constr *)
+val exist_to_meta :
+  Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
+
+(* The Type of Constructions clausale environments. *)
+
+module Metaset : Set.S with type elt = metavariable
+
+module Metamap : Map.S with type key = metavariable
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Metaset.t }
+
+type clbinding = 
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Metamap.t;
+  env : clbinding Metamap.t;
+  hook : 'a }
+
+type wc = named_context sigma (* for a better reading of the following *)
+
+(* [templval] is the template which we are trying to fill out.
+ * [templtyp] is its type.
+ * [namenv] is a mapping from metavar numbers to names, for
+ *          use in instanciating metavars by name.
+ * [env] is the mapping from metavar numbers to their types
+ *       and values.
+ * [hook] is the pointer to the current walking context, for
+ *        integrating existential vars and metavars. *)
+
+val collect_metas : constr -> metavariable list
+val mk_clenv : 'a -> constr -> 'a clausenv
+val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
+val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
+val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
+val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
+val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
+val mk_clenv_type_of : wc -> constr -> wc clausenv
+
+val subst_clenv : (substitution -> 'a -> 'a) -> 
+  substitution -> 'a clausenv -> 'a clausenv
+
+val connect_clenv : wc -> 'a clausenv -> wc clausenv
+(*i Was used in wcclausenv.ml
+val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
+i*)
+val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
+val clenv_instance_term : wc clausenv -> constr -> constr
+val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
+val clenv_template : 'a clausenv -> constr freelisted
+val clenv_template_type : 'a clausenv -> constr freelisted
+val clenv_instance_type : wc clausenv -> metavariable -> constr
+val clenv_instance_template : wc clausenv -> constr
+val clenv_instance_template_type : wc clausenv -> constr
+val clenv_type_of : wc clausenv -> constr -> constr
+val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+
+(* Unification with clenv *)
+type arg_bindings = (int * constr) list
+
+val unify_0 : 
+  Reductionops.conv_pb -> wc -> constr -> constr 
+    -> Termops.metamap * (constr * constr) list
+val clenv_unify : 
+  bool -> Reductionops.conv_pb -> constr -> constr ->
+  wc clausenv -> wc clausenv
+val clenv_match_args :
+  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
+val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+
+(* Bindings *)
+val clenv_independent : wc clausenv -> metavariable list
+val clenv_missing : 'a clausenv -> metavariable list
+val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
+  constr list -> wc clausenv -> wc clausenv
+(*
+val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
+*)
+val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
+val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
+
+val make_clenv_binding_apply :
+  wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
+val make_clenv_binding :
+  wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
+
+(* Tactics *)
+val unify : constr -> tactic
+val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
+val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
+val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
+val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic
+val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val elim_res_pf_THEN_i : 
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
+
+(* Pretty-print *)
+val pr_clenv : 'a clausenv -> Pp.std_ppcmds
+
+(* Exported for debugging *)
+val unify_to_subterm : 
+  wc clausenv -> constr * constr -> wc clausenv * constr
+val unify_to_subterm_list : 
+  bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
+val clenv_typed_unify :
+  Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
+
+(*i This should be in another module i*)
+
+(* [abstract_list_all env sigma t c l]                     *)
+(* abstracts the terms in l over c to get a term of type t *)
+val abstract_list_all :
+  Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr
diff --git a/proofs/doc.tex b/proofs/doc.tex
new file mode 100644
index 00000000..431027ef
--- /dev/null
+++ b/proofs/doc.tex
@@ -0,0 +1,14 @@
+
+\newpage
+\section*{The Proof Engine}
+
+\ocwsection \label{proofs}
+This chapter describes the \Coq\ proof engine, which is also called
+the ``refiner'', since it provides a way to build terms by successive
+refining steps. Those steps are either primitive rules or higher-level
+tactics.
+The modules of the proof engine are organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=proofs.dep.ps,width=\linewidth}\end{center}
+
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
new file mode 100644
index 00000000..d59ff835
--- /dev/null
+++ b/proofs/evar_refiner.ml
@@ -0,0 +1,187 @@
+(************************************************************************)
+(*  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: evar_refiner.ml,v 1.36.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Environ
+open Evd
+open Sign
+open Reductionops
+open Typing
+open Instantiate
+open Tacred
+open Proof_trees
+open Proof_type
+open Logic
+open Refiner
+open Tacexpr
+open Nameops
+
+
+type wc = named_context sigma (* for a better reading of the following *)
+
+let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
+let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
+
+type w_tactic = named_context sigma -> named_context sigma
+
+let startWalk gls =
+  let evc = project_with_focus gls in
+  (evc,
+   (fun wc' gls' ->
+      if not !Options.debug or (gls.it = gls'.it) then
+(*        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*)
+          tclIDTAC {it=gls'.it; sigma = (get_gc wc')}
+(*        else
+          (local_Constraints (get_focus (ids_it wc'))
+             {it=gls'.it; sigma = get_gc (ids_it wc')})*)
+      else error "Walking"))
+
+let extract_decl sp evc =
+  let evdmap = evc.sigma in
+  let evd = Evd.map evdmap sp in 
+    { it = evd.evar_hyps;
+      sigma = Evd.rmv evdmap sp }
+
+let restore_decl sp evd evc =
+  (rc_add evc (sp,evd))
+
+
+(* [w_Focusing sp wt wc]
+ *
+ * Focuses the walking context WC onto the declaration SP, given that
+ * this declaration is UNDEFINED.  Then, it runs the walking_tactic,
+ * WT, on this new context.  When the result is returned, we recover
+ * the resulting focus (access list) and restore it to SP's declaration.
+ *
+ * It is an error to cause SP to change state while we are focused on it. *)
+
+(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
+                       (wc : named_context sigma) =
+  let hyps  = wc.it
+  and evd   = Evd.map wc.sigma sp in
+  let (wc' : named_context sigma) = extract_decl sp wc in
+  let (wc'',rslt) = wt wc' in 
+(*  if not (ids_eq wc wc'') then error "w_saving_focus"; *)
+  if wc'==wc'' then 
+    wt' rslt wc
+  else 
+    let wc''' = restore_decl sp evd wc'' in 
+    wt' rslt {it = hyps; sigma = wc'''.sigma} *)
+      
+let w_add_sign (id,t) (wc : named_context sigma) =
+  { it = Sign.add_named_decl (id,None,t) wc.it;
+    sigma = wc.sigma }
+
+let w_Focus sp wc = extract_decl sp wc
+
+let w_Underlying wc = wc.sigma
+let w_whd wc c      = Evarutil.whd_castappevar (w_Underlying wc) c
+let w_type_of wc c  =
+  type_of (Global.env_of_context wc.it) wc.sigma c
+let w_env     wc    = get_env wc
+let w_hyps    wc    = named_context (get_env wc)
+let w_defined_evar wc k      = Evd.is_defined (w_Underlying wc) k
+let w_const_value wc         = constant_value (w_env wc)
+let w_conv_x wc m n          = is_conv (w_env wc) (w_Underlying wc) m n
+let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
+let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
+
+
+let w_Declare sp ty (wc : named_context sigma) =
+  let _ = w_type_of wc ty in (* Utile ?? *)
+  let sign = get_hyps wc in
+  let newdecl = mk_goal sign ty in 
+  ((rc_add wc (sp,newdecl)): named_context sigma)
+
+let w_Define sp c wc =
+  let spdecl = Evd.map (w_Underlying wc) sp in
+  let cty = 
+    try 
+      w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
+    with 
+	Not_found -> error "Instantiation contains unlegal variables"
+      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
+      errorlabstrm "w_Define"
+      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
+       str (string_of_existential sp))
+  in 
+  match spdecl.evar_body with
+    | Evar_empty ->
+    	let spdecl' = { evar_hyps = spdecl.evar_hyps;
+                       	evar_concl = spdecl.evar_concl;
+                       	evar_body = Evar_defined c }
+    	in 
+	  Proof_trees.rc_add wc (sp,spdecl')
+    | _ -> error "define_evar"
+
+
+(******************************************)
+(* Instantiation of existential variables *)
+(******************************************)
+
+(* The instantiate tactic *)
+
+let evars_of evc c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+    | _ -> fold_constr evrec acc c
+  in 
+  evrec [] c
+
+let instantiate n c ido gl = 
+  let wc = Refiner.project_with_focus gl in
+  let evl = 
+    match ido with
+	None -> evars_of wc.sigma gl.it.evar_concl 
+      | Some (id,_,_) -> 
+	  let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in
+	    evars_of wc.sigma typ in
+    if List.length evl < n then error "not enough evars";
+    let (n,_) as k = destEvar (List.nth evl (n-1)) in 
+      if Evd.is_defined wc.sigma n then 
+	error "Instantiate called on already-defined evar";
+      let wc' = w_Define n c wc in 
+	tclIDTAC {it = gl.it ; sigma = wc'.sigma}
+
+let pfic gls c =
+  let evc = gls.sigma in 
+  Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
+
+(*
+let instantiate_tac = function
+  | [Integer n; Command com] ->
+      (fun gl -> instantiate n (pfic gl com) gl)
+  | [Integer n; Constr c] ->
+      (fun gl -> instantiate n c gl)
+  | _ -> invalid_arg "Instantiate called with bad arguments"
+*)
+
+(* vernac command existential *)
+
+let instantiate_pf_com n com pfts = 
+  let gls = top_goal_of_pftreestate pfts in
+  let wc = project_with_focus gls in
+  let sigma = (w_Underlying wc) in 
+  let (sp,evd) = 
+    try
+      List.nth (Evd.non_instantiated sigma) (n-1) 
+    with Failure _ -> 
+      error "not so many uninstantiated existential variables"
+  in 
+  let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in     
+  let wc' = w_Define sp c wc in
+  let newgc = (w_Underlying wc') in
+  change_constraints_pftreestate newgc pfts
+
+
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
new file mode 100644
index 00000000..d7f393b3
--- /dev/null
+++ b/proofs/evar_refiner.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: evar_refiner.mli,v 1.28.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Environ
+open Evd
+open Refiner
+open Proof_type
+(*i*)
+
+type wc = named_context sigma (* for a better reading of the following *)
+
+(* Refinement of existential variables. *)
+
+val rc_of_pfsigma : proof_tree sigma -> wc
+val rc_of_glsigma : goal sigma -> wc
+
+(* A [w_tactic] is a tactic which modifies the a set of evars of which
+   a goal depend, either by instantiating one, or by declaring a new
+   dependent goal *)
+type w_tactic = wc -> wc
+
+val startWalk : goal sigma -> wc * (wc -> tactic)
+
+val extract_decl : evar -> w_tactic
+val restore_decl : evar -> evar_info -> w_tactic
+val w_Declare    : evar -> types -> w_tactic
+val w_Define     : evar -> constr -> w_tactic
+
+val w_Underlying : wc -> evar_map
+val w_env        : wc -> env
+val w_hyps       : wc -> named_context
+val w_whd        : wc -> constr -> constr
+val w_type_of    : wc -> constr -> constr
+val w_add_sign   : (identifier * types) -> w_tactic
+
+val w_whd_betadeltaiota : wc -> constr -> constr
+val w_hnf_constr        : wc -> constr -> constr
+val w_conv_x            : wc -> constr -> constr -> bool
+val w_const_value       : wc -> constant -> constr
+val w_defined_evar      : wc -> existential_key -> bool
+
+val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic
+(*
+val instantiate_tac : tactic_arg list -> tactic
+*)
+val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
new file mode 100644
index 00000000..3cc44a0f
--- /dev/null
+++ b/proofs/logic.ml
@@ -0,0 +1,786 @@
+(************************************************************************)
+(*  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: logic.ml,v 1.80.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Evd
+open Term
+open Termops
+open Sign
+open Environ
+open Reductionops
+open Inductive
+open Inductiveops
+open Typing
+open Proof_trees
+open Proof_type
+open Typeops
+open Type_errors
+open Coqast
+open Retyping
+open Evarutil
+ 
+type refiner_error =
+
+  (* Errors raised by the refiner *)
+  | BadType of constr * constr * constr
+  | OccurMeta of constr
+  | OccurMetaGoal of constr
+  | CannotApply of constr * constr
+  | NotWellTyped of constr
+  | NonLinearProof of constr
+
+  (* Errors raised by the tactics *)
+  | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
+  | CannotGeneralize of constr
+  | IntroNeedsProduct
+  | DoesNotOccurIn of constr * identifier
+  | NoOccurrenceFound of constr
+
+exception RefinerError of refiner_error
+
+open Pretype_errors
+
+let catchable_exception = function
+  | Util.UserError _ | TypeError _ | RefinerError _
+  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
+    Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true
+  | _ -> false
+
+let error_cannot_unify (m,n) =
+  raise (RefinerError (CannotUnify (m,n)))
+
+(* Tells if the refiner should check that the submitted rules do not
+   produce invalid subgoals *)
+let check = ref false
+
+let without_check tac gl =
+  let c = !check in
+  check := false;
+  let r = tac gl in
+  check := c;
+  r
+
+let with_check tac gl =
+  let c = !check in
+  check := true;
+  let r = tac gl in
+  check := c;
+  r
+   
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the structural rules (moving and deleting
+   hypotheses around) *)
+
+let check_clear_forward cleared_ids used_ids whatfor =
+  if !check && cleared_ids<>[] then
+    Idset.iter
+      (fun id' ->
+        if List.mem id' cleared_ids then
+          error (string_of_id id'^" is used in "^whatfor))
+      used_ids
+
+(* The Clear tactic: it scans the context for hypotheses to be removed
+   (instead of iterating on the list of identifier to be removed, which
+   forces the user to give them in order). *)
+let clear_hyps ids gl =
+  let env = Global.env() in
+  let (nhyps,rmv) =
+    Sign.fold_named_context
+      (fun (id,c,ty as d) (hyps,rmv) ->
+        if List.mem id ids then
+          (hyps,id::rmv)
+        else begin
+          check_clear_forward rmv (global_vars_set_of_decl env d)
+            ("hypothesis "^string_of_id id);
+          (add_named_decl d hyps, rmv)
+        end)
+      gl.evar_hyps
+      ~init:(empty_named_context,[]) in
+  let ncl = gl.evar_concl in
+  check_clear_forward rmv (global_vars_set env ncl) "conclusion";
+  mk_goal nhyps ncl
+
+(* The ClearBody tactic *)
+
+(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
+   returns [tail::(f head (id,_,_) tail)] *)
+let apply_to_hyp sign id f =
+  let found = ref false in
+  let sign' =
+    fold_named_context_both_sides
+      (fun head (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f head d tail
+	 end else 
+	   add_named_decl d head)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign' else error "No such assumption"
+
+(* Same but with whole environment *)
+let apply_to_hyp2 env id f =
+  let found = ref false in
+  let env' =
+    fold_named_context_both_sides
+      (fun env (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f env d tail
+	 end else 
+	   push_named d env)
+      (named_context env) ~init:(reset_context env)
+  in
+  if (not !check) || !found then env' else error "No such assumption"
+
+let apply_to_hyp_and_dependent_on sign id f g =
+  let found = ref false in
+  let sign =
+    Sign.fold_named_context
+      (fun (idc,_,_ as d) oldest ->
+         if idc = id then (found := true; add_named_decl (f d) oldest)
+         else if !found then add_named_decl (g d) oldest
+         else add_named_decl d oldest)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign else error "No such assumption"
+
+let check_typability env sigma c =
+  if !check then let _ = type_of env sigma c in () 
+
+let recheck_typability (what,id) env sigma t =
+  try check_typability env sigma t
+  with _ ->
+    let s = match what with
+      | None -> "the conclusion"
+      | Some id -> "hypothesis "^(string_of_id id) in
+    error
+      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
+  
+let remove_hyp_body env sigma id =
+  apply_to_hyp2 env id
+    (fun env (_,c,t) tail ->
+       match c with
+         | None -> error ((string_of_id id)^" is not a local definition")
+         | Some c ->
+             let env' = push_named (id,None,t) env in
+             if !check then 
+               ignore
+                 (Sign.fold_named_context 
+                    (fun (id',c,t as d) env'' ->
+                       (match c with
+                          | None -> 
+                              recheck_typability (Some id',id) env'' sigma t
+                          | Some b ->
+                              let b' = mkCast (b,t) in
+                              recheck_typability (Some id',id) env'' sigma b');
+                       push_named d env'')
+                    (List.rev tail) ~init:env');
+             env')
+
+
+(* Auxiliary functions for primitive MOVE tactic
+ *
+ * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves
+ * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the 
+ * left side [left] of the full signature if [toleft=true] or to the hyps 
+ * on the right side [right] if [toleft=false].
+ * If [with_dep] then dependent hypotheses are moved accordingly. *)
+
+let split_sign hfrom hto l =
+  let rec splitrec left toleft = function
+    | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom))
+    | (hyp,c,typ) as d :: right ->
+      	if hyp = hfrom then 
+	  (left,right,d,toleft) 
+      	else 
+	  splitrec (d::left) (toleft or (hyp = hto)) right
+  in 
+  splitrec [] false l
+
+let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
+  let env = Global.env() in
+  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
+    if toleft
+    then occur_var_in_decl env hyp2 d
+    else occur_var_in_decl env hyp d2
+  in
+  let rec moverec first middle = function
+    | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
+    | (hyp,_,_) as d :: right ->
+	let (first',middle') =
+      	  if List.exists (test_dep d) middle then 
+	    if with_dep & (hyp <> hto) then 
+	      (first, d::middle)
+            else 
+	      error 
+		("Cannot move "^(string_of_id idfrom)^" after "
+		 ^(string_of_id hto)
+		 ^(if toleft then ": it occurs in " else ": it depends on ")
+		 ^(string_of_id hyp))
+          else 
+	    (d::first, middle)
+	in
+      	if hyp = hto then 
+	  (List.rev first')@(List.rev middle')@right
+      	else 
+	  moverec first' middle' right
+  in
+  if toleft then 
+    List.rev_append (moverec [] [declfrom] left) right
+  else 
+    List.rev_append left (moverec [] [declfrom] right)
+
+let check_backward_dependencies sign d =
+  if not (Idset.for_all
+	    (fun id -> mem_named_context id sign)
+	    (global_vars_set_of_decl (Global.env()) d))
+  then
+    error "Can't introduce at that location: free variable conflict"
+
+
+let check_forward_dependencies id tail =
+  let env = Global.env() in
+  List.iter
+    (function (id',_,_ as decl) ->
+       if occur_var_in_decl env id decl then
+	 error ((string_of_id id) ^ " is used in hypothesis " 
+		^ (string_of_id id')))
+    tail
+
+
+let rename_hyp id1 id2 sign =
+  apply_to_hyp_and_dependent_on sign id1
+    (fun (_,b,t) -> (id2,b,t))
+    (map_named_declaration (replace_vars [id1,mkVar id2]))
+
+let replace_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign _ tail ->
+       if !check then
+	 (check_backward_dependencies sign d;
+	  check_forward_dependencies id tail);
+       add_named_decl d sign)
+
+let insert_after_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign d' _ ->
+       if !check then check_backward_dependencies sign d;
+       add_named_decl d (add_named_decl d' sign))
+
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the logical rules *)
+
+(* Will only be used on terms given to the Refine rule which have meta 
+variables only in Application and Case *)
+
+let collect_meta_variables c = 
+  let rec collrec acc c = match kind_of_term c with
+    | Meta mv -> mv::acc
+    | Cast(c,_) -> collrec acc c
+    | (App _| Case _) -> fold_constr collrec acc c
+    | _ -> acc
+  in 
+  List.rev(collrec [] c)
+
+let check_conv_leq_goal env sigma arg ty conclty =
+  if !check & not (is_conv_leq env sigma ty conclty) then 
+    raise (RefinerError (BadType (arg,ty,conclty)))
+
+let goal_type_of env sigma c =
+  (if !check then type_of else Retyping.get_type_of) env sigma c
+
+let rec mk_refgoals sigma goal goalacc conclty trm =
+  let env = evar_env goal in
+  let hyps = goal.evar_hyps in
+(*
+   if  not (occur_meta trm) then
+    let t'ty = (unsafe_machine env sigma trm).uj_type in 	
+    let _ = conv_leq_goal env sigma trm t'ty conclty in
+      (goalacc,t'ty)
+  else
+*)
+  match kind_of_term trm with
+    | Meta _ ->
+	if occur_meta conclty then
+          raise (RefinerError (OccurMetaGoal conclty));
+	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
+
+    | Cast (t,ty) ->
+	check_typability env sigma ty;
+	check_conv_leq_goal env sigma trm ty conclty;
+	mk_refgoals sigma goal goalacc ty t
+
+    | App (f,l) ->
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc'',conclty') =
+	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
+	check_conv_leq_goal env sigma trm conclty' conclty;
+        (acc'',conclty')
+
+    | Case (_,p,c,lf) ->
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
+	check_conv_leq_goal env sigma trm conclty' conclty;
+	let acc'' = 
+	  array_fold_left2
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
+            acc' lbrty lf 
+	in
+	(acc'',conclty')
+
+    | _ -> 
+	if occur_meta trm then raise (RefinerError (OccurMeta trm));
+      	let t'ty = goal_type_of env sigma trm in
+	check_conv_leq_goal env sigma trm t'ty conclty;
+        (goalacc,t'ty)
+
+(* Same as mkREFGOALS but without knowing te type of the term. Therefore,
+ * Metas should be casted. *)
+
+and mk_hdgoals sigma goal goalacc trm =
+  let env = evar_env goal in
+  let hyps = goal.evar_hyps in
+  match kind_of_term trm with
+    | Cast (c,ty) when isMeta c ->
+	check_typability env sigma ty;
+	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
+
+    | App (f,l) ->
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	mk_arggoals sigma goal acc' hdty (Array.to_list l)
+
+    | Case (_,p,c,lf) ->
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
+	let acc'' = 
+	  array_fold_left2
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
+            acc' lbrty lf 
+	in
+	(acc'',conclty')
+
+    | _ -> goalacc, goal_type_of env sigma trm
+
+and mk_arggoals sigma goal goalacc funty = function
+  | [] -> goalacc,funty
+  | harg::tlargs as allargs ->
+      let t = whd_betadeltaiota (evar_env goal) sigma funty in
+      match kind_of_term t with
+	| Prod (_,c1,b) ->
+	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
+	    mk_arggoals sigma goal acc' (subst1 harg b) tlargs
+	| LetIn (_,c1,_,b) ->
+	    mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
+	| _ -> raise (RefinerError (CannotApply (t,harg)))
+
+and mk_casegoals sigma goal goalacc p c =
+  let env = evar_env goal in
+  let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
+  let (acc'',pt) = mk_hdgoals sigma goal acc' p in
+  let pj = {uj_val=p; uj_type=pt} in 
+  let indspec =
+    try find_mrectype env sigma ct
+    with Not_found -> anomaly "mk_casegoals" in
+  let (lbrty,conclty) =
+    type_case_branches_with_names env indspec pj c in
+  (acc'',lbrty,conclty)
+
+
+let error_use_instantiate () =
+  errorlabstrm "Logic.prim_refiner"
+    (str"cannot intro when there are open metavars in the domain type" ++
+       spc () ++ str"- use Instantiate")
+
+let convert_hyp sign sigma (id,b,bt as d) =
+  apply_to_hyp sign id
+    (fun sign (_,c,ct) _ ->
+       let env = Global.env_of_context sign in
+       if !check && not (is_conv env sigma bt ct) &&
+         not (option_compare (is_conv env sigma) b c) then
+	   error "convert-hyp rule passed non-converting term";
+       add_named_decl d sign)
+
+
+(************************************************************************)
+(************************************************************************)
+(* Primitive tactics are handled here *)
+
+let prim_refiner r sigma goal =
+  let env = evar_env goal in
+  let sign = goal.evar_hyps in
+  let cl = goal.evar_concl in
+  match r with
+    (* Logical rules *)
+    | Intro id ->
+    	if !check && mem_named_context id sign then
+	  error "New variable is already declared";
+        (match kind_of_term (strip_outer_cast cl) with
+	   | Prod (_,c1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let sg = mk_goal (add_named_decl (id,None,c1) sign)
+			  (subst1 (mkVar id) b) in
+	       [sg]
+	   | LetIn (_,c1,t1,b) ->
+	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
+	       let sg =
+		 mk_goal (add_named_decl (id,Some c1,t1) sign)
+		   (subst1 (mkVar id) b) in
+	       [sg]
+	   | _ ->
+	       raise (RefinerError IntroNeedsProduct))
+	
+    | Intro_replacing id ->
+	(match kind_of_term (strip_outer_cast cl) with
+           | Prod (_,c1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let sign' = replace_hyp sign id (id,None,c1) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
+	       [sg]
+           | LetIn (_,c1,t1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let sign' = replace_hyp sign id (id,Some c1,t1) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
+	       [sg]
+	   | _ ->
+	       raise (RefinerError IntroNeedsProduct))
+	
+    | Cut (b,id,t) ->
+    	if !check && mem_named_context id sign then
+	  error "New variable is already declared";
+        if occur_meta t then error_use_instantiate();
+        let sg1 = mk_goal sign (nf_betaiota t) in
+        let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in
+        if b then [sg1;sg2] else [sg2;sg1]  
+
+    | FixRule (f,n,rest) ->
+     	let rec check_ind env k cl = 
+          match kind_of_term (strip_outer_cast cl) with 
+            | Prod (na,c1,b) -> 
+            	if k = 1 then 
+		  try 
+		    fst (find_inductive env sigma c1)
+		  with Not_found -> 
+		    error "cannot do a fixpoint on a non inductive type"
+            	else 
+		  check_ind (push_rel (na,None,c1) env) (k-1) b
+            | _ -> error "not enough products"
+	in
+	let (sp,_) = check_ind env n cl in
+	let all = (f,n,cl)::rest in
+     	let rec mk_sign sign = function 
+	  | (f,n,ar)::oth ->
+	      let (sp',_)  = check_ind env n ar in 
+	      if not (sp=sp') then 
+		error ("fixpoints should be on the same " ^ 
+		       "mutual inductive declaration");
+	      if !check && mem_named_context f sign then 
+		error "name already used in the environment";
+	      mk_sign (add_named_decl (f,None,ar) sign) oth
+	  | [] -> 
+	      List.map (fun (_,_,c) -> mk_goal sign c) all
+	in 
+	mk_sign sign all
+	
+    | Cofix (f,others) ->
+     	let rec check_is_coind env cl = 
+	  let b = whd_betadeltaiota env sigma cl in
+          match kind_of_term b with
+            | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
+            | _ -> 
+		try 
+		  let _ = find_coinductive env sigma b in ()
+                with Not_found -> 
+		  error ("All methods must construct elements " ^
+			  "in coinductive types")
+	in
+	let all = (f,cl)::others in
+     	List.iter (fun (_,c) -> check_is_coind env c) all;
+        let rec mk_sign sign = function 
+          | (f,ar)::oth ->
+	      (try
+                (let _ = Sign.lookup_named f sign in
+                error "name already used in the environment")
+              with
+              |	Not_found ->
+                  mk_sign (add_named_decl (f,None,ar) sign) oth)
+	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
+     	in 
+	mk_sign sign all
+
+    | Refine c ->
+        if not (list_distinct (collect_meta_variables c)) then
+          raise (RefinerError (NonLinearProof c));
+	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
+	let sgl = List.rev sgl in
+	sgl
+
+    (* Conversion rules *)
+    | Convert_concl cl' ->
+	check_typability env sigma cl';
+	if (not !check) || is_conv_leq env sigma cl' cl then
+          let sg = mk_goal sign cl' in
+          [sg]
+	else 
+	  error "convert-concl rule passed non-converting term"
+
+    | Convert_hyp (id,copt,ty) ->
+	[mk_goal (convert_hyp sign sigma (id,copt,ty)) cl]
+
+    (* And now the structural rules *)
+    | Thin ids -> 
+	[clear_hyps ids goal]
+
+    | ThinBody ids ->
+	let clear_aux env id =
+          let env' = remove_hyp_body env sigma id in
+          if !check then recheck_typability (None,id) env' sigma cl;
+          env'
+	in
+	let sign' = named_context (List.fold_left clear_aux env ids) in
+     	let sg = mk_goal sign' cl in
+     	[sg]
+
+    | Move (withdep, hfrom, hto) ->
+  	let (left,right,declfrom,toleft) = split_sign hfrom hto sign in
+  	let hyps' = 
+	  move_after withdep toleft (left,declfrom,right) hto in
+  	[mk_goal hyps' cl]
+
+    | Rename (id1,id2) ->
+        if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then
+          error ((string_of_id id2)^" is already used");
+        let sign' = rename_hyp id1 id2 sign in
+        let cl' = replace_vars [id1,mkVar id2] cl in
+        [mk_goal sign' cl']
+
+(************************************************************************)
+(************************************************************************)
+(* Extracting a proof term from the proof tree *)
+
+(* Util *)
+let rec rebind id1 id2 = function
+  | [] -> []
+  | id::l -> 
+      if id = id1 then id2::l else
+        let l' = rebind id1 id2 l in
+        if id = id2 then
+          (* TODO: find a more elegant way to hide a variable *)
+          (id_of_string "_@")::l'
+        else id::l'
+
+let prim_extractor subfun vl pft =
+  let cl = pft.goal.evar_concl in
+  match pft.ref with
+    | Some (Prim (Intro id), [spf]) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | Prod (_,ty,_) ->
+	       let cty = subst_vars vl ty in
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | LetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
+	   | _ -> error "incomplete proof!")
+	
+    | Some (Prim (Intro_replacing id),[spf]) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | Prod (_,ty,_) ->
+	       let cty = subst_vars vl ty in
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | LetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
+	   | _ -> error "incomplete proof!")
+
+    | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
+        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)
+
+    | Some (Prim (FixRule (f,n,others)),spfl) ->
+	let all = Array.of_list ((f,n,cl)::others) in
+	let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all in
+	let names = Array.map (fun (f,_,_) -> Name f) all in
+	let vn = Array.map (fun (_,n,_) -> n-1) all in
+	let newvl = List.fold_left (fun vl (id,_,_)->(id::vl)) (f::vl)others in
+	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+	mkFix ((vn,0),(names,lcty,lfix))	
+
+    | Some (Prim (Cofix (f,others)),spfl) ->
+	let all = Array.of_list ((f,cl)::others) in
+	let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all in
+	let names  = Array.map (fun (f,_) -> Name f) all in
+	let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (f::vl) others in 
+	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+	mkCoFix (0,(names,lcty,lfix))
+	  
+    | Some (Prim (Refine c),spfl) ->
+	let mvl = collect_meta_variables c in
+	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
+	let cc = subst_vars vl c in 
+	plain_instance metamap cc
+
+    (* Structural and conversion rules do not produce any proof *)
+    | Some (Prim (Convert_concl _),[pf]) ->
+	subfun vl pf
+	
+    | Some (Prim (Convert_hyp _),[pf]) ->
+	subfun vl pf
+
+    | Some (Prim (Thin _),[pf]) ->
+     (* No need to make ids Anonymous in vl: subst_vars take the more recent *)
+	subfun vl pf
+	
+    | Some (Prim (ThinBody _),[pf]) ->
+	subfun vl pf
+	
+    | Some (Prim (Move _),[pf]) ->
+	subfun vl pf
+
+    | Some (Prim (Rename (id1,id2)),[pf]) ->
+	subfun (rebind id1 id2 vl) pf
+
+    | Some _ -> anomaly "prim_extractor"
+
+    | None-> error "prim_extractor handed incomplete proof"
+	  
+(* Pretty-printer *)
+
+open Printer
+
+let prterm x = prterm_env (Global.env()) x
+
+let pr_prim_rule_v7 = function
+  | Intro id -> 
+      str"Intro " ++ pr_id id
+	
+  | Intro_replacing id -> 
+      (str"intro replacing "  ++ pr_id id)
+	
+  | Cut (b,id,t) ->
+      if b then
+        (str"Assert " ++ prterm t)
+      else
+        (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
+	
+  | FixRule (f,n,[]) ->
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n)
+      
+  | FixRule (f,n,others) -> 
+      let rec print_mut = function
+	| (f,n,ar)::oth -> 
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
+        | [] -> mt () in
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[]) ->
+      (str"Cofix " ++ pr_id f)
+
+  | Cofix (f,others) ->
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"Cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+
+  | Refine c -> 
+      str(if occur_meta c then "Refine " else "Exact ") ++
+      Constrextern.with_meta_as_hole prterm c
+      
+  | Convert_concl c ->
+      (str"Change "  ++ prterm c)
+      
+  | Convert_hyp (id,None,t) ->
+      (str"Change "  ++ prterm t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (Type of "  ++ pr_id id ++ str ")")
+      
+  | Thin ids ->
+      (str"Clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | ThinBody ids ->
+      (str"ClearBody "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "Dependent " else "") ++
+	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | Rename (id1,id2) ->
+      (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+let pr_prim_rule_v8 = function
+  | Intro id -> 
+      str"intro " ++ pr_id id
+	
+  | Intro_replacing id -> 
+      (str"intro replacing "  ++ pr_id id)
+	
+  | Cut (b,id,t) ->
+      if b then
+        (str"assert " ++ prterm t)
+      else
+        (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+	
+  | FixRule (f,n,[]) ->
+      (str"fix " ++ pr_id f ++ str"/" ++ int n)
+      
+  | FixRule (f,n,others) -> 
+      let rec print_mut = function
+	| (f,n,ar)::oth -> 
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
+        | [] -> mt () in
+      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[]) ->
+      (str"cofix " ++ pr_id f)
+
+  | Cofix (f,others) ->
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+
+  | Refine c -> 
+      str(if occur_meta c then "refine " else "exact ") ++
+      Constrextern.with_meta_as_hole prterm c
+      
+  | Convert_concl c ->
+      (str"change "  ++ prterm c)
+      
+  | Convert_hyp (id,None,t) ->
+      (str"change "  ++ prterm t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"change "  ++ prterm c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
+      
+  | Thin ids ->
+      (str"clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | ThinBody ids ->
+      (str"clearbody "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "dependent " else "") ++
+	 str"move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | Rename (id1,id2) ->
+      (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+let pr_prim_rule t =
+  if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t
diff --git a/proofs/logic.mli b/proofs/logic.mli
new file mode 100644
index 00000000..7eef22bd
--- /dev/null
+++ b/proofs/logic.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: logic.mli,v 1.27.6.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Evd
+open Environ
+open Proof_type
+(*i*)
+
+(* This suppresses check done in [prim_refiner] for the tactic given in
+   argument; works by side-effect *)
+
+val without_check : tactic -> tactic
+val with_check    : tactic -> tactic
+
+(* [without_check] respectively means:\\
+  [Intro]: no check that the name does not exist\\
+  [Intro_after]: no check that the name does not exist and that variables in
+     its type does not escape their scope\\
+  [Intro_replacing]: no check that the name does not exist and that 
+     variables in its type does not escape their scope\\
+  [Convert_hyp]: 
+  no check that the name exist and that its type is convertible\\
+*)
+
+(* The primitive refiner. *)
+
+val prim_refiner : prim_rule -> evar_map -> goal -> goal list
+
+val prim_extractor :
+  (identifier list -> proof_tree -> constr)
+  -> identifier list -> proof_tree -> constr
+
+(*s Refiner errors. *)
+
+type refiner_error =
+
+  (*i Errors raised by the refiner i*)
+  | BadType of constr * constr * constr
+  | OccurMeta of constr
+  | OccurMetaGoal of constr
+  | CannotApply of constr * constr
+  | NotWellTyped of constr
+  | NonLinearProof of constr
+
+  (*i Errors raised by the tactics i*)
+  | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
+  | CannotGeneralize of constr
+  | IntroNeedsProduct
+  | DoesNotOccurIn of constr * identifier
+  | NoOccurrenceFound of constr
+
+exception RefinerError of refiner_error
+
+val error_cannot_unify : constr * constr -> 'a
+
+val catchable_exception : exn -> bool
+
+
+(*s Pretty-printer. *)
+
+val pr_prim_rule   : prim_rule -> Pp.std_ppcmds
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
new file mode 100644
index 00000000..f53ea870
--- /dev/null
+++ b/proofs/pfedit.ml
@@ -0,0 +1,333 @@
+(************************************************************************)
+(*  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: pfedit.ml,v 1.47.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Sign
+open Term
+open Declarations
+open Entries
+open Environ
+open Evd
+open Typing
+open Tacmach
+open Proof_trees
+open Tacexpr
+open Proof_type
+open Lib
+open Safe_typing
+
+(*********************************************************************)
+(* Managing the proofs state                                         *)
+(* Mainly contributed by C. Murthy                                   *)
+(*********************************************************************)
+
+type proof_topstate = {
+  mutable top_end_tac : tactic option;
+  top_hyps : named_context * named_context;
+  top_goal : goal;
+  top_strength : Decl_kinds.goal_kind;
+  top_hook : declaration_hook }
+
+let proof_edits =
+  (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)
+
+let get_all_proof_names () = Edit.dom proof_edits
+
+let msg_proofs use_resume =
+  match Edit.dom proof_edits with
+    | [] -> (spc () ++ str"(No proof-editing in progress).")
+    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
+               (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++
+	       str"." ++
+               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
+              	else (mt ()))
+)
+
+let undo_default = 50
+let undo_limit = ref undo_default
+
+(*********************************************************************)
+(*    Functions for decomposing and modifying the proof state        *)
+(*********************************************************************)
+
+let get_state () =
+  match Edit.read proof_edits with
+    | None -> errorlabstrm "Pfedit.get_state"
+          (str"No focused proof" ++ msg_proofs true)
+    | Some(_,pfs,ts) -> (pfs,ts)
+
+let get_topstate ()    = snd(get_state())
+let get_pftreestate () = fst(get_state())
+
+let get_end_tac () = let ts = get_topstate () in ts.top_end_tac
+
+let get_goal_context n =
+  let pftree = get_pftreestate () in
+  let goal = nth_goal_of_pftreestate n pftree in
+  (project goal, pf_env goal)
+
+let get_current_goal_context () = get_goal_context 1
+
+let set_current_proof = Edit.focus proof_edits
+
+let resume_proof (loc,id) = 
+  try 
+    Edit.focus proof_edits id
+  with Invalid_argument "Edit.focus" ->
+    user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
+
+let suspend_proof () =
+  try 
+    Edit.unfocus proof_edits
+  with Invalid_argument "Edit.unfocus" ->
+    errorlabstrm "Pfedit.suspend_current_proof"
+      (str"No active proof" ++ (msg_proofs true))
+      
+let resume_last_proof () =
+  match (Edit.last_focused proof_edits) with
+    | None ->
+        errorlabstrm "resume_last" (str"No proof-editing in progress.")
+    | Some p -> 
+	Edit.focus proof_edits p
+	  
+let get_current_proof_name () =
+  match Edit.read proof_edits with
+    | None ->
+        errorlabstrm "Pfedit.get_proof"
+          (str"No focused proof" ++ msg_proofs true)
+    | Some(na,_,_) -> na
+
+let add_proof (na,pfs,ts) =
+  Edit.create proof_edits (na,pfs,ts,!undo_limit+1)
+
+let delete_proof_gen = Edit.delete proof_edits
+
+let delete_proof (loc,id) =
+  try 
+    delete_proof_gen id
+  with (UserError ("Edit.delete",_)) ->
+    user_err_loc
+      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+      
+let init_proofs () = Edit.clear proof_edits
+		       
+let mutate f =
+  try 
+    Edit.mutate proof_edits (fun _ pfs -> f pfs)
+  with Invalid_argument "Edit.mutate" ->
+    errorlabstrm "Pfedit.mutate"
+      (str"No focused proof" ++ msg_proofs true)
+
+let start (na,ts) =
+  let pfs = mk_pftreestate ts.top_goal in 
+  add_proof(na,pfs,ts)
+    
+let restart_proof () =
+  match Edit.read proof_edits with
+    | None -> 
+	errorlabstrm "Pfedit.restart"
+          (str"No focused proof to restart" ++ msg_proofs true)
+    | Some(na,_,ts) -> 
+	delete_proof_gen na;
+        start (na,ts);
+        set_current_proof na
+
+let proof_term () =
+  extract_pftreestate (get_pftreestate())
+    
+(* Detect is one has completed a subtree of the initial goal *)
+let subtree_solved () = 
+  let pts = get_pftreestate () in
+  is_complete_proof (proof_of_pftreestate pts) & 
+  not (is_top_pftreestate pts)
+
+(*********************************************************************)
+(*                 Undo functions                                    *)
+(*********************************************************************)
+
+let set_undo = function
+  | None -> undo_limit := undo_default
+  | Some n -> 
+      if n>=0 then 
+	undo_limit := n
+      else 
+	error "Cannot set a negative undo limit"
+
+let get_undo () = Some !undo_limit
+
+let undo n =
+  try 
+    Edit.undo proof_edits n; 
+       (* needed because the resolution of a subtree is done in 2 steps 
+       then a sequence of undo can lead to a focus on a completely solved 
+       subtree - this solution only works properly if undoing one step *)
+    if subtree_solved() then  Edit.undo proof_edits 1
+  with (Invalid_argument "Edit.undo") ->
+    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
+
+(*********************************************************************)
+(*                  Proof cooking                                    *)
+(*********************************************************************)
+
+let xml_cook_proof = ref (fun _ -> ())
+let set_xml_cook_proof f = xml_cook_proof := f
+
+let cook_proof () =
+  let (pfs,ts) = get_state() 
+  and ident = get_current_proof_name () in
+  let {evar_concl=concl} = ts.top_goal 
+  and strength = ts.top_strength in
+  let pfterm = extract_pftreestate pfs in
+  !xml_cook_proof (strength,pfs);
+  (ident,
+   ({ const_entry_body = pfterm;
+      const_entry_type = Some concl;
+      const_entry_opaque = true },
+    strength, ts.top_hook))
+
+let current_proof_statement () = 
+  let ts = get_topstate() in
+  (get_current_proof_name (), ts.top_strength, 
+   ts.top_goal.evar_concl, ts.top_hook)
+
+(*********************************************************************)
+(*              Abort   functions                                    *)
+(*********************************************************************)
+ 
+let refining () = [] <> (Edit.dom proof_edits)
+
+let check_no_pending_proofs () =
+  if refining () then 
+    errorlabstrm "check_no_pending_proofs"
+      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+         str"Use \"Abort All\" first or complete proof(s).")
+
+let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
+
+let delete_all_proofs = init_proofs
+
+(*********************************************************************)
+(*   Modifying the end tactic of the current profftree               *)
+(*********************************************************************)
+let set_end_tac tac =
+  let top = get_topstate () in
+  top.top_end_tac <- Some tac
+
+(*********************************************************************)
+(*              Modifying the current prooftree                      *)
+(*********************************************************************)
+
+let start_proof na str sign concl hook =
+  let top_goal = mk_goal sign concl in
+  let ts = { 
+    top_end_tac = None;
+    top_hyps = (sign,empty_named_context);
+    top_goal = top_goal;
+    top_strength = str;
+    top_hook = hook}
+  in
+  start(na,ts);
+  set_current_proof na
+
+
+let solve_nth k tac =
+  let pft = get_pftreestate () in
+  if not (List.mem (-1) (cursor_of_pftreestate pft)) then
+    mutate (solve_nth_pftreestate k tac)
+  else 
+    error "cannot apply a tactic when we are descended behind a tactic-node"
+
+let by tac = mutate (solve_pftreestate tac)
+
+let instantiate_nth_evar_com n c =
+  mutate (Evar_refiner.instantiate_pf_com n c)
+
+let traverse n = mutate (traverse n)
+ 
+(* [traverse_to path]
+
+   Traverses the current proof to get to the location specified by
+   [path].
+
+   ALGORITHM: The algorithm works on reversed paths. One just has to remove
+   the common part on the reversed paths.
+
+*)
+
+let common_ancestor l1 l2 =
+  let rec common_aux l1 l2 =
+    match l1, l2 with
+      | a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2'
+      | _, _ -> List.rev l1, List.length l2
+  in
+  common_aux (List.rev l1) (List.rev l2)
+      
+let rec traverse_up = function
+  | 0 -> (function pf -> pf)
+  | n -> (function pf -> Tacmach.traverse 0 (traverse_up (n - 1) pf))
+
+let rec traverse_down = function
+  | [] -> (function pf -> pf)
+  | n::l -> (function pf -> Tacmach.traverse n (traverse_down l pf))
+
+let traverse_to path =
+  let up_and_down path pfs =
+    let cursor = cursor_of_pftreestate pfs in
+    let down_list, up_count = common_ancestor path cursor in
+    traverse_down down_list (traverse_up up_count pfs)
+  in
+  mutate (up_and_down path)
+
+(* traverse the proof tree until it reach the nth subgoal *)
+let traverse_nth_goal n = mutate (nth_unproven n)
+
+let traverse_prev_unproven () = mutate prev_unproven
+
+let traverse_next_unproven () = mutate next_unproven
+
+
+(* The goal focused on *)
+let focus_n = ref 0
+let make_focus n = focus_n := n
+let focus () = !focus_n
+let focused_goal () = let n = !focus_n in if n=0 then 1 else n
+
+let reset_top_of_tree () = 
+  let pts = get_pftreestate () in 
+  if not (is_top_pftreestate pts) then mutate top_of_tree
+
+(** Printers *)
+
+let pr_subgoals_of_pfts pfts = 
+  let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
+  let sigma = project (top_goal_of_pftreestate pfts) in
+  pr_subgoals_existential sigma gls
+
+let pr_open_subgoals () =
+  let pfts = get_pftreestate () in
+  match focus() with
+    | 0 -> 
+	pr_subgoals_of_pfts pfts
+    | n -> 
+	let pf = proof_of_pftreestate pfts in
+	let gls = fst (frontier pf) in 
+	assert (n > List.length gls);
+	if List.length gls < 2 then 
+	  pr_subgoal n gls
+	else 
+	  v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
+	  pr_subgoal n gls)
+
+let pr_nth_open_subgoal n =
+  let pf = proof_of_pftreestate (get_pftreestate ()) in
+  pr_subgoal n (fst (frontier pf))
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
new file mode 100644
index 00000000..e95881ba
--- /dev/null
+++ b/proofs/pfedit.mli
@@ -0,0 +1,183 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: pfedit.mli,v 1.35.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+open Decl_kinds
+open Tacmach
+open Tacexpr
+(*i*)
+
+(*s Several proofs can be opened simultaneously but at most one is
+   focused at some time. The following functions work by side-effect
+   on current set of open proofs. In this module, ``proofs'' means an
+   open proof (something started by vernacular command [Goal], [Lemma]
+   or [Theorem]), and ``goal'' means a subgoal of the current focused
+   proof *)
+
+(*s [refining ()] tells if there is some proof in progress, even if a not
+   focused one *)
+
+val refining : unit -> bool
+
+(* [check_no_pending_proofs ()] fails if there is still some proof in
+   progress *)
+
+val check_no_pending_proofs : unit -> unit
+
+(*s [delete_proof name] deletes proof of name [name] or fails if no proof
+    has this name *)
+
+val delete_proof : identifier located -> unit
+
+(* [delete_current_proof ()] deletes current focused proof or fails if
+    no proof is focused *)
+
+val delete_current_proof : unit -> unit
+
+(* [delete_all_proofs ()] deletes all open proofs if any *)
+
+val delete_all_proofs : unit -> unit
+
+(*s [undo n] undoes the effect of the last [n] tactics applied to the
+    current proof; it fails if no proof is focused or if the ``undo''
+    stack is exhausted *)
+
+val undo : int -> unit
+
+(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
+   sets the size to the default value (12) *)
+
+val set_undo : int option -> unit
+val get_undo : unit -> int option
+
+(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion
+    [t]; [hook] is optionally a function to be applied at proof end (e.g. to
+    declare the built constructions as a coercion or a setoid morphism) *)
+
+val start_proof : 
+  identifier -> goal_kind -> named_context -> constr
+    -> declaration_hook -> unit
+
+(* [restart_proof ()] restarts the current focused proof from the beginning
+   or fails if no proof is focused *)
+
+val restart_proof : unit -> unit
+
+(*s [resume_last_proof ()] focus on the last unfocused proof or fails
+   if there is no suspended proofs *)
+
+val resume_last_proof : unit -> unit
+
+(* [resume_proof name] focuses on the proof of name [name] or
+   raises [UserError] if no proof has name [name] *)
+
+val resume_proof : identifier located -> unit
+
+(* [suspend_proof ()] unfocuses the current focused proof or
+   failed with [UserError] if no proof is currently focused *)
+
+val suspend_proof : unit -> unit
+
+(*s [cook_proof opacity] turns the current proof (assumed completed) into
+    a constant with its name, kind and possible hook (see [start_proof]);
+    it fails if there is no current proof of if it is not completed *)
+
+val cook_proof : unit -> 
+  identifier * (Entries.definition_entry * goal_kind * declaration_hook)
+
+(* To export completed proofs to xml *)
+val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
+
+(*s [get_pftreestate ()] returns the current focused pending proof or
+   raises [UserError "no focused proof"] *)
+
+val get_pftreestate : unit -> pftreestate
+
+(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
+
+val get_end_tac : unit -> tactic option
+
+(* [get_goal_context n] returns the context of the [n]th subgoal of
+   the current focused proof or raises a [UserError] if there is no
+   focused proof or if there is no more subgoals *)
+
+val get_goal_context : int -> Evd.evar_map * env
+
+(* [get_current_goal_context ()] works as [get_goal_context 1] *)
+
+val get_current_goal_context : unit -> Evd.evar_map * env
+
+(* [current_proof_statement] *)
+
+val current_proof_statement :
+  unit -> identifier * goal_kind * types * declaration_hook
+
+(*s [get_current_proof_name ()] return the name of the current focused
+    proof or failed if no proof is focused *)
+
+val get_current_proof_name : unit -> identifier
+
+(* [get_all_proof_names ()] returns the list of all pending proof names *)
+
+val get_all_proof_names : unit -> identifier list
+
+(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
+    by [solve_nth] *)
+
+val set_end_tac : tactic -> unit
+
+(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
+   current focused proof or raises a UserError if no proof is focused or
+   if there is no [n]th subgoal *)
+
+val solve_nth : int -> tactic -> unit
+
+(* [by tac] applies tactic [tac] to the 1st subgoal of the current
+   focused proof or raises a UserError if there is no focused proof or
+   if there is no more subgoals *)
+
+val by : tactic -> unit
+
+(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
+   existential variable of the current focused proof by [c] or raises a
+   UserError if no proof is focused or if there is no such [n]th
+   existential variable *)
+
+val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
+
+(*s To deal with subgoal focus *)
+
+val make_focus : int -> unit
+val focus : unit -> int
+val focused_goal : unit -> int
+val subtree_solved : unit -> bool
+
+val reset_top_of_tree : unit -> unit
+val traverse : int -> unit
+val traverse_nth_goal : int -> unit
+val traverse_next_unproven : unit -> unit
+val traverse_prev_unproven : unit -> unit
+
+
+(* These two functions make it possible to implement more elaborate
+   proof and goal management, as it is done, for instance in pcoq *)
+val traverse_to : int list -> unit
+val mutate : (pftreestate -> pftreestate) -> unit
+
+(** Printers *)
+
+val pr_open_subgoals    : unit -> std_ppcmds
+val pr_nth_open_subgoal : int -> std_ppcmds
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
new file mode 100644
index 00000000..aaf54a36
--- /dev/null
+++ b/proofs/proof_trees.ml
@@ -0,0 +1,253 @@
+(************************************************************************)
+(*  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: proof_trees.ml,v 1.53.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Closure
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Evd
+open Environ
+open Evarutil
+open Proof_type
+open Tacred
+open Typing
+open Libnames
+open Nametab
+
+(*
+let is_bind = function
+  | Tacexpr.Cbindings _ -> true
+  | _ -> false
+*)
+
+(* Functions on goals *)
+
+let mk_goal hyps cl = 
+  { evar_hyps = hyps; evar_concl = cl; 
+    evar_body = Evar_empty}
+
+(* Functions on proof trees *)
+
+let ref_of_proof pf =
+  match pf.ref with
+    | None -> failwith "rule_of_proof"
+    | Some r -> r
+
+let rule_of_proof pf =
+  let (r,_) = ref_of_proof pf in r
+
+let children_of_proof pf = 
+  let (_,cl) = ref_of_proof pf in cl
+				    
+let goal_of_proof pf = pf.goal
+
+let subproof_of_proof pf = match pf.ref with
+  | Some (Tactic (_,pf), _) -> pf
+  | _ -> failwith "subproof_of_proof"
+
+let status_of_proof pf = pf.open_subgoals
+
+let is_complete_proof pf = pf.open_subgoals = 0
+
+let is_leaf_proof pf = (pf.ref = None)
+
+let is_tactic_proof pf = match pf.ref with
+  | Some (Tactic _, _) -> true
+  | _ -> false
+
+
+(*******************************************************************)
+(*            Constraints for existential variables                *)
+(*******************************************************************)
+
+(* A readable constraint is a global constraint plus a focus set
+   of existential variables and a signature. *)
+
+(* Functions on readable constraints *)
+			     
+let mt_evcty gc = 
+  { it = empty_named_context; sigma = gc }
+
+let rc_of_gc evds gl = 
+  { it = gl.evar_hyps; sigma = evds }
+
+let rc_add evc (k,v) = 
+  { it  = evc.it;
+    sigma = Evd.add evc.sigma k v }
+
+let get_hyps  evc = evc.it
+let get_env   evc = Global.env_of_context evc.it
+let get_gc    evc = evc.sigma
+
+let pf_lookup_name_as_renamed env ccl s =
+  Detyping.lookup_name_as_renamed env ccl s
+
+let pf_lookup_index_as_renamed env ccl n =
+  Detyping.lookup_index_as_renamed env ccl n
+
+(*********************************************************************)
+(*                  Pretty printing functions                        *)
+(*********************************************************************)
+
+open Pp
+open Printer
+
+(* Il faudrait parametrer toutes les pr_term, term_env, etc. par la
+  strategie de renommage choisie pour Termast (en particulier, il
+  faudrait pouvoir etre sur que lookup_as_renamed qui est utilisé par
+  Intros Until fonctionne exactement comme on affiche le but avec
+  term_env *)
+
+let pf_lookup_name_as_renamed hyps ccl s =
+  Detyping.lookup_name_as_renamed hyps ccl s
+
+let pf_lookup_index_as_renamed ccl n =
+  Detyping.lookup_index_as_renamed ccl n
+
+let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+
+let pr_goal g =
+  let env = evar_env g in
+  let penv = pr_context_of env in
+  let pc = prterm_env_at_top env g.evar_concl in
+  str"  " ++ hv 0 (penv ++ fnl () ++
+		   str (emacs_str (String.make 1 (Char.chr 253)))  ++
+                   str "============================" ++ fnl ()  ++
+                   str" "  ++ pc) ++ fnl ()
+
+let pr_concl n g =
+  let env = evar_env g in
+  let pc = prterm_env_at_top env g.evar_concl in
+  str (emacs_str (String.make 1 (Char.chr 253)))  ++
+  str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+
+(* print the subgoals but write Subtree proved! even in case some existential 
+   variables remain unsolved, pr_subgoals_existential is a safer version 
+   of pr_subgoals *)
+
+let pr_subgoals = function
+  | [] -> (str"Proof completed." ++ fnl ())
+  | [g] ->
+      let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
+  | g1::rest ->
+      let rec pr_rec n = function
+        | [] -> (mt ())
+        | g::rest ->
+            let pg = pr_concl n g in
+            let prest = pr_rec (n+1) rest in
+            (cut () ++ pg ++ prest) 
+      in
+      let pg1 = pr_goal g1 in
+      let pgr = pr_rec 2 rest in
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ pgr)
+
+let pr_subgoal n =
+  let rec prrec p = function
+    | [] -> error "No such goal"
+    | g::rest ->
+       	if p = 1 then
+          let pg = pr_goal g in
+          v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
+       	else 
+	  prrec (p-1) rest
+  in 
+  prrec n
+
+let pr_seq evd = 
+  let env = evar_env evd
+  and cl = evd.evar_concl
+  in
+  let pdcl = pr_named_context_of env in
+  let pcl = prterm_env_at_top env cl in
+  hov 0 (pdcl  ++ spc ()  ++ hov 0 (str"|- "  ++ pcl))
+
+let prgl gl =
+  let pgl = pr_seq gl in
+  (str"["  ++ pgl  ++ str"]"  ++ spc ())
+
+let pr_evgl gl =
+  let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in
+  let pc = prterm gl.evar_concl in
+  hov 0 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pc ++ str"]")
+
+let pr_evgl_sign gl = 
+  let ps = pr_named_context_of (evar_env gl) in
+  let pc = prterm gl.evar_concl in
+  hov 0 (str"["  ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]")
+
+(*  evd.evgoal.lc seems to be printed twice *)
+let pr_decl evd =
+  let pevgl = pr_evgl evd in
+  let pb =
+    match evd.evar_body with
+      | Evar_empty -> (fnl ())
+      | Evar_defined c -> let pc = prterm c in (str" => "  ++ pc ++  fnl ())
+  in
+  h 0 (pevgl ++ pb)
+
+let pr_evd evd = 
+  prlist_with_sep pr_fnl
+    (fun (ev,evd) ->
+       let pe = pr_decl evd in 
+       h 0 (str (string_of_existential ev)  ++ str"=="  ++ pe))
+    (Evd.to_list evd)
+    
+let pr_decls decls = pr_evd decls
+		       
+let pr_evc evc =
+  let pe = pr_evd evc.sigma in
+  (pe)
+
+let pr_evars = 
+  prlist_with_sep pr_fnl
+    (fun (ev,evd) ->
+       let pegl = pr_evgl_sign evd in 
+       (str (string_of_existential ev) ++ str " : " ++ pegl))
+
+(* Print an enumerated list of existential variables *)
+let rec pr_evars_int i = function
+  | [] -> (mt ())
+  | (ev,evd)::rest ->
+      let pegl = pr_evgl_sign evd in 
+      let pei = pr_evars_int (i+1) rest in
+      (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
+              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++ 
+      fnl () ++ pei
+
+(* Equivalent to pr_subgoals but start from the prooftree and 
+   check for uninstantiated existential variables *)
+
+let pr_subgoals_existential sigma = function 
+  | [] -> 
+      let exl = Evd.non_instantiated sigma in 
+      if exl = [] then 
+	(str"Proof completed."  ++ fnl ())
+      else
+        let pei = pr_evars_int 1 exl in
+        (str "No more subgoals but non-instantiated existential " ++
+           str "variables :"  ++fnl () ++ (hov 0 pei))
+  | [g] ->
+      let pg = pr_goal g in
+      v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
+  | g1::rest ->
+      let rec pr_rec n = function
+        | [] -> (mt ())
+        | g::rest ->
+            let pc = pr_concl n g in
+            let prest = pr_rec (n+1) rest in
+            (cut () ++ pc ++ prest) 
+      in
+      let pg1 = pr_goal g1 in
+      let prest = pr_rec 2 rest in
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
+	   ++ pg1 ++ prest ++ fnl ())
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
new file mode 100644
index 00000000..c31d5207
--- /dev/null
+++ b/proofs/proof_trees.mli
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: proof_trees.mli,v 1.27.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Evd
+open Environ
+open Proof_type
+(*i*)
+
+(* This module declares readable constraints, and a few utilities on
+   constraints and proof trees *)
+
+val mk_goal : named_context -> constr -> goal
+
+val rule_of_proof     : proof_tree -> rule
+val ref_of_proof      : proof_tree -> (rule * proof_tree list)
+val children_of_proof : proof_tree -> proof_tree list
+val goal_of_proof     : proof_tree -> goal
+val subproof_of_proof : proof_tree -> proof_tree
+val status_of_proof   : proof_tree -> int
+val is_complete_proof : proof_tree -> bool
+val is_leaf_proof     : proof_tree -> bool
+val is_tactic_proof   : proof_tree -> bool
+
+(*s A readable constraint is a global constraint plus a focus set
+    of existential variables and a signature. *)
+
+val rc_of_gc  : evar_map -> goal -> named_context sigma
+val rc_add    : named_context sigma -> existential_key * goal -> 
+  named_context sigma
+val get_hyps  : named_context sigma -> named_context
+val get_env   : named_context sigma -> env
+val get_gc    : named_context sigma -> evar_map
+
+val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val pf_lookup_index_as_renamed : env -> constr -> int -> int option
+
+
+(*s Pretty printing functions. *)
+
+(*i*)
+open Pp
+(*i*)
+
+val pr_goal      : goal -> std_ppcmds
+val pr_subgoals  : goal list -> std_ppcmds
+val pr_subgoal   : int -> goal list -> std_ppcmds
+
+val pr_decl      : goal -> std_ppcmds
+val pr_decls     : evar_map -> std_ppcmds
+val pr_evc       : named_context sigma -> std_ppcmds
+
+val prgl         : goal -> std_ppcmds
+val pr_seq       : goal -> std_ppcmds
+val pr_evars     : (existential_key * goal) list -> std_ppcmds
+val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds
+val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
new file mode 100644
index 00000000..cbed5e27
--- /dev/null
+++ b/proofs/proof_type.ml
@@ -0,0 +1,101 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: proof_type.ml,v 1.29.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+(*i*)
+open Environ
+open Evd
+open Names
+open Libnames
+open Term
+open Util
+open Tacexpr
+open Rawterm
+open Genarg
+open Nametab
+open Pattern
+(*i*)
+
+(* This module defines the structure of proof tree and the tactic type. So, it
+   is used by Proof_tree and Refiner *)
+
+type prim_rule =
+  | Intro of identifier
+  | Intro_replacing of identifier
+  | Cut of bool * identifier * types
+  | FixRule of identifier * int * (identifier * int * constr) list
+  | Cofix of identifier * (identifier * constr) list
+  | Refine of constr
+  | Convert_concl of types
+  | Convert_hyp of named_declaration
+  | Thin of identifier list
+  | ThinBody of identifier list
+  | Move of bool * identifier * identifier
+  | Rename of identifier * identifier
+
+
+(* Signature useful to define the tactic type *)
+type 'a sigma = { 
+  it : 'a ; 
+  sigma : evar_map }
+
+(*s Proof trees. 
+  [ref] = [None] if the goal has still to be proved, 
+  and [Some (r,l)] if the rule [r] was applied to the goal
+  and gave [l] as subproofs to be completed. 
+  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
+  that the goal can be proven if the goals in [l] are solved. *)
+type proof_tree = {
+  open_subgoals : int;
+  goal : goal;
+  ref : (rule * proof_tree list) option }
+
+and rule =
+  | Prim of prim_rule
+  | Tactic of tactic_expr * proof_tree
+  | Change_evars
+
+and goal = evar_info
+
+and tactic = goal sigma -> (goal list sigma * validation)
+
+and validation = (proof_tree list -> proof_tree)
+
+and tactic_expr =
+  (constr,
+   constr_pattern,
+   evaluable_global_reference,
+   inductive,
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
+     Tacexpr.gen_tactic_expr
+
+and atomic_tactic_expr =
+  (constr,
+   constr_pattern,
+   evaluable_global_reference,
+   inductive,
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
+     Tacexpr.gen_atomic_tactic_expr
+
+and tactic_arg =
+  (constr,
+   constr_pattern,
+   evaluable_global_reference,
+   inductive,
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
+     Tacexpr.gen_tactic_arg
+
+type hyp_location = identifier Tacexpr.raw_hyp_location
+
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
new file mode 100644
index 00000000..42606552
--- /dev/null
+++ b/proofs/proof_type.mli
@@ -0,0 +1,128 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: proof_type.mli,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Environ
+open Evd
+open Names
+open Libnames
+open Term
+open Util
+open Tacexpr
+open Rawterm
+open Genarg
+open Nametab
+open Pattern
+(*i*)
+
+(* This module defines the structure of proof tree and the tactic type. So, it
+   is used by [Proof_tree] and [Refiner] *)
+
+type prim_rule =
+  | Intro of identifier
+  | Intro_replacing of identifier
+  | Cut of bool * identifier * types
+  | FixRule of identifier * int * (identifier * int * constr) list
+  | Cofix of identifier * (identifier * constr) list
+  | Refine of constr
+  | Convert_concl of types
+  | Convert_hyp of named_declaration
+  | Thin of identifier list
+  | ThinBody of identifier list
+  | Move of bool * identifier * identifier
+  | Rename of identifier * identifier
+
+(* The type [goal sigma] is the type of subgoal. It has the following form
+\begin{verbatim}
+   it    = { evar_concl = [the conclusion of the subgoal]
+             evar_hyps = [the hypotheses of the subgoal]
+             evar_body = Evar_Empty;
+             evar_info = { pgm    : [The Realizer pgm if any]
+                           lc     : [Set of evar num occurring in subgoal] }}
+   sigma = { stamp = [an int characterizing the ed field, for quick compare]
+             ed : [A set of existential variables depending in the subgoal]
+               number of first evar,
+               it = { evar_concl = [the type of first evar]
+                      evar_hyps = [the context of the evar]
+                      evar_body = [the body of the Evar if any]
+                      evar_info = { pgm    : [Useless ??]
+                                    lc     : [Set of evars occurring
+                                              in the type of evar] } };
+               ...
+               number of last evar, 
+               it = { evar_concl = [the type of evar]
+                      evar_hyps = [the context of the evar]
+                      evar_body = [the body of the Evar if any]
+                      evar_info = { pgm    : [Useless ??]
+                                    lc     : [Set of evars occurring
+                                              in the type of evar] } } }
+   }
+\end{verbatim}
+*)
+
+(* The type constructor ['a sigma] adds an evar map to an object of
+  type ['a] (see below the form of a [goal sigma] *)
+type 'a sigma = { 
+  it : 'a ; 
+  sigma : evar_map}
+
+(*s Proof trees. 
+  [ref] = [None] if the goal has still to be proved, 
+  and [Some (r,l)] if the rule [r] was applied to the goal
+  and gave [l] as subproofs to be completed. 
+  if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
+  that the goal can be proven if the goals in [l] are solved. *)
+type proof_tree = {
+  open_subgoals : int;
+  goal : goal;
+  ref : (rule * proof_tree list) option }
+
+and rule =
+  | Prim of prim_rule
+  | Tactic of tactic_expr * proof_tree
+  | Change_evars
+
+and goal = evar_info
+
+and tactic = goal sigma -> (goal list sigma * validation)
+
+and validation = (proof_tree list -> proof_tree)
+
+and tactic_expr =
+  (constr,
+   constr_pattern,
+   evaluable_global_reference,
+   inductive,
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
+     Tacexpr.gen_tactic_expr
+
+and atomic_tactic_expr =
+  (constr,
+   constr_pattern,
+   evaluable_global_reference,
+   inductive,
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
+     Tacexpr.gen_atomic_tactic_expr
+
+and tactic_arg =
+  (constr,
+   constr_pattern,
+   evaluable_global_reference,
+   inductive,
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
+     Tacexpr.gen_tactic_arg
+
+type hyp_location = identifier Tacexpr.raw_hyp_location
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
new file mode 100644
index 00000000..55f11d52
--- /dev/null
+++ b/proofs/refiner.ml
@@ -0,0 +1,1030 @@
+(************************************************************************)
+(*  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: refiner.ml,v 1.67.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Pp
+open Util
+open Term
+open Termops
+open Sign
+open Evd
+open Sign
+open Environ
+open Reductionops
+open Instantiate
+open Type_errors
+open Proof_trees
+open Proof_type
+open Logic
+open Printer
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+let hypotheses gl = gl.evar_hyps
+let conclusion gl = gl.evar_concl
+
+let sig_it x = x.it
+let sig_sig x = x.sigma
+
+
+let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it)
+
+let pf_status pf = pf.open_subgoals
+
+let is_complete pf = (0 = (pf_status pf))
+
+let on_open_proofs f pf = if is_complete pf then pf else f pf
+
+let and_status = List.fold_left (+) 0
+
+(* Normalizing evars in a goal. Called by tactic Local_constraints
+   (i.e. when the sigma of the proof tree changes). Detect if the
+   goal is unchanged *)
+let norm_goal sigma gl =
+  let red_fun = Evarutil.nf_evar sigma in
+  let ncl = red_fun gl.evar_concl in
+  let ngl =
+    { evar_concl = ncl;
+      evar_hyps =
+      Sign.fold_named_context 
+        (fun (d,b,ty) sign ->
+          add_named_decl (d, option_app red_fun b, red_fun ty) sign)
+        gl.evar_hyps ~init:empty_named_context;
+      evar_body = gl.evar_body} in
+  if ngl = gl then None else Some ngl
+
+
+(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
+   gives
+   [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ;
+   (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ]
+ *)
+
+let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) 
+                    (l : proof_tree list) =
+  match nl with
+    | [] -> []
+    | h::t ->
+	let m,l = list_chop h l in 
+	(List.hd fl m) :: (mapshape t (List.tl fl) l)
+
+(* [frontier : proof_tree -> goal list * validation]
+   given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals
+   to be solved to complete the proof, and [v] is the corresponding 
+   validation *)
+   
+let rec frontier p =
+  match p.ref with
+    | None -> 
+	([p.goal],
+	 (fun lp' -> 
+	    let p' = List.hd lp' in
+            if p'.goal = p.goal then 
+	      p'
+            else 
+	      errorlabstrm "Refiner.frontier"
+                (str"frontier was handed back a ill-formed proof.")))
+    | Some(r,pfl) ->
+    	let gll,vl = List.split(List.map frontier pfl) in
+    	(List.flatten gll,
+         (fun retpfl ->
+            let pfl' = mapshape (List.map List.length gll) vl retpfl in
+            { open_subgoals = and_status (List.map pf_status pfl');
+              goal = p.goal;
+              ref = Some(r,pfl')}))
+
+
+let rec frontier_map_rec f n p =
+  if n < 1 || n > p.open_subgoals then p else
+  match p.ref with
+    | None -> 
+        let p' = f p in
+        if p'.goal == p.goal || p'.goal = p.goal then p'
+        else 
+	  errorlabstrm "Refiner.frontier_map"
+            (str"frontier_map was handed back a ill-formed proof.")
+    | Some(r,pfl) ->
+        let (_,rpfl') =
+          List.fold_left
+            (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
+            (n,[]) pfl in
+        let pfl' = List.rev rpfl' in
+        { open_subgoals = and_status (List.map pf_status pfl');
+          goal = p.goal;
+          ref = Some(r,pfl')}
+
+let frontier_map f n p =
+  let nmax = p.open_subgoals in
+  let n = if n < 0 then nmax + n + 1 else n in
+  if n < 1 || n > nmax then
+    errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); 
+  frontier_map_rec f n p
+
+let rec frontier_mapi_rec f i p =
+  if p.open_subgoals = 0 then p else
+  match p.ref with
+    | None -> 
+        let p' = f i p in
+        if p'.goal == p.goal || p'.goal = p.goal then p'
+        else 
+	  errorlabstrm "Refiner.frontier_mapi"
+            (str"frontier_mapi was handed back a ill-formed proof.")
+    | Some(r,pfl) ->
+        let (_,rpfl') =
+          List.fold_left
+            (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
+            (i,[]) pfl in
+        let pfl' = List.rev rpfl' in
+        { open_subgoals = and_status (List.map pf_status pfl');
+          goal = p.goal;
+          ref = Some(r,pfl')}
+
+let frontier_mapi f p = frontier_mapi_rec f 1 p
+
+(* [list_pf p] is the lists of goals to be solved in order to complete the
+   proof [p] *)
+
+let list_pf p = fst (frontier p)
+
+let rec nb_unsolved_goals pf = pf.open_subgoals
+
+(* leaf g is the canonical incomplete proof of a goal g *)
+
+let leaf g = {
+  open_subgoals = 1;
+  goal = g;
+  ref = None }
+
+(* Tactics table. *)
+
+let tac_tab = Hashtbl.create 17
+
+let add_tactic s t =
+  if Hashtbl.mem tac_tab s then
+    errorlabstrm ("Refiner.add_tactic: ") 
+      (str ("Cannot redeclare tactic "^s));
+  Hashtbl.add tac_tab s t
+
+let overwriting_add_tactic s t =
+  if Hashtbl.mem tac_tab s then begin
+    Hashtbl.remove tac_tab s;
+    warning ("Overwriting definition of tactic "^s)
+  end;
+  Hashtbl.add tac_tab s t
+
+let lookup_tactic s =
+  try 
+    Hashtbl.find tac_tab s
+  with Not_found -> 
+    errorlabstrm "Refiner.lookup_tactic"
+      (str"The tactic " ++ str s ++ str" is not installed")
+
+
+(* refiner r is a tactic applying the rule r *)
+
+let bad_subproof () =
+  anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.")
+
+let check_subproof_connection gl spfl =
+  if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl)
+  then (bad_subproof (); false) else true
+
+let abstract_tactic_expr te tacfun gls =
+  let (sgl_sigma,v) = tacfun gls in
+  let hidden_proof = v (List.map leaf sgl_sigma.it) in
+  (sgl_sigma,
+   fun spfl ->
+     assert (check_subproof_connection sgl_sigma.it spfl);
+     { open_subgoals = and_status (List.map pf_status spfl);
+       goal = gls.it;
+       ref = Some(Tactic(te,hidden_proof),spfl) })
+
+let refiner = function
+  | Prim pr as r ->
+      let prim_fun = prim_refiner pr in
+      (fun goal_sigma ->
+         let sgl = prim_fun goal_sigma.sigma goal_sigma.it in 
+	 ({it=sgl; sigma = goal_sigma.sigma},
+          (fun spfl ->
+	     assert (check_subproof_connection sgl spfl);
+             { open_subgoals = and_status (List.map pf_status spfl);
+               goal = goal_sigma.it;
+               ref = Some(r,spfl) })))
+
+  | Tactic _ -> failwith "Refiner: should not occur"
+      
+   (* [Local_constraints lc] makes the local constraints be [lc] and
+      normalizes evars *)
+
+  | Change_evars as r ->
+      (fun goal_sigma ->
+         let gl = goal_sigma.it in
+         (match norm_goal goal_sigma.sigma gl with
+             Some ngl ->
+	       ({it=[ngl];sigma=goal_sigma.sigma},
+                (fun spfl -> 
+	          assert (check_subproof_connection [ngl] spfl);
+                  { open_subgoals = (List.hd spfl).open_subgoals;
+                    goal = gl;
+                    ref = Some(r,spfl) }))
+           (* if the evar change does not affect the goal, leave the
+              proof tree unchanged *)
+           | None -> ({it=[gl];sigma=goal_sigma.sigma},
+                      (fun spfl ->
+                        assert (List.length spfl = 1);
+                        List.hd spfl))))
+
+
+let local_Constraints gl = refiner Change_evars gl
+
+let norm_evar_tac = local_Constraints
+
+(*
+let vernac_tactic (s,args) =
+  let tacfun = lookup_tactic s args in
+  abstract_extra_tactic s args tacfun
+*)
+let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
+
+let abstract_extended_tactic s args = 
+  abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
+
+let vernac_tactic (s,args) =
+  let tacfun = lookup_tactic s args in
+  abstract_extended_tactic s args tacfun
+
+(* [rc_of_pfsigma : proof sigma -> readable_constraints] *)
+let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
+
+(* [rc_of_glsigma : proof sigma -> readable_constraints] *)
+let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
+
+(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
+  takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
+  where pfterm is the constr corresponding to the proof
+  and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
+  where the mi are metavariables numbers, and ci are their types.
+  Their proof should be completed in order to complete the initial proof *)
+
+let extract_open_proof sigma pf =
+  let next_meta = 
+    let meta_cnt = ref 0 in
+    let rec f () =
+      incr meta_cnt; 
+      if in_dom sigma (existential_of_int !meta_cnt) then f ()
+      else !meta_cnt
+    in f
+  in
+  let open_obligations = ref [] in
+  let rec proof_extractor vl = function
+    | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
+	  
+    | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
+	let sgl,v = frontier hidden_proof in
+	let flat_proof = v spfl in
+	proof_extractor vl flat_proof
+	  
+    | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
+	  
+    | {ref=None;goal=goal} ->
+	let visible_rels =
+          map_succeed
+            (fun id ->
+               try let n = list_index id vl in (n,id)
+	       with Not_found -> failwith "caught")
+            (ids_of_named_context goal.evar_hyps) in
+	let sorted_rels =
+	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
+        let sorted_env =
+          List.map (fun (n,id) -> (n,Sign.lookup_named id goal.evar_hyps))
+            sorted_rels in
+	let abs_concl =
+          List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
+            sorted_env goal.evar_concl	in
+        let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
+        let meta = next_meta () in
+	open_obligations := (meta,abs_concl):: !open_obligations;
+	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) 
+	  
+    | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
+  in
+  let pfterm = proof_extractor [] pf in
+  (pfterm, List.rev !open_obligations)
+  
+(*********************)
+(*   Tacticals       *)
+(*********************)
+
+(* unTAC : tactic -> goal sigma -> proof sigma *)
+
+let unTAC tac g =
+  let (gl_sigma,v) = tac g in 
+  { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
+
+let unpackage glsig = (ref (glsig.sigma)),glsig.it
+
+let repackage r v = {it=v;sigma = !r}
+
+let apply_sig_tac r tac g =
+  check_for_interrupt (); (* Breakpoint *) 
+  let glsigma,v = tac (repackage r g) in 
+  r := glsigma.sigma;
+  (glsigma.it,v)
+
+let idtac_valid = function
+    [pf] -> pf
+  | _ -> anomaly "Refiner.idtac_valid"
+
+(* [goal_goal_list : goal sigma -> goal list sigma] *)
+let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
+
+(* identity tactic without any message *)
+let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
+
+(* the message printing identity tactic *)
+let tclIDTAC_MESSAGE s gls = 
+  if s = "" then tclIDTAC gls
+  else 
+    begin
+      msgnl (str ("Idtac says : "^s)); tclIDTAC gls
+    end
+
+(* General failure tactic *)
+let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
+
+(* A special exception for levels for the Fail tactic *)
+exception FailError of int * string
+
+(* The Fail tactic *)
+let tclFAIL lvl s g = raise (FailError (lvl,s))
+
+let start_tac gls =
+  let (sigr,g) = unpackage gls in
+  (sigr,[g],idtac_valid)
+
+let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
+
+(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *)
+let thensf_tac taci tac (sigr,gs,p) =
+  let n = Array.length taci in
+  let nsg = List.length gs in
+  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+  let gll,pl =
+    List.split
+      (list_map_i (fun i -> apply_sig_tac sigr (if i<n then taci.(i) else tac))
+	0 gs) in
+  (sigr, List.flatten gll,
+   compose p (mapshape (List.map List.length gll) pl))
+
+(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *)
+let thensl_tac tac taci (sigr,gs,p) =
+  let n = Array.length taci in
+  let nsg = List.length gs in
+  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+  let gll,pl =
+    List.split
+      (list_map_i (fun i -> apply_sig_tac sigr (if i<0 then tac else taci.(i)))
+	(n-nsg) gs) in
+  (sigr, List.flatten gll,
+   compose p (mapshape (List.map List.length gll) pl))
+
+(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
+let thensi_tac tac (sigr,gs,p) =
+  let gll,pl =
+    List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in
+  (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl))
+
+let then_tac tac = thensf_tac [||] tac
+
+let non_existent_goal n =
+  errorlabstrm ("No such goal: "^(string_of_int n))
+    (str"Trying to apply a tactic to a non existent goal")
+
+(* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
+   the last goal (i=-1). *)
+let theni_tac i tac ((_,gl,_) as subgoals) =
+  let nsg = List.length gl in
+  let k = if i < 0 then nsg + i + 1 else i in
+  if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
+  else if k >= 1 & k <= nsg then
+    thensf_tac
+      (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC
+      subgoals
+  else non_existent_goal k 
+
+(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
+   to [gls] and applies [t1], ..., [tn] to the [n] first resulting
+   subgoals, and [tac2] to the others subgoals. Raises an error if
+   the number of resulting subgoals is strictly less than [n] *)
+let tclTHENSFIRSTn tac1 taci tac gls =
+  finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls)))
+
+(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
+   to [gls] and applies [t1], ..., [tn] to the [n] last resulting
+   subgoals, and [tac2] to the other subgoals. Raises an error if the
+   number of resulting subgoals is strictly less than [n] *)
+let tclTHENSLASTn tac1 tac taci gls =
+  finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls)))
+
+(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
+   [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
+   number of subgoals is *)
+let tclTHEN_i tac taci gls =
+  finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
+
+let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci
+let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
+
+(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [tac2] to every resulting subgoals *)
+let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2
+
+(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
+   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
+   an error if the number of resulting subgoals is not [n] *)
+let tclTHENSV tac1 tac2v =
+  tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.")
+
+let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
+
+(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the last resulting subgoal *)
+let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
+
+(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the first resulting subgoal *)
+let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
+
+
+(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
+   convenient than [tclTHEN] when [n] is large. *)
+let rec tclTHENLIST = function
+    [] -> tclIDTAC
+  | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
+
+
+
+
+(* various progress criterions *)
+let same_goal gl subgoal = 
+  (hypotheses subgoal) = (hypotheses gl) &
+  eq_constr (conclusion subgoal) (conclusion gl)
+
+
+let weak_progress gls ptree =
+  (List.length gls.it <> 1) or 
+  (not (same_goal (List.hd gls.it) ptree.it))
+
+(* Il y avait ici un ts_eq ........ *)
+let progress gls ptree =
+  (weak_progress gls ptree) or
+  (not (ptree.sigma == gls.sigma))
+
+
+(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
+the goal unchanged *)
+let tclPROGRESS tac ptree =
+  let rslt = tac ptree in
+  if progress (fst rslt) ptree then rslt
+  else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
+
+(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails 
+   if tac leaves the goal unchanged, possibly modifying sigma *)
+let tclWEAK_PROGRESS tac ptree =
+  let rslt = tac ptree in
+  if weak_progress (fst rslt) ptree then rslt
+  else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.")
+
+
+(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
+   one of them being identical to the original goal *)
+let tclNOTSAMEGOAL (tac : tactic) goal =
+  let rslt = tac goal in
+  let gls = (fst rslt).it in
+  if List.exists (same_goal goal.it) gls
+  then errorlabstrm "Refiner.tclNOTSAMEGOAL" 
+      (str"Tactic generated a subgoal identical to the original goal.")
+  else rslt
+
+
+
+(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
+let tclORELSE0 t1 t2 g =
+  try 
+    t1 g
+  with (* Breakpoint *)
+  | e when catchable_exception e -> check_for_interrupt (); t2 g
+  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) ->
+      check_for_interrupt (); t2 g
+  | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+  | Stdpp.Exc_located (s,FailError (lvl,s')) ->
+      raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
+
+(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
+   then applies t2 *)
+let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
+
+(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
+let tclTRY f = (tclORELSE0 f tclIDTAC)
+
+let tclTHENTRY f g = (tclTHEN f (tclTRY g))
+
+(* Try the first tactic that does not fail in a list of tactics *)
+
+let rec tclFIRST = function
+  | [] -> tclFAIL_s "No applicable tactic."
+  |  t::rest -> tclORELSE0 t (tclFIRST rest)
+
+let ite_gen tcal tac_if continue tac_else gl=
+  let success=ref false in
+  let tac_if0 gl=
+    let result=tac_if gl in
+      success:=true;result in
+  let tac_else0 e gl=
+    if !success then 
+      raise e 
+    else 
+      tac_else gl in
+    try 
+      tcal tac_if0 continue gl
+    with (* Breakpoint *)
+      | e when catchable_exception e ->
+	  check_for_interrupt (); tac_else0 e gl
+      | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e ->
+	  check_for_interrupt (); tac_else0 e gl
+      | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+      | Stdpp.Exc_located (s,FailError (lvl,s')) ->
+	  raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
+	
+(* Try the first tactic and, if it succeeds, continue with 
+   the second one, and if it fails, use the third one *)
+
+let tclIFTHENELSE=ite_gen tclTHEN
+
+(* Idem with tclTHENS and tclTHENSV *)
+
+let tclIFTHENSELSE=ite_gen tclTHENS
+
+let tclIFTHENSVELSE=ite_gen tclTHENSV
+
+
+(* Fails if a tactic did not solve the goal *)
+let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
+
+(* Try the first thats solves the current goal *)
+let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
+
+			   
+(* Iteration tacticals *)
+
+let tclDO n t = 
+  let rec dorec k = 
+    if k < 0 then errorlabstrm "Refiner.tclDO"
+      (str"Wrong argument : Do needs a positive integer.");
+    if k = 0 then tclIDTAC
+    else if k = 1 then t else (tclTHEN t (dorec (k-1)))
+  in 
+  dorec n 
+
+(* Beware: call by need of CAML, g is needed *)
+let rec tclREPEAT t g =
+  (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g
+
+let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
+
+(* Repeat on the first subgoal (no failure if no more subgoal) *)
+let rec tclREPEAT_MAIN t g =
+  (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else
+    tclIDTAC)) tclIDTAC) g
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+(* Functions working on goal list for correct backtracking in Prolog *)
+
+let tclFIRSTLIST = tclFIRST
+let tclIDTAC_list gls = (gls, fun x -> x)
+
+(* first_goal : goal list sigma -> goal sigma *)
+
+let first_goal gls = 
+  let gl = gls.it and sig_0 = gls.sigma in 
+  if gl = [] then error "first_goal"; 
+  { it = List.hd gl; sigma = sig_0 }
+
+(* goal_goal_list : goal sigma -> goal list sigma *)
+
+let goal_goal_list gls = 
+  let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
+
+(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
+
+let apply_tac_list tac glls = 
+  let (sigr,lg) = unpackage glls in
+  match lg with
+  | (g1::rest) ->
+      let (gl,p) = apply_sig_tac sigr tac g1 in
+      let n = List.length gl in 
+      (repackage sigr (gl@rest), 
+       fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
+  | _ -> error "apply_tac_list"
+	  
+let then_tactic_list tacl1 tacl2 glls = 
+  let (glls1,pl1) = tacl1 glls in
+  let (glls2,pl2) = tacl2 glls1 in
+  (glls2, compose pl1 pl2)
+
+(* Transform a tactic_list into a tactic *)
+
+let tactic_list_tactic tac gls = 
+    let (glres,vl) = tac (goal_goal_list gls) in
+    (glres, compose idtac_valid vl)
+
+
+
+
+(* The type of proof-trees state and a few utilities 
+   A proof-tree state is built from a proof-tree, a set of global
+   constraints, and a stack which allows to navigate inside the
+   proof-tree remembering how to rebuild the global proof-tree
+   possibly after modification of one of the focused children proof-tree.
+   The number in the stack corresponds to 
+   either the selected subtree and the validation is a function from a
+   proof-tree list consisting only of one proof-tree to the global
+   proof-tree 
+   or -1 when the move is done behind a registered tactic in which
+   case the validation corresponds to a constant function giving back 
+   the original proof-tree. *)
+
+type pftreestate = {
+  tpf      : proof_tree ;
+  tpfsigma : evar_map;
+  tstack   : (int * validation) list }
+
+let proof_of_pftreestate pts = pts.tpf
+let is_top_pftreestate pts = pts.tstack = [] 
+let cursor_of_pftreestate pts = List.map fst pts.tstack
+let evc_of_pftreestate pts = pts.tpfsigma
+
+let top_goal_of_pftreestate pts = 
+  { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
+
+let nth_goal_of_pftreestate n pts =
+  let goals = fst (frontier pts.tpf) in
+  try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
+  with Invalid_argument _ | Failure _ -> non_existent_goal n
+
+let descend n p =
+  match p.ref with
+    | None        -> error "It is a leaf."
+    | Some(r,pfl) ->
+    	if List.length pfl >= n then
+	  (match list_chop (n-1) pfl with 
+	     | left,(wanted::right) ->
+		 (wanted,
+		  (fun pfl' ->
+                     if (List.length pfl' = 1) 
+		       & (List.hd pfl').goal = wanted.goal 
+		     then
+                       let pf'       = List.hd pfl' in
+                       let spfl      = left@(pf'::right) in
+                       let newstatus = and_status (List.map pf_status spfl) in
+                       { open_subgoals = newstatus;
+			 goal          = p.goal;
+			 ref           = Some(r,spfl) }
+                     else 
+		       error "descend: validation"))
+	     | _ -> assert false)
+    	else 
+	  error "Too few subproofs"
+
+let traverse n pts = match n with 
+  | 0 -> (* go to the parent *)
+      (match  pts.tstack with
+	 | [] -> error "traverse: no ancestors"
+	 | (_,v)::tl ->
+	     { tpf = v [pts.tpf];
+	       tstack = tl;
+	       tpfsigma = pts.tpfsigma })
+  | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
+      (match pts.tpf.ref with
+	 | Some (Tactic (_,spf),_) ->
+	     let v = (fun pfl -> pts.tpf) in 
+	     { tpf = spf;
+               tstack = (-1,v)::pts.tstack;
+               tpfsigma = pts.tpfsigma }
+	 | _ -> error "traverse: not a tactic-node")
+  | n -> (* when n>0, go to the nth child *)
+      let (npf,v) = descend n pts.tpf in 
+      { tpf = npf;
+        tpfsigma = pts.tpfsigma;
+        tstack = (n,v):: pts.tstack }
+
+let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc }
+
+let app_tac sigr tac p =
+  let (gll,v) = tac {it=p.goal;sigma= !sigr} in
+  sigr := gll.sigma;
+  v (List.map leaf gll.it)
+
+(* solve the nth subgoal with tactic tac *)
+let solve_nth_pftreestate n tac pts =
+  let sigr = ref pts.tpfsigma in
+  let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+  let tpf'' =
+    if !sigr == pts.tpfsigma then tpf'
+    else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
+  { tpf      = tpf'';
+    tpfsigma = !sigr;
+    tstack   = pts.tstack }
+
+let solve_pftreestate = solve_nth_pftreestate 1
+
+(* This function implements a poor man's undo at the current goal.
+   This is a gross approximation as it does not attempt to clean correctly
+   the global constraints given in tpfsigma. *)
+
+let weak_undo_pftreestate pts =
+  let pf = leaf pts.tpf.goal in
+  { tpf = pf;
+    tpfsigma = pts.tpfsigma;
+    tstack = pts.tstack }
+
+(* Gives a new proof (a leaf) of a goal gl *)
+let mk_pftreestate g =
+  { tpf      = leaf g;
+    tstack   = [];
+    tpfsigma = Evd.empty }
+
+(* Extracts a constr from a proof-tree state ; raises an error if the
+   proof is not complete or the state does not correspond to the head
+   of the proof-tree *)
+
+let extract_open_pftreestate pts =
+  extract_open_proof pts.tpfsigma pts.tpf
+
+let extract_pftreestate pts =
+  if pts.tstack <> [] then
+    errorlabstrm "extract_pftreestate"
+      (str"Cannot extract from a proof-tree in which we have descended;" ++
+         spc () ++ str"Please ascend to the root");
+  let pfterm,subgoals = extract_open_pftreestate pts in
+  if subgoals <> [] then
+   errorlabstrm "extract_proof"
+   (str "Attempt to save an incomplete proof");
+  let env = Global.env_of_context pts.tpf.goal.evar_hyps in
+  strong whd_betaiotaevar env pts.tpfsigma pfterm
+  (***
+  local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
+  ***)
+(* Focus on the first leaf proof in a proof-tree state *)
+
+let rec first_unproven pts =
+  let pf = (proof_of_pftreestate pts) in 
+  if is_complete_proof pf then
+    errorlabstrm "first_unproven" (str"No unproven subgoals");
+  if is_leaf_proof pf then
+    pts
+  else
+    let childnum =
+      list_try_find_i 
+	(fun n pf -> 
+	   if not(is_complete_proof pf) then n else failwith "caught")
+	1 (children_of_proof pf)
+    in 
+    first_unproven (traverse childnum pts)
+
+(* Focus on the last leaf proof in a proof-tree state *)
+
+let rec last_unproven pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_complete_proof pf then
+    errorlabstrm "last_unproven" (str"No unproven subgoals");
+  if is_leaf_proof pf then
+    pts
+  else 
+    let children = (children_of_proof pf) in
+    let nchilds = List.length children in
+    let childnum =
+      list_try_find_i 
+        (fun n pf ->
+           if not(is_complete_proof pf) then n else failwith "caught")
+        1 (List.rev children)
+    in 
+    last_unproven (traverse (nchilds-childnum+1) pts)
+      
+let rec nth_unproven n pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_complete_proof pf then
+    errorlabstrm "nth_unproven" (str"No unproven subgoals");
+  if is_leaf_proof pf then
+    if n = 1 then 
+      pts 
+    else
+      errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
+  else 
+    let children = children_of_proof pf in
+    let rec process i k = function
+      | [] -> 
+	  errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
+      | pf1::rest -> 
+	  let k1 = nb_unsolved_goals pf1 in 
+	  if k1 < k then 
+	    process (i+1) (k-k1) rest
+	  else 
+	    nth_unproven k (traverse i pts)
+    in 
+    process 1 n children
+
+let rec node_prev_unproven loc pts =
+  let pf = proof_of_pftreestate pts in 
+  match cursor_of_pftreestate pts with
+    | [] -> last_unproven pts
+    | n::l ->
+	if is_complete_proof pf or loc = 1 then
+          node_prev_unproven n (traverse 0 pts)
+	else 
+	  let child = List.nth (children_of_proof pf) (loc - 2) in
+	  if is_complete_proof child then
+	    node_prev_unproven (loc - 1) pts
+	  else 
+	    first_unproven (traverse (loc - 1) pts)
+
+let rec node_next_unproven loc pts =
+  let pf = proof_of_pftreestate pts in 
+  match cursor_of_pftreestate pts with
+    | [] -> first_unproven pts
+    | n::l ->
+	if is_complete_proof pf ||
+           loc = (List.length (children_of_proof pf)) then
+             node_next_unproven n (traverse 0 pts)
+	else if is_complete_proof (List.nth (children_of_proof pf) loc) then
+	  node_next_unproven (loc + 1) pts
+	else 
+	  last_unproven(traverse (loc + 1) pts)
+
+let next_unproven pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_leaf_proof pf then
+    match cursor_of_pftreestate pts with
+      | [] -> error "next_unproven"
+      | n::_ -> node_next_unproven n (traverse 0 pts)
+  else 
+    node_next_unproven (List.length (children_of_proof pf)) pts
+
+let prev_unproven pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_leaf_proof pf then
+    match cursor_of_pftreestate pts with
+      | [] -> error "prev_unproven"
+      | n::_ -> node_prev_unproven n (traverse 0 pts)
+  else 
+    node_prev_unproven 1 pts
+
+let rec top_of_tree pts = 
+  if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
+
+
+(* Pretty-printers. *)
+
+open Pp
+
+let pr_tactic = function
+  | Tacexpr.TacArg (Tacexpr.Tacexp t) ->
+      if !Options.v7 then
+	Pptactic.pr_glob_tactic t (*top tactic from tacinterp*)
+      else
+	Pptacticnew.pr_glob_tactic (Global.env()) t
+  | t -> 
+      if !Options.v7 then
+	Pptactic.pr_tactic t
+      else
+	Pptacticnew.pr_tactic (Global.env()) t
+
+let pr_rule = function
+  | Prim r -> hov 0 (pr_prim_rule r)
+  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
+  | Change_evars ->
+      (* This is internal tactic and cannot be replayed at user-level.
+         Function pr_rule_dot below is used when we want to hide
+         Change_evars *)
+      str "Evar change"
+
+(* Does not print change of evars *)
+let pr_rule_dot = function 
+  | Change_evars -> mt ()
+  | r -> pr_rule r ++ str"."
+
+exception Different
+
+(* We remove from the var context of env what is already in osign *)
+let thin_sign osign sign =
+  Sign.fold_named_context
+    (fun (id,c,ty as d) sign ->
+       try 
+	 if Sign.lookup_named id osign = (id,c,ty) then sign
+	 else raise Different
+       with Not_found | Different -> add_named_decl d sign)
+    sign ~init:empty_named_context
+
+let rec print_proof sigma osign pf =
+  let {evar_hyps=hyps; evar_concl=cl; 
+       evar_body=body} = pf.goal in
+  let hyps' = thin_sign osign hyps in
+  match pf.ref with
+    | None -> 
+	hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
+    | Some(r,spfl) ->
+    	hov 0 
+	  (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
+	   spc () ++ str" BY " ++
+	   hov 0 (pr_rule r) ++ fnl () ++
+	   str"  " ++
+	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
+)
+	  
+let pr_change gl = 
+  (str"Change " ++ prterm_env (Global.env()) gl.evar_concl ++ str".")
+
+let rec print_script nochange sigma osign pf =
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  match pf.ref with
+    | None ->
+        (if nochange then 
+	  (str"<Your Tactic Text here>") 
+	else 
+	  pr_change pf.goal)
+	++ fnl ()
+    | Some(r,spfl) ->
+        ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+           pr_rule_dot r ++ fnl () ++
+           prlist_with_sep pr_fnl
+             (print_script nochange sigma sign) spfl)
+
+let print_treescript nochange sigma _osign pf =
+  let rec aux top pf =
+    let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+    match pf.ref with
+    | None ->
+        if nochange then 
+	  (str"<Your Tactic Text here>") 
+	else 
+	  (pr_change pf.goal)
+    | Some(r,spfl) ->
+        (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
+	pr_rule_dot r ++
+	match spfl with
+	| [] -> mt ()
+	| [spf] -> fnl () ++ (if top then mt () else str "  ") ++ aux top spf
+	| _ -> fnl () ++ str " " ++
+	    hov 0 (prlist_with_sep fnl (aux false) spfl)
+  in hov 0 (aux true pf)
+
+let rec print_info_script sigma osign pf =
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  match pf.ref with
+    | None -> (mt ())
+    | Some(Change_evars,[spf]) ->
+        print_info_script sigma osign spf
+    | Some(r,spfl) ->
+        (pr_rule r ++ 
+           match spfl with
+             | [pf1] ->
+                 if pf1.ref = None then 
+		   (str "." ++ fnl ())
+                 else 
+		   (str";" ++ brk(1,3) ++
+		      print_info_script sigma sign pf1)
+             | _ -> (str"." ++ fnl () ++
+                       prlist_with_sep pr_fnl
+                         (print_info_script sigma sign) spfl))
+
+let format_print_info_script sigma osign pf = 
+  hov 0 (print_info_script sigma osign pf)
+    
+let print_subscript sigma sign pf = 
+  if is_tactic_proof pf then 
+    format_print_info_script sigma sign (subproof_of_proof pf)
+  else 
+    format_print_info_script sigma sign pf
+
+let tclINFO (tac : tactic) gls = 
+  let (sgl,v) as res = tac gls in 
+  begin try 
+    let pf = v (List.map leaf (sig_it sgl)) in
+    let sign = (sig_it gls).evar_hyps in
+    msgnl (hov 0 (str" == " ++
+                  print_subscript (sig_sig gls) sign pf))
+  with e when catchable_exception e -> 
+    msgnl (hov 0 (str "Info failed to apply validation"))
+  end;
+  res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
new file mode 100644
index 00000000..bed1158d
--- /dev/null
+++ b/proofs/refiner.mli
@@ -0,0 +1,210 @@
+
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: refiner.mli,v 1.31.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+
+(*i*)
+open Term
+open Sign
+open Evd
+open Proof_trees
+open Proof_type
+open Tacexpr
+(*i*)
+
+(* The refiner (handles primitive rules and high-level tactics). *)
+
+val sig_it  : 'a sigma -> 'a
+val sig_sig : 'a sigma -> evar_map
+
+val project_with_focus : goal sigma -> named_context sigma
+
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
+val apply_sig_tac :
+  evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+val add_tactic             : string -> (closed_generic_argument list -> tactic) -> unit
+val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
+val lookup_tactic          : string -> (closed_generic_argument list) -> tactic
+
+(*s Hiding the implementation of tactics. *)
+
+(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
+   a single proof node *)
+val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : tactic_expr -> tactic -> tactic
+val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
+
+val refiner : rule -> tactic
+val vernac_tactic : string * closed_generic_argument list -> tactic
+val frontier : transformation_tactic
+val list_pf : proof_tree -> goal list
+val unTAC : tactic -> goal sigma -> proof_tree sigma
+
+val local_Constraints : tactic
+
+(* [frontier_map f n p] applies f on the n-th open subgoal of p and
+   rebuilds proof-tree.
+   n=1 for first goal, n negative counts from the right *)
+val frontier_map :
+  (proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree
+
+(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *)
+val frontier_mapi :
+  (int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree
+
+(*s Tacticals. *)
+
+(* [tclIDTAC] is the identity tactic without message printing*)
+val tclIDTAC          : tactic
+val tclIDTAC_MESSAGE  : string -> tactic
+
+
+(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [tac2] to every resulting subgoals *)
+val tclTHEN          : tactic -> tactic -> tactic
+
+(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
+   convenient than [tclTHEN] when [n] is large *)
+val tclTHENLIST      : tactic list -> tactic
+
+(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
+val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
+
+(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the last resulting subgoal (previously called [tclTHENL]) *)
+val tclTHENLAST         : tactic -> tactic -> tactic
+
+(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the first resulting subgoal *)
+val tclTHENFIRST         : tactic -> tactic -> tactic
+
+(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
+   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
+   an error if the number of resulting subgoals is not [n] *)
+val tclTHENSV         : tactic -> tactic array -> tactic
+
+(* Same with a list of tactics *)
+val tclTHENS         : tactic -> tactic list -> tactic
+
+(* [tclTHENST] is renamed [tclTHENSFIRSTn]
+val tclTHENST        : tactic -> tactic array -> tactic -> tactic
+*)
+
+(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
+   last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
+val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
+
+(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
+   applies [t1],...,[tn] on the first [n] resulting subgoals and
+   [tac2] for the remaining last subgoals (previously called tclTHENST) *)
+val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
+
+(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
+   applies [t1],...,[tn] on the last [n] resulting subgoals and leaves
+   unchanged the other subgoals *)
+val tclTHENLASTn    : tactic -> tactic array -> tactic
+
+(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
+   applies [t1],...,[tn] on the first [n] resulting subgoals and leaves
+   unchanged the other subgoals (previously called [tclTHENSI]) *)
+val tclTHENFIRSTn   : tactic -> tactic array -> tactic
+
+(* A special exception for levels for the Fail tactic *)
+exception FailError of int * string
+
+val tclORELSE        : tactic -> tactic -> tactic
+val tclREPEAT        : tactic -> tactic
+val tclREPEAT_MAIN   : tactic -> tactic
+val tclFIRST         : tactic list -> tactic
+val tclSOLVE         : tactic list -> tactic
+val tclTRY           : tactic -> tactic
+val tclTHENTRY       : tactic -> tactic -> tactic
+val tclCOMPLETE      : tactic -> tactic
+val tclAT_LEAST_ONCE : tactic -> tactic
+val tclFAIL          : int -> string -> tactic
+val tclDO            : int -> tactic -> tactic
+val tclPROGRESS      : tactic -> tactic
+val tclWEAK_PROGRESS : tactic -> tactic
+val tclNOTSAMEGOAL   : tactic -> tactic
+val tclINFO          : tactic -> tactic
+
+(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
+   if it succeeds, applies [tac2] to the resulting subgoals, 
+   and if not applies [tac3] to the initial goal [gls] *)
+val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
+val tclIFTHENSELSE   : tactic -> tactic list -> tactic ->tactic
+val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+val tclFIRSTLIST       : tactic_list list -> tactic_list
+val tclIDTAC_list      : tactic_list
+val first_goal         : 'a list sigma -> 'a sigma
+val apply_tac_list     : tactic -> tactic_list
+val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
+val tactic_list_tactic : tactic_list -> tactic
+val goal_goal_list     : 'a sigma -> 'a list sigma
+
+
+(*s Functions for handling the state of the proof editor. *)
+
+type pftreestate
+
+val proof_of_pftreestate : pftreestate -> proof_tree
+val cursor_of_pftreestate : pftreestate -> int list
+val is_top_pftreestate : pftreestate -> bool
+val evc_of_pftreestate : pftreestate -> evar_map
+val top_goal_of_pftreestate : pftreestate -> goal sigma
+val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
+
+val traverse : int -> pftreestate -> pftreestate
+val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
+val solve_pftreestate : tactic -> pftreestate -> pftreestate
+
+(* a weak version of logical undoing, that is really correct only *)
+(* if there are no existential variables.                         *)
+val weak_undo_pftreestate : pftreestate -> pftreestate
+
+val mk_pftreestate : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_pftreestate : pftreestate -> constr
+val first_unproven : pftreestate -> pftreestate
+val last_unproven : pftreestate -> pftreestate
+val nth_unproven : int -> pftreestate -> pftreestate
+val node_prev_unproven : int -> pftreestate -> pftreestate
+val node_next_unproven : int -> pftreestate -> pftreestate
+val next_unproven : pftreestate -> pftreestate
+val prev_unproven : pftreestate -> pftreestate
+val top_of_tree : pftreestate -> pftreestate
+val change_constraints_pftreestate 
+  : evar_map -> pftreestate -> pftreestate
+
+
+(*s Pretty-printers. *)
+
+(*i*)
+open Pp
+(*i*)
+
+val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
+val pr_rule     : rule -> std_ppcmds
+val pr_tactic   : tactic_expr -> std_ppcmds
+val print_script :
+  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+val print_treescript :
+  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
new file mode 100644
index 00000000..d8d7319d
--- /dev/null
+++ b/proofs/tacexpr.ml
@@ -0,0 +1,314 @@
+(************************************************************************)
+(*  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: tacexpr.ml,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Names
+open Topconstr
+open Libnames
+open Nametab
+open Rawterm
+open Util
+open Genarg
+open Pattern
+
+type 'a or_metaid = AI of 'a | MetaId of loc * string
+
+type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+
+type raw_red_flag =
+  | FBeta
+  | FIota
+  | FZeta
+  | FConst of reference list
+  | FDeltaBut of reference list
+
+let make_red_flag =
+  let rec add_flag red = function
+    | [] -> red
+    | FBeta :: lf -> add_flag { red with rBeta = true } lf
+    | FIota :: lf -> add_flag { red with rIota = true } lf
+    | FZeta :: lf -> add_flag { red with rZeta = true } lf
+    | FConst l :: lf ->
+	if red.rDelta then
+	  error
+	    "Cannot set both constants to unfold and constants not to unfold";
+        add_flag { red with rConst = list_union red.rConst l } lf
+    | FDeltaBut l :: lf ->
+	if red.rConst <> [] & not red.rDelta then
+	  error
+	    "Cannot set both constants to unfold and constants not to unfold";
+        add_flag 
+	  { red with rConst = list_union red.rConst l; rDelta = true }
+	  lf
+  in
+  add_flag
+    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} 
+
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
+type 'a raw_hyp_location = 
+    'a * int list * (hyp_location_flag * hyp_location_flag option ref)
+
+type 'a induction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of identifier located
+  | ElimOnAnonHyp of int
+
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
+
+type ('c,'id) inversion_strength =
+  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr option
+  | DepInversion of inversion_kind * 'c option * intro_pattern_expr option
+  | InversionUsing of 'c * 'id list
+
+type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
+
+type 'id gsimple_clause = ('id raw_hyp_location) option
+(* onhyps:
+     [None] means *on every hypothesis*
+     [Some l] means on hypothesis belonging to l *)
+type 'id gclause =
+  { onhyps : 'id raw_hyp_location list option;
+    onconcl : bool;
+    concl_occs :int list }
+
+let simple_clause_of = function
+    { onhyps = Some[scl]; onconcl = false } -> Some scl
+  | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
+  | _ -> error "not a simple clause (one hypothesis or conclusion)"
+
+type pattern_expr = constr_expr
+
+(* Type of patterns *)
+type 'a match_pattern =
+  | Term of 'a
+  | Subterm of identifier option * 'a
+
+(* Type of hypotheses for a Match Context rule *)
+type 'a match_context_hyps =
+  | Hyp of name located * 'a match_pattern
+
+(* Type of a Match rule for Match Context and Match *)
+type ('a,'t) match_rule =
+  | Pat of 'a match_context_hyps list * 'a match_pattern * 't
+  | All of 't
+
+type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
+  (* Basic tactics *)
+  | TacIntroPattern of intro_pattern_expr list
+  | TacIntrosUntil of quantified_hypothesis
+  | TacIntroMove of identifier option * identifier located option
+  | TacAssumption
+  | TacExact of 'constr
+  | TacApply of 'constr with_bindings
+  | TacElim of 'constr with_bindings * 'constr with_bindings option
+  | TacElimType of 'constr
+  | TacCase of 'constr with_bindings
+  | TacCaseType of 'constr
+  | TacFix of identifier option * int
+  | TacMutualFix of identifier * int * (identifier * int * 'constr) list
+  | TacCofix of identifier option
+  | TacMutualCofix of identifier * (identifier * 'constr) list
+  | TacCut of 'constr
+  | TacTrueCut of name * 'constr 
+  | TacForward of bool * name * 'constr
+  | TacGeneralize of 'constr list
+  | TacGeneralizeDep of 'constr
+  | TacLetTac of name * 'constr * 'id gclause
+  | TacInstantiate of int * 'constr * 'id gclause
+
+  (* Derived basic tactics *)
+  | TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref)
+  | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
+      * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref)
+  | TacSimpleDestruct of quantified_hypothesis
+  | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
+      * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref)
+
+  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
+  | TacDecomposeAnd of 'constr
+  | TacDecomposeOr of 'constr
+  | TacDecompose of 'ind list * 'constr
+  | TacSpecialize of int option * 'constr with_bindings
+  | TacLApply of 'constr
+
+  (* Automation tactics *)
+  | TacTrivial of string list option
+  | TacAuto of int option * string list option
+  | TacAutoTDB of int option
+  | TacDestructHyp of (bool * identifier located)
+  | TacDestructConcl
+  | TacSuperAuto of (int option * reference list * bool * bool)
+  | TacDAuto of int option * int option
+
+  (* Context management *)
+  | TacClear of 'id list
+  | TacClearBody of 'id list
+  | TacMove of bool * 'id * 'id
+  | TacRename of 'id * 'id
+
+  (* Constructors *)
+  | TacLeft of 'constr bindings
+  | TacRight of 'constr bindings
+  | TacSplit of bool * 'constr bindings
+  | TacAnyConstructor of 'tac option
+  | TacConstructor of int or_metaid * 'constr bindings
+
+  (* Conversion *)
+  | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
+  | TacChange of
+      'constr occurrences option * 'constr * 'id gclause
+
+  (* Equivalence relations *)
+  | TacReflexivity
+  | TacSymmetry of 'id gclause
+  | TacTransitivity of 'constr 
+
+  (* Equality and inversion *)
+  | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
+      
+  (* For ML extensions *)
+  | TacExtend of loc * string * ('constr,'tac) generic_argument list
+
+  (* For syntax extensions *)
+  | TacAlias of loc * string *
+      (identifier * ('constr,'tac) generic_argument) list
+      * (dir_path * 'tac)
+
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
+  | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
+  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option
+  | TacId of string
+  | TacFail of int or_var * string
+  | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+
+  | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacMatch of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
+  | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
+
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
+  identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+
+  (* These are possible arguments of a tactic definition *)
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
+  | TacDynamic     of loc * Dyn.t
+  | TacVoid
+  | MetaIdArg      of loc * string
+  | ConstrMayEval  of ('constr,'cst) may_eval
+  | IntroPattern   of intro_pattern_expr
+  | Reference      of 'ref
+  | Integer        of int
+  | TacCall        of loc *
+      'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
+  | TacFreshId     of string option
+  | Tacexp of 'tac
+
+type raw_tactic_expr =
+    (constr_expr,
+     pattern_expr,
+     reference,
+     reference,
+     reference,
+     identifier located or_metaid,
+     raw_tactic_expr) gen_tactic_expr
+
+type raw_atomic_tactic_expr =
+    (constr_expr,                  (* constr *)
+     pattern_expr,                 (* pattern *)
+     reference,                    (* evaluable reference *)
+     reference,                    (* inductive *)
+     reference,                    (* ltac reference *)
+     identifier located or_metaid, (* identifier *)
+     raw_tactic_expr) gen_atomic_tactic_expr
+
+type raw_tactic_arg =
+    (constr_expr,
+     pattern_expr,
+     reference,
+     reference,
+     reference,
+     identifier located or_metaid,
+     raw_tactic_expr) gen_tactic_arg
+
+type raw_generic_argument =
+    (constr_expr,raw_tactic_expr) generic_argument
+
+type raw_red_expr = (constr_expr, reference) red_expr_gen
+
+(* Globalized tactics *)
+type glob_tactic_expr =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
+     ltac_constant located or_var,
+     identifier located,
+     glob_tactic_expr) gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
+     ltac_constant located or_var,
+     identifier located,
+     glob_tactic_expr) gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
+     ltac_constant located,
+     identifier located or_var,
+     glob_tactic_expr) gen_tactic_arg
+
+type glob_generic_argument =
+    (rawconstr_and_expr,glob_tactic_expr) generic_argument
+
+type glob_red_expr =
+    (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
+
+type closed_raw_generic_argument =
+    (constr_expr,raw_tactic_expr) generic_argument
+
+type 'a raw_abstract_argument_type =
+    ('a,constr_expr,raw_tactic_expr) abstract_argument_type
+
+type 'a glob_abstract_argument_type =
+    ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type
+
+type open_generic_argument =
+    (Term.constr,glob_tactic_expr) generic_argument
+
+type closed_generic_argument =
+    (Term.constr,glob_tactic_expr) generic_argument
+
+type 'a closed_abstract_argument_type =
+    ('a,Term.constr,glob_tactic_expr) abstract_argument_type
+
+type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
new file mode 100644
index 00000000..0e3a49b0
--- /dev/null
+++ b/proofs/tacmach.ml
@@ -0,0 +1,260 @@
+(************************************************************************)
+(*  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: tacmach.ml,v 1.61.2.1 2004/07/16 19:30:50 herbelin Exp $ *)
+
+open Util
+open Names
+open Nameops
+open Sign
+open Term
+open Termops
+open Instantiate
+open Environ
+open Reductionops
+open Evd
+open Typing
+open Tacred
+open Proof_trees
+open Proof_type
+open Logic
+open Refiner
+open Tacexpr
+
+let re_sig it gc = { it = it; sigma = gc }
+
+(**************************************************************)
+(* Operations for handling terms under a local typing context *)
+(**************************************************************)
+
+type 'a sigma   = 'a Proof_type.sigma;;
+type validation = Proof_type.validation;;
+type tactic     = Proof_type.tactic;;
+
+let unpackage = Refiner.unpackage
+let repackage = Refiner.repackage
+let apply_sig_tac = Refiner.apply_sig_tac
+
+let sig_it     = Refiner.sig_it
+let project    = Refiner.sig_sig
+let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
+let pf_hyps gls = (sig_it gls).evar_hyps
+
+let pf_concl gls = (sig_it gls).evar_concl
+let pf_hyps_types gls  =
+  let sign = Environ.named_context (pf_env gls) in
+  List.map (fun (id,_,x) -> (id, x)) sign
+
+let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
+
+let pf_last_hyp gl = List.hd (pf_hyps gl)
+
+let pf_get_hyp gls id = 
+  try 
+    Sign.lookup_named id (pf_hyps gls)
+  with Not_found -> 
+    error ("No such hypothesis : " ^ (string_of_id id))
+
+let pf_get_hyp_typ gls id =
+  let (_,_,ty)= (pf_get_hyp gls id) in
+  ty
+
+let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
+
+let pf_get_new_id id gls = 
+  next_ident_away id (pf_ids_of_hyps gls)
+
+let pf_get_new_ids ids gls =
+  let avoid = pf_ids_of_hyps gls in
+  List.fold_right
+    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
+    ids []
+
+let pf_interp_constr gls c =
+  let evc = project gls in 
+  Constrintern.interp_constr evc (pf_env gls) c
+
+let pf_interp_openconstr gls c =
+  let evc = project gls in 
+  Constrintern.interp_openconstr evc (pf_env gls) c
+
+let pf_interp_type gls c =
+  let evc = project gls in 
+  Constrintern.interp_type evc (pf_env gls) c
+
+let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
+
+let pf_parse_const gls = compose (pf_global gls) id_of_string
+
+let pf_execute gls =
+  let evc = project gls in 
+  Typing.unsafe_machine (pf_env gls) evc
+
+let pf_reduction_of_redexp gls re c = 
+  reduction_of_redexp re (pf_env gls) (project gls) c 
+
+let pf_apply f gls = f (pf_env gls) (project gls)
+let pf_reduce = pf_apply
+
+let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
+let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
+let pf_hnf_constr                = pf_reduce hnf_constr
+let pf_red_product               = pf_reduce red_product
+let pf_nf                        = pf_reduce nf
+let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
+let pf_compute                   = pf_reduce compute
+let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_type_of                   = pf_reduce type_of
+
+let pf_conv_x                   = pf_reduce is_conv
+let pf_conv_x_leq               = pf_reduce is_conv_leq
+let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
+let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
+let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
+
+let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
+
+let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2)))
+
+(************************************)
+(* Tactics handling a list of goals *)
+(************************************)
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+let first_goal         = first_goal
+let goal_goal_list     = goal_goal_list
+let apply_tac_list     = apply_tac_list
+let then_tactic_list   = then_tactic_list
+let tactic_list_tactic = tactic_list_tactic
+let tclFIRSTLIST       = tclFIRSTLIST
+let tclIDTAC_list      = tclIDTAC_list
+
+
+(********************************************************)
+(* Functions for handling the state of the proof editor *)
+(********************************************************)
+
+type pftreestate = Refiner.pftreestate
+
+let proof_of_pftreestate    = proof_of_pftreestate
+let cursor_of_pftreestate   = cursor_of_pftreestate
+let is_top_pftreestate      = is_top_pftreestate
+let evc_of_pftreestate      = evc_of_pftreestate
+let top_goal_of_pftreestate = top_goal_of_pftreestate
+let nth_goal_of_pftreestate = nth_goal_of_pftreestate
+let traverse                = traverse
+let solve_nth_pftreestate   = solve_nth_pftreestate
+let solve_pftreestate       = solve_pftreestate
+let weak_undo_pftreestate   = weak_undo_pftreestate
+let mk_pftreestate          = mk_pftreestate
+let extract_pftreestate     = extract_pftreestate
+let extract_open_pftreestate = extract_open_pftreestate
+let first_unproven          = first_unproven
+let last_unproven           = last_unproven
+let nth_unproven            = nth_unproven
+let node_prev_unproven      = node_prev_unproven
+let node_next_unproven      = node_next_unproven
+let next_unproven           = next_unproven
+let prev_unproven           = prev_unproven
+let top_of_tree             = top_of_tree
+let frontier                = frontier
+let change_constraints_pftreestate = change_constraints_pftreestate
+
+
+(********************************************)
+(* Definition of the most primitive tactics *)
+(********************************************)
+
+let refiner = refiner
+
+(* This does not check that the variable name is not here *)
+let introduction_no_check id =
+  refiner (Prim (Intro id))
+
+(* This does not check that the dependencies are correct *)
+let intro_replacing_no_check whereid gl = 
+  refiner (Prim (Intro_replacing whereid)) gl
+
+let internal_cut_no_check id t gl = 
+  refiner (Prim (Cut (true,id,t))) gl
+
+let internal_cut_rev_no_check id t gl = 
+  refiner (Prim (Cut (false,id,t))) gl
+
+let refine_no_check c gl = 
+  refiner (Prim (Refine c)) gl
+
+let convert_concl_no_check c gl = 
+  refiner (Prim (Convert_concl c)) gl
+
+let convert_hyp_no_check d gl =
+  refiner (Prim (Convert_hyp d)) gl
+
+(* This does not check dependencies *)
+let thin_no_check ids gl =
+  if ids = [] then tclIDTAC gl else refiner (Prim (Thin ids)) gl
+
+(* This does not check dependencies *)
+let thin_body_no_check ids gl =
+  if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
+
+let move_hyp_no_check with_dep id1 id2 gl = 
+  refiner (Prim (Move (with_dep,id1,id2))) gl
+
+let rename_hyp_no_check id1 id2 gl = 
+  refiner (Prim (Rename (id1,id2))) gl
+
+let mutual_fix f n others gl = 
+  with_check (refiner (Prim (FixRule (f,n,others)))) gl
+
+let mutual_cofix f others gl = 
+  with_check (refiner (Prim (Cofix (f,others)))) gl
+    
+let rename_bound_var_goal gls =
+  let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in 
+  let ids = ids_of_named_context sign in
+  convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls
+
+
+(* Versions with consistency checks *)
+
+let introduction id    = with_check (introduction_no_check id) 
+let intro_replacing id = with_check (intro_replacing_no_check id)
+let internal_cut d t     = with_check (internal_cut_no_check d t)
+let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
+let refine c           = with_check (refine_no_check c)
+let convert_concl d    = with_check (convert_concl_no_check d)
+let convert_hyp d      = with_check (convert_hyp_no_check d)
+let thin l             = with_check (thin_no_check l)
+let thin_body c        = with_check (thin_body_no_check c)
+let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
+let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
+    
+(* Pretty-printers *)
+
+open Pp
+open Printer
+open Tacexpr
+open Rawterm
+
+let rec pr_list f = function
+  | []   -> mt ()
+  | a::l1 -> (f a) ++ pr_list f l1
+
+let pr_gls gls =
+  hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls))
+
+let pr_glls glls =
+  hov 0 (pr_decls (sig_sig glls) ++ fnl () ++
+         prlist_with_sep pr_fnl pr_seq (sig_it glls))
+  
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
new file mode 100644
index 00000000..59b48da2
--- /dev/null
+++ b/proofs/tacmach.mli
@@ -0,0 +1,183 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: tacmach.mli,v 1.50.2.1 2004/07/16 19:30:50 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Environ
+open Evd
+open Reduction
+open Proof_trees
+open Proof_type
+open Refiner
+open Tacred
+open Tacexpr
+open Rawterm
+(*i*)
+
+(* Operations for handling terms under a local typing context. *)
+
+type 'a sigma   = 'a Proof_type.sigma;;
+type validation = Proof_type.validation;;
+type tactic     = Proof_type.tactic;;
+
+val sig_it  : 'a sigma   -> 'a
+val project : goal sigma -> evar_map
+
+val re_sig : 'a -> evar_map -> 'a sigma
+
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
+val apply_sig_tac :
+  evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+
+val pf_concl              : goal sigma -> types
+val pf_env                : goal sigma -> env
+val pf_hyps               : goal sigma -> named_context
+(*i val pf_untyped_hyps       : goal sigma -> (identifier * constr) list i*)
+val pf_hyps_types         : goal sigma -> (identifier * types) list
+val pf_nth_hyp_id         : goal sigma -> int -> identifier
+val pf_last_hyp           : goal sigma -> named_declaration
+val pf_ids_of_hyps        : goal sigma -> identifier list
+val pf_global             : goal sigma -> identifier -> constr
+val pf_parse_const        : goal sigma -> string -> constr
+val pf_type_of            : goal sigma -> constr -> types
+val pf_check_type         : goal sigma -> constr -> types -> unit
+val pf_execute            : goal sigma -> constr -> unsafe_judgment
+val hnf_type_of           : goal sigma -> constr -> types
+
+val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
+val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
+
+val pf_get_hyp            : goal sigma -> identifier -> named_declaration
+val pf_get_hyp_typ        : goal sigma -> identifier -> types
+
+val pf_get_new_id  : identifier      -> goal sigma -> identifier
+val pf_get_new_ids : identifier list -> goal sigma -> identifier list
+
+val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
+
+
+val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
+val pf_reduce : 
+  (env -> evar_map -> constr -> constr) ->
+    goal sigma -> constr -> constr
+
+val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
+val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list 
+val pf_hnf_constr              : goal sigma -> constr -> constr
+val pf_red_product             : goal sigma -> constr -> constr
+val pf_nf                      : goal sigma -> constr -> constr
+val pf_nf_betaiota             : goal sigma -> constr -> constr
+val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
+val pf_compute                 : goal sigma -> constr -> constr
+val pf_unfoldn    : (int list * evaluable_global_reference) list
+        -> goal sigma -> constr -> constr
+
+val pf_const_value : goal sigma -> constant -> constr
+val pf_conv_x      : goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+val frontier : transformation_tactic
+
+
+(*s Functions for handling the state of the proof editor. *)
+
+type pftreestate = Refiner.pftreestate
+
+val proof_of_pftreestate    : pftreestate -> proof_tree
+val cursor_of_pftreestate   : pftreestate -> int list
+val is_top_pftreestate      : pftreestate -> bool
+val evc_of_pftreestate      : pftreestate -> evar_map
+val top_goal_of_pftreestate : pftreestate -> goal sigma
+val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
+val traverse                : int -> pftreestate -> pftreestate
+val weak_undo_pftreestate   : pftreestate -> pftreestate
+val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
+val solve_pftreestate       : tactic -> pftreestate -> pftreestate
+val mk_pftreestate          : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_pftreestate     : pftreestate -> constr
+val first_unproven          : pftreestate -> pftreestate
+val last_unproven           : pftreestate -> pftreestate
+val nth_unproven            : int -> pftreestate -> pftreestate
+val node_prev_unproven      : int -> pftreestate -> pftreestate
+val node_next_unproven      : int -> pftreestate -> pftreestate
+val next_unproven           : pftreestate -> pftreestate
+val prev_unproven           : pftreestate -> pftreestate
+val top_of_tree             : pftreestate -> pftreestate
+val change_constraints_pftreestate :
+  evar_map -> pftreestate -> pftreestate
+
+(*
+val vernac_tactic : string * tactic_arg list -> tactic
+*)
+(*s The most primitive tactics. *)
+
+val refiner                   : rule -> tactic
+val introduction_no_check     : identifier -> tactic
+val intro_replacing_no_check  : identifier -> tactic
+val internal_cut_no_check     : identifier -> types -> tactic
+val internal_cut_rev_no_check : identifier -> types -> tactic
+val refine_no_check           : constr -> tactic
+val convert_concl_no_check    : types -> tactic
+val convert_hyp_no_check      : named_declaration -> tactic
+val thin_no_check             : identifier list -> tactic
+val thin_body_no_check        : identifier list -> tactic
+val move_hyp_no_check         : bool -> identifier -> identifier -> tactic
+val rename_hyp_no_check       : identifier -> identifier -> tactic
+val mutual_fix      :
+  identifier -> int -> (identifier * int * constr) list -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val rename_bound_var_goal : tactic
+
+(*s The most primitive tactics with consistency and type checking *)
+
+val introduction     : identifier -> tactic
+val intro_replacing  : identifier -> tactic
+val internal_cut     : identifier -> types -> tactic
+val internal_cut_rev : identifier -> types -> tactic
+val refine           : constr -> tactic
+val convert_concl    : constr -> tactic
+val convert_hyp      : named_declaration -> tactic
+val thin             : identifier list -> tactic
+val convert_concl    : types -> tactic
+val convert_hyp      : named_declaration -> tactic
+val thin             : identifier list -> tactic
+val thin_body        : identifier list -> tactic
+val move_hyp         : bool -> identifier -> identifier -> tactic
+val rename_hyp       : identifier -> identifier -> tactic
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+val first_goal         : 'a list sigma -> 'a sigma
+val goal_goal_list     : 'a sigma -> 'a list sigma
+val apply_tac_list     : tactic -> tactic_list
+val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
+val tactic_list_tactic : tactic_list -> tactic
+val tclFIRSTLIST       : tactic_list list -> tactic_list
+val tclIDTAC_list      : tactic_list
+
+(*s Pretty-printing functions. *)
+
+(*i*)
+open Pp
+(*i*)
+
+val pr_gls    : goal sigma -> std_ppcmds
+val pr_glls   : goal list sigma -> std_ppcmds
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
new file mode 100644
index 00000000..1fa1101d
--- /dev/null
+++ b/proofs/tactic_debug.ml
@@ -0,0 +1,179 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+open Ast
+open Names
+open Constrextern
+open Pp
+open Pptactic
+open Printer
+open Tacexpr
+open Termops
+
+let pr_glob_tactic x =
+  (if !Options.v7 then pr_glob_tactic else Pptacticnew.pr_glob_tactic (Global.env())) x
+
+(* This module intends to be a beginning of debugger for tactic expressions.
+   Currently, it is quite simple and we can hope to have, in the future, a more
+   complete panel of commands dedicated to a proof assistant framework *)
+
+(* Debug information *)
+type debug_info =
+  | DebugOn of int
+  | DebugOff
+
+(* An exception handler *)
+let explain_logic_error = ref (fun e -> mt())
+
+(* Prints the goal *)
+let db_pr_goal g =
+  msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g))
+
+(* Prints the commands *)
+let help () =
+  msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
+         str "          h/?=Help" ++ fnl() ++
+         str "          r<num>=Run <num> times" ++ fnl() ++
+         str "          s=Skip" ++ fnl() ++
+         str "          x=Exit")
+
+(* Prints the goal and the command to be executed *)
+let goal_com g tac =
+  begin
+    db_pr_goal g;
+    msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ())
+  end
+
+(* Gives the number of a run command *)
+let run_com inst =
+  if (String.get inst 0)='r' then
+    let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
+    if num>0 then num
+    else raise (Invalid_argument "run_com")
+  else
+    raise (Invalid_argument "run_com")
+
+let allskip = ref 0
+let skip = ref 0
+
+(* Prints the run counter *)
+let run ini =
+  if not ini then 
+    for i=1 to 2 do
+      print_char (Char.chr 8);print_char (Char.chr 13)
+    done;
+  msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ 
+       fnl() ++ fnl())
+
+(* Prints the prompt *)
+let rec prompt level =
+  begin
+    msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
+    flush stdout;
+    let inst = read_line () in
+    match inst with
+    | ""  -> true
+    | "s" -> false
+    | "x" -> print_char (Char.chr 8);skip:=0;allskip:=0;raise Sys.Break
+    | "h"| "?" ->
+      begin
+        help ();
+        prompt level
+      end
+    | _ ->
+      (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true
+       with Failure _ | Invalid_argument _ -> prompt level)
+  end
+
+(* Prints the state and waits for an instruction *)
+let debug_prompt lev g tac f =
+  (* What to print and to do next *)
+  let continue =
+    if !skip = 0 then (goal_com g tac; prompt lev)
+    else (decr skip; run false; if !skip=0 then allskip:=0; true) in
+  (* What to execute *)
+  try f (if continue then DebugOn (lev+1) else DebugOff)
+  with e ->
+    skip:=0; allskip:=0;
+    if Logic.catchable_exception e then
+      ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
+    raise e
+
+(* Prints a constr *)
+let db_constr debug env c =
+  if debug <> DebugOff & !skip = 0 then
+    msgnl (str "Evaluated term: " ++ prterm_env env c)
+
+(* Prints the pattern rule *)
+let db_pattern_rule debug num r =
+  if debug <> DebugOff & !skip = 0 then
+  begin
+    msgnl (str "Pattern rule " ++ int num ++ str ":");
+    msgnl (str "|" ++ spc () ++ 
+      pr_match_rule false Printer.pr_pattern pr_glob_tactic r)
+  end
+
+(* Prints the hypothesis pattern identifier if it exists *)
+let hyp_bound = function
+  | Anonymous -> " (unbound)"
+  | Name id -> " (bound to "^(Names.string_of_id id)^")"
+
+(* Prints a matched hypothesis *)
+let db_matched_hyp debug env (id,c) ido =
+  if debug <> DebugOff & !skip = 0 then
+    msgnl (str "Hypothesis " ++
+           str ((Names.string_of_id id)^(hyp_bound ido)^
+                " has been matched: ") ++ prterm_env env c)
+
+(* Prints the matched conclusion *)
+let db_matched_concl debug env c =
+  if debug <> DebugOff & !skip = 0 then
+    msgnl (str "Conclusion has been matched: " ++ prterm_env env c)
+
+(* Prints a success message when the goal has been matched *)
+let db_mc_pattern_success debug =
+  if debug <> DebugOff & !skip = 0 then
+    msgnl (str "The goal has been successfully matched!" ++ fnl() ++
+           str "Let us execute the right-hand side part..." ++ fnl())
+
+let pp_match_pattern env = function
+  | Term c -> Term (extern_pattern env (names_of_rel_context env) c)
+  | Subterm (o,c) ->
+    Subterm (o,(extern_pattern env (names_of_rel_context env) c))
+
+(* Prints a failure message for an hypothesis pattern *)
+let db_hyp_pattern_failure debug env (na,hyp) =
+  if debug <> DebugOff & !skip = 0 then
+    msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
+                " cannot match: ") ++
+           pr_match_pattern
+             (Printer.pr_pattern_env env (names_of_rel_context env))
+             hyp)
+
+(* Prints a matching failure message for a rule *)
+let db_matching_failure debug =
+  if debug <> DebugOff & !skip = 0 then
+    msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
+           str "Let us try the next one...")
+
+(* Prints an evaluation failure message for a rule *)
+let db_eval_failure debug s =
+  if debug <> DebugOff & !skip = 0 then
+    let s = if s="" then "no message" else "message \""^s^"\"" in
+    msgnl 
+      (str "This rule has failed due to \"Fail\" tactic (" ++
+       str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
+
+(* Prints a logic failure message for a rule *)
+let db_logic_failure debug err =
+  if debug <> DebugOff & !skip = 0 then
+  begin
+    msgnl (!explain_logic_error err);
+    msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
+           str "Let us try the next one...")
+  end
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
new file mode 100644
index 00000000..9ab263c4
--- /dev/null
+++ b/proofs/tactic_debug.mli
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: tactic_debug.mli,v 1.12.2.1 2004/07/16 19:30:50 herbelin Exp $ i*)
+
+open Environ
+open Pattern
+open Proof_type
+open Names
+open Tacexpr
+open Term
+
+(* This module intends to be a beginning of debugger for tactic expressions.
+   Currently, it is quite simple and we can hope to have, in the future, a more
+   complete panel of commands dedicated to a proof assistant framework *)
+
+(* Debug information *)
+type debug_info =
+  | DebugOn of int
+  | DebugOff
+
+(* Prints the state and waits *)
+val debug_prompt :
+  int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
+
+(* Prints a constr *)
+val db_constr : debug_info -> env -> constr -> unit
+
+(* Prints the pattern rule *)
+val db_pattern_rule :
+  debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit
+
+(* Prints a matched hypothesis *)
+val db_matched_hyp :
+  debug_info -> env -> identifier * constr -> name -> unit
+
+(* Prints the matched conclusion *)
+val db_matched_concl : debug_info -> env -> constr -> unit
+
+(* Prints a success message when the goal has been matched *)
+val db_mc_pattern_success : debug_info -> unit
+
+(* Prints a failure message for an hypothesis pattern *)
+val db_hyp_pattern_failure :
+  debug_info -> env -> name * constr_pattern match_pattern -> unit
+
+(* Prints a matching failure message for a rule *)
+val db_matching_failure : debug_info -> unit
+
+(* Prints an evaluation failure message for a rule *)
+val db_eval_failure : debug_info -> string -> unit
+
+(* An exception handler *)
+val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+
+(* Prints a logic failure message for a rule *)
+val db_logic_failure : debug_info -> exn -> unit
diff --git a/proofs/tmp-src b/proofs/tmp-src
new file mode 100644
index 00000000..1da11fe0
--- /dev/null
+++ b/proofs/tmp-src
@@ -0,0 +1,56 @@
+
+(********* INSTANTIATE ****************************************************)
+
+(* existential_type gives the type of an existential *)
+let existential_type env k = 
+  let (sp,args) = destConst k in
+  let evd = Evd.map (evar_map env) sp in
+  instantiate_constr 
+    (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args)
+
+(* existential_value gives the value of a defined existential *)
+let existential_value env k =
+  let (sp,args) = destConst k in
+  if defined_const env k then
+    let evd = Evd.map (evar_map env) sp in
+    match evd.evar_body with
+      | EVAR_DEFINED c ->
+ 	  instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args)
+      | _ -> anomalylabstrm "termenv__existential_value"
+            [< 'sTR"The existential variable code just registered a" ;
+               'sPC ; 'sTR"grave internal error." >]
+  else 
+    failwith "undefined existential"
+
+
+(******* REDUCTION ********************************************************)
+
+
+(************ REDUCTION.MLI **********************************************)
+
+(*********** TYPEOPS *****************************************************)
+
+
+(* Constants or existentials. *)
+
+let type_of_constant_or_existential env c =
+  if is_existential c then
+    type_of_existential env c
+  else
+    type_of_constant env c
+
+
+(******** TYPING **********************************************************)
+
+    | IsMeta n ->
+       	let metaty =
+          try lookup_meta n env
+          with Not_found -> error "A variable remains non instanciated" 
+	in
+        (match kind_of_term metaty with
+           | IsCast (typ,kind) -> 
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0)
+           | _ ->
+	       let (jty,cst) = execute mf env metaty in
+	       let k = whd_betadeltaiotaeta env jty.uj_type in
+	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst))