Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

23 files changed, 655 insertions, 2348 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
deleted file mode 100644
index 999bb651..00000000
--- a/proofs/clenv.ml
+++ /dev/null
@@ -1,1175 +0,0 @@
-(************************************************************************)
-(*  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.4 2004/12/06 12:59:11 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;
-    mkCast (mkMeta n, ty) 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
deleted file mode 100644
index 737fbea3..00000000
--- a/proofs/clenv.mli
+++ /dev/null
@@ -1,142 +0,0 @@
-(************************************************************************)
-(*  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.2 2005/01/21 16:41:51 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
-(*i
-val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
-i*)
-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/clenvtac.ml b/proofs/clenvtac.ml
new file mode 100644
index 00000000..71538614
--- /dev/null
+++ b/proofs/clenvtac.ml
@@ -0,0 +1,97 @@
+(************************************************************************)
+(*  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: clenvtac.ml 8023 2006-02-10 18:34:51Z coq $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Environ
+open Evd
+open Evarutil
+open Proof_type
+open Refiner
+open Proof_trees
+open Logic
+open Reduction
+open Reductionops
+open Tacmach
+open Evar_refiner
+open Rawterm
+open Pattern
+open Tacexpr
+open Clenv
+
+    
+(* 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 
+            let b = Typing.meta_type clenv.env mv in
+	    if occur_meta b then u
+            else mkCast (mkMeta mv, DEFAULTcast, b)
+	  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
+
+let clenv_refine clenv gls =
+  tclTHEN
+    (tclEVARS (evars_of clenv.env)) 
+    (refine (clenv_cast_meta clenv (clenv_value clenv)))
+    gls
+
+
+let res_pf clenv ?(allow_K=false) gls =
+  clenv_refine (clenv_unique_resolver allow_K clenv gls) gls
+
+let elim_res_pf_THEN_i clenv tac gls =  
+  let clenv' = (clenv_unique_resolver true clenv gls) in
+  tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
+
+
+let e_res_pf clenv gls =
+  clenv_refine (evar_clenv_unique_resolver clenv gls) gls
+
+
+
+
+(* [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 = 
+  let env = pf_env gls in
+  let evd = create_evar_defs (project gls) in
+  let evd' = Unification.w_unify false env CONV m n evd in
+  tclIDTAC {it = gls.it; sigma = evars_of evd'}
+
+let unify m gls =
+  let n = pf_concl gls in unifyTerms m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
new file mode 100644
index 00000000..505826fa
--- /dev/null
+++ b/proofs/clenvtac.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  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: clenvtac.mli 6099 2004-09-12 11:38:09Z barras $ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Evd
+open Clenv
+open Proof_type
+(*i*)
+
+(* Tactics *)
+val unify : constr -> tactic
+val clenv_refine : clausenv -> tactic
+val res_pf : clausenv -> ?allow_K:bool -> tactic
+val e_res_pf : clausenv -> tactic
+val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ac4dd43a..4ee8001c 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,183 +6,44 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml,v 1.36.2.2 2004/08/03 21:37:27 herbelin Exp $ *)
+(* $Id: evar_refiner.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
 
-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 *)
+(* w_tactic pour instantiate *) 
 
-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 w_refine env ev rawc evd =
+  if Evd.is_defined (evars_of evd) ev then 
+    error "Instantiate called on already-defined evar";
+  let e_info = Evd.map (evars_of evd) ev in
+  let env = Evd.evar_env e_info in
+  let sigma,typed_c = 
+    Pretyping.Default.understand_tcc (evars_of evd) env 
+      ~expected_type:e_info.evar_concl rawc in
+  evar_define ev typed_c (evars_reset_evd sigma evd)
 
-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 *)
+(* 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) = 
+  let sigma = gls.sigma in 
+  let (sp,evi) (* as evc *) = 
     try
-      List.nth (Evd.non_instantiated sigma) (n-1) 
+      List.nth (Evarutil.non_instantiated sigma) (n-1) 
     with Failure _ -> 
-      error "not so many uninstantiated existential variables"
-      | Invalid_argument _ -> error "incorrect existential variable index"
-  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
-
-
+      error "not so many uninstantiated existential variables" in 
+  let env = Evd.evar_env evi in
+  let rawc = Constrintern.intern_constr sigma env com in 
+  let evd = create_evar_defs sigma in
+  let evd' = w_refine env sp rawc evd in
+  change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index d57e1b84..9880f2f0 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,52 +6,21 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_refiner.mli,v 1.28.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: evar_refiner.mli 6616 2005-01-21 17:18:23Z herbelin $ 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_refine :  env -> evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
 
-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_pf_com :
+  int -> Topconstr.constr_expr -> pftreestate -> pftreestate
 
-val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic
-(*i
-val instantiate_tac : tactic_arg list -> tactic
-i*)
-val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index cefeb8ae..1f79d73c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *)
+(* $Id: logic.ml 8696 2006-04-11 07:05:50Z herbelin $ *)
 
 open Pp
 open Util
@@ -25,7 +25,6 @@ open Proof_trees
 open Proof_type
 open Typeops
 open Type_errors
-open Coqast
 open Retyping
 open Evarutil
  
@@ -40,114 +39,72 @@ type refiner_error =
   | 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 _) | 
-    Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true
+let rec catchable_exception = function
+  | Stdpp.Exc_located(_,e) -> catchable_exception e
+  | Util.UserError _ | TypeError _ 
+  | RefinerError _ | Indrec.RecursionSchemeError _
+  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  (* unification errors *)
+  | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _|
+      CannotUnifyBindingType _|NotClean _)) -> 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;
-  try let r = tac gl in check := c; r with e -> check := c; raise e
-
 let with_check = Options.with_option check
-   
+
 (************************************************************************)
 (************************************************************************)
 (* 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 (nhyps,cleared_ids) =
+    let fcheck cleared_ids (id,_,_ as d)  =
+      if !check && cleared_ids<>[] then
+	Idset.iter
+	  (fun id' ->
+            if List.mem id' cleared_ids then
+              error (string_of_id id'^
+		        " is used in hypothesis "^string_of_id id))
+	  (global_vars_set_of_decl env d) in
+    clear_hyps ids fcheck gl.evar_hyps in
   let ncl = gl.evar_concl in
-  check_clear_forward rmv (global_vars_set env ncl) "conclusion";
+  if !check && cleared_ids<>[] then
+    Idset.iter
+      (fun id' ->
+        if List.mem id' cleared_ids then
+          error (string_of_id id'^" is used in conclusion"))
+      (global_vars_set env ncl);
   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)] *)
+   returns [tail::(f head (id,_,_) (rev 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"
+  try apply_to_hyp sign id f 
+  with Hyp_not_found -> 
+    if !check then error "No such assumption"
+    else sign
 
 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"
+  try apply_to_hyp_and_dependent_on sign id f g 
+  with Hyp_not_found -> 
+    if !check then error "No such assumption"
+    else sign
 
 let check_typability env sigma c =
   if !check then let _ = type_of env sigma c in () 
@@ -162,26 +119,24 @@ let recheck_typability (what,id) env sigma t =
       ("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')
-
+  let sign =
+    apply_to_hyp_and_dependent_on (named_context_val env) id
+      (fun (_,c,t) _ ->
+	match c with
+	| None -> error ((string_of_id id)^" is not a local definition")
+	| Some c ->(id,None,t))
+      (fun (id',c,t as d) sign ->
+	(if !check then
+	  begin 
+	    let env = reset_with_named_context sign env in
+	    match c with
+	    | None ->  recheck_typability (Some id',id) env sigma t
+	    | Some b ->
+		let b' = mkCast (b,DEFAULTcast, t) in
+		recheck_typability (Some id',id) env sigma b'
+	  end;d))
+  in
+  reset_with_named_context sign env 
 
 (* Auxiliary functions for primitive MOVE tactic
  *
@@ -231,9 +186,16 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	  moverec first' middle' right
   in
   if toleft then 
-    List.rev_append (moverec [] [declfrom] left) right
+    let right = 
+      List.fold_right push_named_context_val right empty_named_context_val in
+    List.fold_left (fun sign d -> push_named_context_val d sign)
+      right (moverec [] [declfrom] left) 
   else 
-    List.rev_append left (moverec [] [declfrom] right)
+    let right = 
+      List.fold_right push_named_context_val
+	(moverec [] [declfrom] right) empty_named_context_val in
+    List.fold_left (fun sign d -> push_named_context_val d sign)
+      right left
 
 let check_backward_dependencies sign d =
   if not (Idset.for_all
@@ -255,8 +217,8 @@ let check_forward_dependencies 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]))
+    (fun (_,b,t) _ -> (id2,b,t))
+    (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 
 let replace_hyp sign id d =
   apply_to_hyp sign id
@@ -264,13 +226,17 @@ let replace_hyp sign id d =
        if !check then
 	 (check_backward_dependencies sign d;
 	  check_forward_dependencies id tail);
-       add_named_decl d sign)
+       d)
 
+(* why we dont check that id does not appear in tail ??? *)
 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))
+  try 
+    insert_after_hyp sign id d 
+      (fun sign ->
+	if !check then check_backward_dependencies sign d)
+  with Hyp_not_found ->
+    if !check then error "No such assumption"
+    else sign
 
 (************************************************************************)
 (************************************************************************)
@@ -282,7 +248,7 @@ 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
+    | Cast(c,_,_) -> collrec acc c
     | (App _| Case _) -> fold_constr collrec acc c
     | _ -> acc
   in 
@@ -311,13 +277,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
           raise (RefinerError (OccurMetaGoal conclty));
 	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
-    | Cast (t,ty) ->
+    | 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',hdty) =
+	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
+	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  else 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;
@@ -346,12 +316,20 @@ 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 ->
+    | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
 	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
 
+    | Cast (t,_, ty) ->
+	check_typability env sigma ty;
+	mk_refgoals sigma goal goalacc ty t
+
     | App (f,l) ->
-	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc',hdty) = 
+	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
+	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  else mk_hdgoals sigma goal goalacc f
+	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
 
     | Case (_,p,c,lf) ->
@@ -397,16 +375,13 @@ let error_use_instantiate () =
 
 let convert_hyp sign sigma (id,b,bt as d) =
   apply_to_hyp sign id
-    (fun sign (_,c,ct) _ ->
+    (fun _ (_,c,ct) _ ->
        let env = Global.env_of_context sign in
        if !check && not (is_conv env sigma bt ct) then
-	 (* Just a warning in V8.0bugfix for compatibility *)
-	 msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ 
-	       str " (not well-typed in current signature)");
+	 error ("Incorrect change of the type of "^(string_of_id id));
        if !check && not (option_compare (is_conv env sigma) b c) then
-	 msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++
-	       str " (not well-typed in current signature)");
-       add_named_decl d sign)
+	 error ("Incorrect change of the body of "^(string_of_id id));
+       d)
 
 
 (************************************************************************)
@@ -420,18 +395,18 @@ let prim_refiner r sigma goal =
   match r with
     (* Logical rules *)
     | Intro id ->
-    	if !check && mem_named_context id sign then
+    	if !check && mem_named_context id (named_context_of_val 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)
+	       let sg = mk_goal (push_named_context_val (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)
+		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -453,11 +428,11 @@ let prim_refiner r sigma goal =
 	       raise (RefinerError IntroNeedsProduct))
 	
     | Cut (b,id,t) ->
-    	if !check && mem_named_context id sign then
+    	if !check && mem_named_context id (named_context_of_val 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
+        let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in
         if b then [sg1;sg2] else [sg2;sg1]  
 
     | FixRule (f,n,rest) ->
@@ -481,9 +456,9 @@ let prim_refiner r sigma goal =
 	      if not (sp=sp') then 
 		error ("fixpoints should be on the same " ^ 
 		       "mutual inductive declaration");
-	      if !check && mem_named_context f sign then 
+	      if !check && mem_named_context f (named_context_of_val sign) then
 		error "name already used in the environment";
-	      mk_sign (add_named_decl (f,None,ar) sign) oth
+	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
@@ -506,11 +481,11 @@ let prim_refiner r sigma goal =
         let rec mk_sign sign = function 
           | (f,ar)::oth ->
 	      (try
-                (let _ = Sign.lookup_named f sign in
+                (let _ = lookup_named_val f sign in
                 error "name already used in the environment")
               with
               |	Not_found ->
-                  mk_sign (add_named_decl (f,None,ar) sign) oth)
+                  mk_sign (push_named_context_val (f,None,ar) sign) oth)
 	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
      	in 
 	mk_sign sign all
@@ -523,7 +498,7 @@ let prim_refiner r sigma goal =
 	sgl
 
     (* Conversion rules *)
-    | Convert_concl cl' ->
+    | 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
@@ -544,18 +519,20 @@ let prim_refiner r sigma goal =
           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 sign' = named_context_val (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 (left,right,declfrom,toleft) = 
+	  split_sign hfrom hto (named_context_of_val sign) in
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
   	[mk_goal hyps' cl]
 
     | Rename (id1,id2) ->
-        if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then
+        if !check & id1 <> id2 &&
+	  List.mem id2 (ids_of_named_context (named_context_of_val 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
@@ -566,15 +543,39 @@ let prim_refiner r sigma goal =
 (* Extracting a proof term from the proof tree *)
 
 (* Util *)
+
+type variable_proof_status = ProofVar | SectionVar of identifier
+
+type proof_variable = name * variable_proof_status
+
+let subst_proof_vars = 
+  let rec aux p vars =
+    let _,subst =
+      List.fold_left (fun (n,l) var ->
+        let t = match var with
+          | Anonymous,_ -> l
+          | Name id, ProofVar -> (id,mkRel n)::l
+          | Name id, SectionVar id' -> (id,mkVar id')::l in
+        (n+1,t)) (p,[]) vars
+    in replace_vars (List.rev subst)
+  in aux 1
+         
 let rec rebind id1 id2 = function
-  | [] -> []
-  | id::l -> 
-      if id = id1 then id2::l else
+  | [] -> [Name id2,SectionVar id1]
+  | (na,_ as x)::l -> 
+      if na = Name id1 then (Name id2,ProofVar)::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'
+        if na = Name id2 then (Anonymous,ProofVar)::l' else x::l'
+
+let add_proof_var id vl = (Name id,ProofVar)::vl
+
+let proof_variable_index x = 
+  let rec aux n = function
+    | (Name id,ProofVar)::l when x = id -> n
+    | _::l ->  aux (n+1) l
+    | [] -> raise Not_found
+  in 
+  aux 1
 
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
@@ -582,61 +583,64 @@ let prim_extractor subfun vl pft =
     | 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)
+	       let cty = subst_proof_vars vl ty in
+	       mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
 	   | LetIn (_,b,ty,_) ->
-	       let cb = subst_vars vl b in
-	       let cty = subst_vars vl ty in
-	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
+	       let cb = subst_proof_vars vl b in
+	       let cty = subst_proof_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | Some (Prim (Intro_replacing id),[spf]) ->
 	(match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,ty,_) ->
-	       let cty = subst_vars vl ty in
-	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	       let cty = subst_proof_vars vl ty in
+	       mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
 	   | LetIn (_,b,ty,_) ->
-	       let cb = subst_vars vl b in
-	       let cty = subst_vars vl ty in
-	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
+	       let cb = subst_proof_vars vl b in
+	       let cty = subst_proof_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
 	   | _ -> error "incomplete proof!")
 
     | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
         let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
-	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)
+	mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
+                 subfun (add_proof_var id vl) spf2)
 
     | Some (Prim (FixRule (f,n,others)),spfl) ->
 	let all = Array.of_list ((f,n,cl)::others) in
-	let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all in
+	let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
 	let names = Array.map (fun (f,_,_) -> Name f) all in
 	let vn = Array.map (fun (_,n,_) -> n-1) all in
-	let newvl = List.fold_left (fun vl (id,_,_)->(id::vl)) (f::vl)others in
+	let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
+          (add_proof_var f vl) others in
 	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
 	mkFix ((vn,0),(names,lcty,lfix))	
 
     | Some (Prim (Cofix (f,others)),spfl) ->
 	let all = Array.of_list ((f,cl)::others) in
-	let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all in
+	let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
 	let names  = Array.map (fun (f,_) -> Name f) all in
-	let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (f::vl) others in 
+	let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
+          (add_proof_var f vl) others in 
 	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
 	mkCoFix (0,(names,lcty,lfix))
 	  
     | Some (Prim (Refine c),spfl) ->
 	let mvl = collect_meta_variables c in
 	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
-	let cc = subst_vars vl c in 
+	let cc = subst_proof_vars vl c in 
 	plain_instance metamap cc
 
     (* Structural and conversion rules do not produce any proof *)
-    | Some (Prim (Convert_concl _),[pf]) ->
-	subfun vl pf
-	
+    | Some (Prim (Convert_concl (t,k)),[pf]) ->
+	if k = DEFAULTcast then subfun vl pf
+	else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
     | Some (Prim (Convert_hyp _),[pf]) ->
 	subfun vl pf
 
     | Some (Prim (Thin _),[pf]) ->
-     (* No need to make ids Anonymous in vl: subst_vars take the more recent *)
+     (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
 	subfun vl pf
 	
     | Some (Prim (ThinBody _),[pf]) ->
@@ -652,133 +656,3 @@ let prim_extractor subfun vl pft =
 
     | 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
index 7eef22bd..ab65b1d5 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: logic.mli,v 1.27.6.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+(*i $Id: logic.mli 8107 2006-03-01 17:34:36Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -20,7 +20,6 @@ open Proof_type
 (* 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:\\
@@ -37,9 +36,13 @@ val with_check    : tactic -> tactic
 
 val prim_refiner : prim_rule -> evar_map -> goal -> goal list
 
+type proof_variable
+
 val prim_extractor :
-  (identifier list -> proof_tree -> constr)
-  -> identifier list -> proof_tree -> constr
+  (proof_variable list -> proof_tree -> constr)
+  -> proof_variable list -> proof_tree -> constr
+
+val proof_variable_index : identifier -> proof_variable list -> int
 
 (*s Refiner errors. *)
 
@@ -54,20 +57,9 @@ type refiner_error =
   | 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
index f53ea870..fa6f8c37 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pfedit.ml,v 1.47.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+(* $Id: pfedit.ml 6947 2005-04-20 16:18:41Z coq $ *)
 
 open Pp
 open Util
@@ -19,7 +19,7 @@ open Entries
 open Environ
 open Evd
 open Typing
-open Tacmach
+open Refiner
 open Proof_trees
 open Tacexpr
 open Proof_type
@@ -33,7 +33,6 @@ open Safe_typing
 
 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 }
@@ -175,6 +174,21 @@ let undo n =
   with (Invalid_argument "Edit.undo") ->
     errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
 
+(* Undo current focused proof to reach depth [n]. This is used in
+   [vernac_backtrack]. *)
+let undo_todepth n =
+  try 
+    Edit.undo_todepth proof_edits n
+  with (Invalid_argument "Edit.undo") ->
+    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
+
+(* Return the depth of the current focused proof stack, this is used
+   to put informations in coq prompt (in emacs mode). *)
+let current_proof_depth() = 
+  try
+    Edit.depth proof_edits
+  with (Invalid_argument "Edit.depth") -> -1
+
 (*********************************************************************)
 (*                  Proof cooking                                    *)
 (*********************************************************************)
@@ -192,7 +206,8 @@ let cook_proof () =
   (ident,
    ({ const_entry_body = pfterm;
       const_entry_type = Some concl;
-      const_entry_opaque = true },
+      const_entry_opaque = true;
+      const_entry_boxed = false},
     strength, ts.top_hook))
 
 let current_proof_statement () = 
@@ -231,7 +246,6 @@ 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}
@@ -274,11 +288,11 @@ let common_ancestor l1 l2 =
       
 let rec traverse_up = function
   | 0 -> (function pf -> pf)
-  | n -> (function pf -> Tacmach.traverse 0 (traverse_up (n - 1) pf))
+  | n -> (function pf -> Refiner.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))
+  | n::l -> (function pf -> Refiner.traverse n (traverse_down l pf))
 
 let traverse_to path =
   let up_and_down path pfs =
@@ -305,29 +319,3 @@ 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
index e95881ba..ca379d2e 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
 (*         *       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 $Id: pfedit.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
 
 (*i*)
 open Util
@@ -57,6 +57,14 @@ val delete_all_proofs : unit -> unit
 
 val undo : int -> unit
 
+(* Same as undo, but undoes the current proof stack to reach depth
+   [n]. This is used in [vernac_backtrack]. *)
+val undo_todepth : int -> unit
+
+(* Returns the depth of the current focused proof stack, this is used
+   to put informations in coq prompt (in emacs mode). *)
+val current_proof_depth: unit -> int
+
 (* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
    sets the size to the default value (12) *)
 
@@ -68,7 +76,7 @@ val get_undo : unit -> int option
     declare the built constructions as a coercion or a setoid morphism) *)
 
 val start_proof : 
-  identifier -> goal_kind -> named_context -> constr
+  identifier -> goal_kind -> named_context_val -> constr
     -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
@@ -176,8 +184,3 @@ val traverse_prev_unproven : unit -> unit
    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
index aaf54a36..7e299b89 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
 (*         *       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 $ *)
+(* $Id: proof_trees.ml 6113 2004-09-17 20:28:19Z barras $ *)
 
 open Closure
 open Util
@@ -66,29 +66,6 @@ let is_tactic_proof pf = match pf.ref with
   | _ -> 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
 
@@ -100,154 +77,12 @@ let pf_lookup_index_as_renamed env ccl n =
 (*********************************************************************)
 
 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 db_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
+  let penv = print_named_context env in
+  let pc = print_constr_env 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
index c31d5207..cbf91c8a 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -6,7 +6,7 @@
 (*         *       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 $Id: proof_trees.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
 
 (*i*)
 open Util
@@ -21,7 +21,7 @@ open Proof_type
 (* This module declares readable constraints, and a few utilities on
    constraints and proof trees *)
 
-val mk_goal : named_context -> constr -> goal
+val mk_goal : named_context_val -> constr -> goal
 
 val rule_of_proof     : proof_tree -> rule
 val ref_of_proof      : proof_tree -> (rule * proof_tree list)
@@ -33,16 +33,6 @@ 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
 
@@ -53,16 +43,4 @@ val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 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
+val db_pr_goal : goal -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index cbed5e27..009e9d5b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml,v 1.29.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+(*i $Id: proof_type.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
 
 (*i*)
 open Environ
@@ -32,19 +32,13 @@ type prim_rule =
   | FixRule of identifier * int * (identifier * int * constr) list
   | Cofix of identifier * (identifier * constr) list
   | Refine of constr
-  | Convert_concl of types
+  | Convert_concl of types * cast_kind
   | 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
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 42606552..0e42dcba 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.mli,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+(*i $Id: proof_type.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
 
 (*i*)
 open Environ
@@ -32,7 +32,7 @@ type prim_rule =
   | FixRule of identifier * int * (identifier * int * constr) list
   | Cofix of identifier * (identifier * constr) list
   | Refine of constr
-  | Convert_concl of types
+  | Convert_concl of types * cast_kind 
   | Convert_hyp of named_declaration
   | Thin of identifier list
   | ThinBody of identifier list
@@ -67,12 +67,6 @@ type prim_rule =
 \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
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
new file mode 100644
index 00000000..8b3b5f5f
--- /dev/null
+++ b/proofs/redexpr.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(*  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: redexpr.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Libnames
+open Rawterm
+open Reductionops
+open Tacred
+open Closure
+open RedFlags
+
+
+(* call by value normalisation function using the virtual machine *)
+let cbv_vm env _ c =
+  let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
+  Vconv.cbv_vm env c ctyp
+
+
+let set_opaque_const sp = 
+  Conv_oracle.set_opaque_const sp;
+  Csymtable.set_opaque_const sp
+
+let set_transparent_const sp =
+  let cb = Global.lookup_constant sp in
+  if cb.const_body <> None & cb.const_opaque then
+    errorlabstrm "set_transparent_const"
+      (str "Cannot make" ++ spc () ++ 
+         Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+         spc () ++ str "transparent because it was declared opaque.");
+  Conv_oracle.set_transparent_const sp;
+  Csymtable.set_transparent_const sp
+
+let set_opaque_var      = Conv_oracle.set_opaque_var
+let set_transparent_var = Conv_oracle.set_transparent_var
+
+let _ = 
+  Summary.declare_summary "Transparent constants and variables"
+    { Summary.freeze_function = Conv_oracle.freeze;
+      Summary.unfreeze_function = Conv_oracle.unfreeze;
+      Summary.init_function = Conv_oracle.init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+
+(* Generic reduction: reduction functions used in reduction tactics *)
+
+type red_expr = (constr, evaluable_global_reference) red_expr_gen
+
+
+let make_flag_constant = function
+  | EvalVarRef id -> fVAR id
+  | EvalConstRef sp -> fCONST sp
+
+let make_flag f =
+  let red = no_red in
+  let red = if f.rBeta then red_add red fBETA else red in
+  let red = if f.rIota then red_add red fIOTA else red in
+  let red = if f.rZeta then red_add red fZETA else red in
+  let red =
+    if f.rDelta then (* All but rConst *)
+        let red = red_add red fDELTA in
+        let red = red_add_transparent red (Conv_oracle.freeze ()) in
+	List.fold_right
+	  (fun v red -> red_sub red (make_flag_constant v))
+	  f.rConst red
+    else (* Only rConst *)
+        let red = red_add_transparent (red_add red fDELTA) all_opaque in
+	List.fold_right
+	  (fun v red -> red_add red (make_flag_constant v))
+	  f.rConst red
+  in red
+
+let is_reference c = 
+  try let _ref = global_of_constr c in true with _ -> false
+
+let red_expr_tab = ref Stringmap.empty
+
+let declare_red_expr s f =
+  try 
+    let _ = Stringmap.find s !red_expr_tab in
+    error ("There is already a reduction expression of name "^s)
+  with Not_found ->
+    red_expr_tab := Stringmap.add s f !red_expr_tab
+
+let reduction_of_red_expr = function
+  | Red internal -> 
+      if internal then (try_red_product,DEFAULTcast) 
+      else (red_product,DEFAULTcast)
+  | Hnf -> (hnf_constr,DEFAULTcast)
+  | Simpl (Some (_,c as lp)) -> 
+      (contextually (is_reference c) lp nf,DEFAULTcast)
+  | Simpl None -> (nf,DEFAULTcast)
+  | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
+  | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
+  | Unfold ubinds -> (unfoldn ubinds,DEFAULTcast)
+  | Fold cl -> (fold_commands cl,DEFAULTcast)
+  | Pattern lp -> (pattern_occs lp,DEFAULTcast)
+  | ExtraRedExpr s ->
+      (try (Stringmap.find s !red_expr_tab,DEFAULTcast)
+      with Not_found -> error("unknown user-defined reduction \""^s^"\""))
+  | CbvVm -> (cbv_vm ,VMcast)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
new file mode 100644
index 00000000..c442b16e
--- /dev/null
+++ b/proofs/redexpr.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  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: redexpr.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+
+open Names
+open Term
+open Closure
+open Rawterm
+open Reductionops
+
+
+type red_expr = (constr, evaluable_global_reference) red_expr_gen
+
+val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
+(* [true] if we should use the vm to verify the reduction *)
+
+val declare_red_expr : string -> reduction_function -> unit
+
+(* Opaque and Transparent commands. *)
+val set_opaque_const      : constant -> unit
+val set_transparent_const : constant -> unit
+
+val set_opaque_var      : identifier -> unit
+val set_transparent_var : identifier -> unit
+
+
+
+(* call by value normalisation function using the virtual machine *)
+val cbv_vm : reduction_function
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 785e6dd4..2b878d37 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml,v 1.67.2.3 2005/11/04 08:59:30 herbelin Exp $ *)
+(* $Id: refiner.ml 8708 2006-04-14 08:13:02Z jforest $ *)
 
 open Pp
 open Util
@@ -17,12 +17,10 @@ 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)
 
@@ -30,10 +28,7 @@ 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 project x = x.sigma
 
 let pf_status pf = pf.open_subgoals
 
@@ -43,6 +38,11 @@ let on_open_proofs f pf = if is_complete pf then pf else f pf
 
 let and_status = List.fold_left (+) 0
 
+(* Getting env *)
+
+let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
+let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
+
 (* 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 *)
@@ -51,13 +51,9 @@ let norm_goal sigma gl =
   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_hyps = map_named_val red_fun gl.evar_hyps; 
       evar_body = gl.evar_body} in
-  if ngl = gl then None else Some ngl
+  if Evd.eq_evar_info ngl gl then None else Some ngl
 
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -85,7 +81,7 @@ let rec frontier p =
 	([p.goal],
 	 (fun lp' -> 
 	    let p' = List.hd lp' in
-            if p'.goal = p.goal then 
+            if Evd.eq_evar_info p'.goal p.goal then 
 	      p'
             else 
 	      errorlabstrm "Refiner.frontier"
@@ -105,7 +101,7 @@ let rec frontier_map_rec f n p =
   match p.ref with
     | None -> 
         let p' = f p in
-        if p'.goal == p.goal || p'.goal = p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then p'
         else 
 	  errorlabstrm "Refiner.frontier_map"
             (str"frontier_map was handed back a ill-formed proof.")
@@ -131,7 +127,7 @@ let rec frontier_mapi_rec f i p =
   match p.ref with
     | None -> 
         let p' = f i p in
-        if p'.goal == p.goal || p'.goal = p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then p'
         else 
 	  errorlabstrm "Refiner.frontier_mapi"
             (str"frontier_mapi was handed back a ill-formed proof.")
@@ -189,7 +185,7 @@ let lookup_tactic s =
 (* refiner r is a tactic applying the rule r *)
 
 let check_subproof_connection gl spfl =
-  list_for_all2eq (fun g pf -> g=pf.goal) gl spfl
+  list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
 
 let abstract_tactic_expr te tacfun gls =
   let (sgl_sigma,v) = tacfun gls in
@@ -255,12 +251,6 @@ 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
@@ -292,13 +282,13 @@ let extract_open_proof sigma pf =
 	let visible_rels =
           map_succeed
             (fun id ->
-               try let n = list_index id vl in (n,id)
+               try let n = proof_variable_index id vl in (n,id)
 	       with Not_found -> failwith "caught")
-            (ids_of_named_context goal.evar_hyps) in
+            (ids_of_named_context (named_context_of_val 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))
+          List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps))
             sorted_rels in
 	let abs_concl =
           List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
@@ -308,7 +298,7 @@ let extract_open_proof sigma pf =
 	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"
+    | _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
   in
   let pfterm = proof_extractor [] pf in
   (pfterm, List.rev !open_obligations)
@@ -345,17 +335,13 @@ 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
+  msg (hov 0 s); tclIDTAC gls
 
 (* 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
+exception FailError of int * std_ppcmds
 
 (* The Fail tactic *)
 let tclFAIL lvl s g = raise (FailError (lvl,s))
@@ -469,7 +455,7 @@ let rec tclTHENLIST = function
 
 (* various progress criterions *)
 let same_goal gl subgoal = 
-  (hypotheses subgoal) = (hypotheses gl) &
+  eq_named_context_val (hypotheses subgoal) (hypotheses gl) &&
   eq_constr (conclusion subgoal) (conclusion gl)
 
 
@@ -774,15 +760,16 @@ let extract_pftreestate pts =
       (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
-  let exl = Evd.non_instantiated pts.tpfsigma in 
+  let exl = Evarutil.non_instantiated pts.tpfsigma in
   if subgoals <> [] or exl <> [] then
-   errorlabstrm "extract_proof"
-   (if subgoals <> [] then 
-     str "Attempt to save an incomplete proof"
-    else
-      str "Attempt to save a proof with existential variables still non-instantiated");
+    errorlabstrm "extract_proof"
+      (if subgoals <> [] then
+        str "Attempt to save an incomplete proof"
+      else
+        str "Attempt to save a proof with existential variables still non-instantiated");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
-  strong whd_betaiotaevar env pts.tpfsigma pfterm
+  nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+  (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
   (***
   local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
   ***)
@@ -894,136 +881,21 @@ let rec top_of_tree pts =
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
 
-(* Pretty-printers. *)
+(* Change evars *)
+let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 
-open Pp
+(* Pretty-printers. *)
 
-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 pp_info = ref (fun _ _ _ -> assert false)
+let set_info_printer f = pp_info := f
 
 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
+    let sign = named_context_of_val (sig_it gls).evar_hyps in
     msgnl (hov 0 (str" == " ++
-                  print_subscript (sig_sig gls) sign pf))
+                  !pp_info (project gls) sign pf))
   with e when catchable_exception e -> 
     msgnl (hov 0 (str "Info failed to apply validation"))
   end;
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index f6f2082e..417ddbcd 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: refiner.mli,v 1.31.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: refiner.mli 7911 2006-01-21 11:18:36Z herbelin $ i*)
 
 (*i*)
 open Term
@@ -20,9 +20,10 @@ open Tacexpr
 (* The refiner (handles primitive rules and high-level tactics). *)
 
 val sig_it  : 'a sigma -> 'a
-val sig_sig : 'a sigma -> evar_map
+val project : 'a sigma -> evar_map
 
-val project_with_focus : goal sigma -> named_context sigma
+val pf_env  : goal sigma -> Environ.env
+val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
@@ -65,8 +66,10 @@ val frontier_mapi :
 
 (* [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
-val tclIDTAC_MESSAGE  : string -> tactic
+val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
 
+(* [tclEVARS sigma] changes the current evar map *)
+val tclEVARS : evar_map -> tactic
 
 (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
@@ -120,7 +123,7 @@ val tclTHENLASTn    : tactic -> tactic array -> tactic
 val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int * string
+exception FailError of int * Pp.std_ppcmds
 
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
@@ -131,7 +134,7 @@ 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 tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
@@ -199,11 +202,5 @@ val change_constraints_pftreestate
 (*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
+val set_info_printer :
+  (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index cd8d34db..aff6b944 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacexpr.ml,v 1.33.2.3 2005/05/15 12:47:04 herbelin Exp $ i*)
+(*i $Id: tacexpr.ml 8651 2006-03-21 21:54:43Z jforest $ i*)
 
 open Names
 open Topconstr
@@ -20,6 +20,7 @@ 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 lazy_flag = bool      (* true = lazy             false = eager *)
 
 type raw_red_flag =
   | FBeta
@@ -55,8 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *)
   | InHypTypeOnly
   | InHypValueOnly
 
-type 'a raw_hyp_location = 
-    'a * int list * (hyp_location_flag * hyp_location_flag option ref)
+type 'a raw_hyp_location = 'a * int list * hyp_location_flag
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
@@ -69,12 +69,17 @@ type inversion_kind =
   | 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
+  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr
+  | DepInversion of inversion_kind * 'c option * intro_pattern_expr
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
 
+type 'id message_token =
+  | MsgString of string
+  | MsgInt of int
+  | MsgIdent of 'id
+
 type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
@@ -84,6 +89,8 @@ type 'id gclause =
     onconcl : bool;
     concl_occs :int list }
 
+let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
+
 let simple_clause_of = function
     { onhyps = Some[scl]; onconcl = false } -> Some scl
   | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
@@ -112,6 +119,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacIntroMove of identifier option * identifier located option
   | TacAssumption
   | TacExact of 'constr
+  | TacExactNoCheck of 'constr
   | TacApply of 'constr with_bindings
   | TacElim of 'constr with_bindings * 'constr with_bindings option
   | TacElimType of 'constr
@@ -122,20 +130,19 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCofix of identifier option
   | TacMutualCofix of identifier * (identifier * 'constr) list
   | TacCut of 'constr
-  | TacTrueCut of name * 'constr 
-  | TacForward of bool * name * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause
-  | TacInstantiate of int * 'constr * 'id gclause
+(*  | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location) *)
 
   (* 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)
+  | TacSimpleInduction of quantified_hypothesis
+  | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option
+      * intro_pattern_expr
   | 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)
+  | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option
+      * intro_pattern_expr
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
@@ -145,8 +152,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacLApply of 'constr
 
   (* Automation tactics *)
-  | TacTrivial of string list option
-  | TacAuto of int or_var option * string list option
+  | TacTrivial of 'constr list * string list option
+  | TacAuto of int or_var option * 'constr list * string list option
   | TacAutoTDB of int option
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
@@ -154,7 +161,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacDAuto of int or_var option * int option
 
   (* Context management *)
-  | TacClear of 'id list
+  | TacClear of bool * 'id list
   | TacClearBody of 'id list
   | TacMove of bool * 'id * 'id
   | TacRename of 'id * 'id
@@ -185,13 +192,14 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* For syntax extensions *)
   | TacAlias of loc * string *
       (identifier * ('constr,'tac) generic_argument) list
-      * (dir_path * 'tac)
+      * (dir_path * glob_tactic_expr)
 
 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
+  | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | 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
@@ -199,14 +207,13 @@ and ('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
+  | TacId of 'id message_token list
+  | TacFail of int or_var * 'id message_token list
   | 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
+  | TacMatch of lazy_flag * ('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 lazy_flag * 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
 
@@ -224,9 +231,21 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | Integer        of int
   | TacCall        of loc *
       'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
+  | TacExternal of loc * string * string * 
+      ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
   | TacFreshId     of string option
   | Tacexp of 'tac
 
+(* Globalized tactics *)
+and 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 raw_tactic_expr =
     (constr_expr,
      pattern_expr,
@@ -259,16 +278,6 @@ type raw_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,
@@ -283,8 +292,8 @@ type glob_tactic_arg =
      constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
-     ltac_constant located,
-     identifier located or_var,
+     ltac_constant located or_var,
+     identifier located,
      glob_tactic_expr) gen_tactic_arg
 
 type glob_generic_argument =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0e3a49b0..b426f75d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml,v 1.61.2.1 2004/07/16 19:30:50 herbelin Exp $ *)
+(* $Id: tacmach.ml 7682 2005-12-21 15:06:11Z herbelin $ *)
 
 open Util
 open Names
@@ -14,11 +14,11 @@ open Nameops
 open Sign
 open Term
 open Termops
-open Instantiate
 open Environ
 open Reductionops
 open Evd
 open Typing
+open Redexpr
 open Tacred
 open Proof_trees
 open Proof_type
@@ -32,7 +32,7 @@ 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 'a sigma   = 'a Evd.sigma;;
 type validation = Proof_type.validation;;
 type tactic     = Proof_type.tactic;;
 
@@ -40,10 +40,10 @@ 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 sig_it   = Refiner.sig_it
+let project  = Refiner.project
+let pf_env   = Refiner.pf_env
+let pf_hyps  = Refiner.pf_hyps
 
 let pf_concl gls = (sig_it gls).evar_concl
 let pf_hyps_types gls  =
@@ -79,10 +79,6 @@ 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
@@ -91,12 +87,8 @@ 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_reduction_of_red_expr gls re c = 
+  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c 
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
@@ -119,7 +111,8 @@ 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)))
+let pf_check_type gls c1 c2 = 
+  ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
 
 (************************************)
 (* Tactics handling a list of goals *)
@@ -194,8 +187,8 @@ let internal_cut_rev_no_check 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_concl_no_check c sty gl = 
+  refiner (Prim (Convert_concl (c,sty))) gl
 
 let convert_hyp_no_check d gl =
   refiner (Prim (Convert_hyp d)) gl
@@ -221,9 +214,11 @@ 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
+  let { evar_hyps = sign; evar_concl = cl } = sig_it gls in 
+  let ids = ids_of_named_context (named_context_of_val sign) in
+  convert_concl_no_check 
+    (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls 
+
 
 
 (* Versions with consistency checks *)
@@ -233,7 +228,7 @@ 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_concl d sty = with_check (convert_concl_no_check d sty)
 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)
@@ -243,7 +238,6 @@ let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
 (* Pretty-printers *)
 
 open Pp
-open Printer
 open Tacexpr
 open Rawterm
 
@@ -252,9 +246,9 @@ let rec pr_list f = function
   | 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))
+  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (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))
+  hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
+         prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
   
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 2990567e..9352cb5d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacmach.mli,v 1.50.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
+(*i $Id: tacmach.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
 
 (*i*)
 open Names
@@ -18,14 +18,14 @@ open Reduction
 open Proof_trees
 open Proof_type
 open Refiner
-open Tacred
+open Redexpr
 open Tacexpr
 open Rawterm
 (*i*)
 
 (* Operations for handling terms under a local typing context. *)
 
-type 'a sigma   = 'a Proof_type.sigma;;
+type 'a sigma   = 'a Evd.sigma;;
 type validation = Proof_type.validation;;
 type tactic     = Proof_type.tactic;;
 
@@ -51,7 +51,6 @@ 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
@@ -63,7 +62,7 @@ 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_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -120,9 +119,6 @@ val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   evar_map -> pftreestate -> pftreestate
 
-(*i
-val vernac_tactic : string * tactic_arg list -> tactic
-i*)
 (*s The most primitive tactics. *)
 
 val refiner                   : rule -> tactic
@@ -131,7 +127,7 @@ 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_concl_no_check    : types -> cast_kind -> tactic
 val convert_hyp_no_check      : named_declaration -> tactic
 val thin_no_check             : identifier list -> tactic
 val thin_body_no_check        : identifier list -> tactic
@@ -149,10 +145,7 @@ 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_concl    : types -> cast_kind -> tactic
 val convert_hyp      : named_declaration -> tactic
 val thin             : identifier list -> tactic
 val thin_body        : identifier list -> tactic
@@ -173,11 +166,6 @@ 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
+(*s Pretty-printing functions (debug only). *)
+val pr_gls    : goal sigma -> Pp.std_ppcmds
+val pr_glls   : goal list sigma -> Pp.std_ppcmds
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1fa1101d..43807872 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,17 +6,18 @@
 (*         *       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
+let prtac = ref (fun _ -> assert false)
+let set_tactic_printer f = prtac := f
+let prmatchpatt = ref (fun _ _ -> assert false)
+let set_match_pattern_printer f = prmatchpatt := f
+let prmatchrl = ref (fun _ -> assert false)
+let set_match_rule_printer f = prmatchrl := f
 
 (* 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
@@ -32,7 +33,7 @@ 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))
+  msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
 
 (* Prints the commands *)
 let help () =
@@ -46,7 +47,7 @@ let help () =
 let goal_com g tac =
   begin
     db_pr_goal g;
-    msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ())
+    msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
   end
 
 (* Gives the number of a run command *)
@@ -107,15 +108,14 @@ let debug_prompt lev g tac f =
 (* Prints a constr *)
 let db_constr debug env c =
   if debug <> DebugOff & !skip = 0 then
-    msgnl (str "Evaluated term: " ++ prterm_env env c)
+    msgnl (str "Evaluated term: " ++ print_constr_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)
+    msgnl (str "|" ++ spc () ++ !prmatchrl r)
   end
 
 (* Prints the hypothesis pattern identifier if it exists *)
@@ -128,12 +128,12 @@ 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)
+                " has been matched: ") ++ print_constr_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)
+    msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
 
 (* Prints a success message when the goal has been matched *)
 let db_mc_pattern_success debug =
@@ -142,18 +142,16 @@ let db_mc_pattern_success debug =
            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)
+  | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
   | Subterm (o,c) ->
-    Subterm (o,(extern_pattern env (names_of_rel_context env) c))
+    Subterm (o,(extern_constr_pattern (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)
+           !prmatchpatt env hyp)
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
@@ -164,10 +162,10 @@ let db_matching_failure debug =
 (* 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
+    let s = str "message \"" ++ s ++ str "\"" in
     msgnl 
       (str "This rule has failed due to \"Fail\" tactic (" ++
-       str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
+       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 =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 9ab263c4..fc1b6120 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,10 +6,11 @@
 (*         *       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*)
+(*i $Id: tactic_debug.mli 7911 2006-01-21 11:18:36Z herbelin $ i*)
 
 open Environ
 open Pattern
+open Evd
 open Proof_type
 open Names
 open Tacexpr
@@ -19,6 +20,13 @@ open Term
    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 *)
 
+val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
+val set_match_pattern_printer :
+  (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
+val set_match_rule_printer :
+  ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+    unit
+
 (* Debug information *)
 type debug_info =
   | DebugOn of int
@@ -53,7 +61,7 @@ val db_hyp_pattern_failure :
 val db_matching_failure : debug_info -> unit
 
 (* Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> string -> unit
+val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
 
 (* An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref