petits changements cosmetiques sur les tactiques

+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses
definies


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

27 files changed, 666 insertions, 722 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 102135e96..f6a47f986 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -465,7 +465,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	(List.map 
 	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
 		(tclTHEN 
-		   (clear_one id)
+		   (clear [id])
 		   (free_try (search_gen decomp p db_list local_db []))))
 	   (pf_ids_of_hyps goal)) 
   in
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index 7b6303130..b794b2893 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -5,16 +5,16 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A module to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 06/12/2000                                 *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                              PROJECT HELM                                 *)
+(*                                                                           *)
+(*                    A module to print Coq objects in XML                   *)
+(*                                                                           *)
+(*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                06/12/2000                                 *)
+(*                                                                           *)
+(*****************************************************************************)
 
 
 (* CONFIGURATION PARAMETERS *)
@@ -195,11 +195,11 @@ let add_to_pvars x =
    match x with
       Definition (v, bod, typ) ->
        cumenv :=
-         E.push_named_decl (Names.id_of_string v, Some bod, typ) !cumenv ;
+         E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ;
        v
     | Assumption (v, typ) ->
        cumenv :=
-         E.push_named_decl (Names.id_of_string v, None, typ) !cumenv ;
+         E.push_named (Names.id_of_string v, None, typ) !cumenv ;
        v
   in
    match !pvars with
diff --git a/dev/base_include b/dev/base_include
index 969db5581..a9d8d7812 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -2,6 +2,7 @@
 (* File to include to get some Coq facilities under the ocaml toplevel.
    This file is loaded by include *)
 
+#cd".";;
 #use "top_printers.ml";;
 
 #install_printer  (* identifier *) prid;;
diff --git a/dev/include b/dev/include
index 8fa4ba374..165853221 100644
--- a/dev/include
+++ b/dev/include
@@ -1,6 +1,7 @@
 
 (* File to include to install the pretty-printers in the ocaml toplevel *)
 
+#cd ".";;
 #use "base_include";;
 
 #install_printer  (* ast *)  prast;;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 94303bada..2cff2f716 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -49,84 +49,82 @@ let universes env = env.env_universes
 let named_context env = env.env_named_context
 let rel_context env = env.env_rel_context
 
-(* Access functions. *)
-
+(* Rel context *)
 let lookup_rel n env =
   Sign.lookup_rel n env.env_rel_context
 
-let lookup_named id env =
-  Sign.lookup_named id env.env_named_context
-
-let lookup_constant sp env =
-  Spmap.find sp env.env_globals.env_constants
-
-let lookup_mind sp env =
-  Spmap.find sp env.env_globals.env_inductives
-
-(* Construction functions. *)
+let evaluable_rel n env =
+  try
+    match lookup_rel n env with
+        (_,Some _,_) -> true
+      | _ -> false
+  with Not_found -> 
+    false
 
-(* Rel context *)
 let rel_context_app f env =
   { env with
       env_rel_context = f env.env_rel_context }
 
-let reset_context env =
-  { env with
-      env_named_context = empty_named_context;
-      env_rel_context = empty_rel_context }
-
-let reset_with_named_context ctxt env =
-  { env with
-      env_named_context = ctxt;
-      env_rel_context = empty_rel_context }
+let push_rel d   = rel_context_app (add_rel_decl d)
+let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
+let push_rec_types (lna,typarray,_) env =
+  let ctxt =
+    array_map2_i
+      (fun i na t -> (na, None, type_app (lift i) t)) lna typarray in
+  Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 let reset_rel_context env =
   { env with
       env_rel_context = empty_rel_context }
 
-let push_rel d   = rel_context_app (add_rel_decl d)
-let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
-let push_rel_assum (id,ty) = push_rel (id,None,ty)
-
-let push_rec_types (lna,typarray,_) env =
-  let ctxt =
-    array_map2_i (fun i na t -> (na, type_app (lift i) t)) lna typarray in
-  Array.fold_left
-    (fun e assum -> push_rel_assum assum e) env ctxt
-
 let fold_rel_context f env ~init =
-  snd (fold_rel_context
+  snd (Sign.fold_rel_context
 	 (fun d (env,e) -> (push_rel d env, f env d e))
          (rel_context env) ~init:(reset_rel_context env,init))
 
+
 (* Named context *)
+let lookup_named id env =
+  Sign.lookup_named id env.env_named_context
+
+(* A local const is evaluable if it is defined and not opaque *)
+let evaluable_named id env =
+  try 
+    match lookup_named id env with
+        (_,Some _,_) -> true
+      | _ -> false
+  with Not_found -> 
+    false
+
 let named_context_app f env =
   { env with
       env_named_context = f env.env_named_context }
 
-let push_named_decl d   = named_context_app (add_named_decl d)
-let push_named_assum (id,ty) = push_named_decl (id,None,ty)
-let pop_named_decl id         = named_context_app (pop_named_decl id)
+let push_named d   = named_context_app (Sign.add_named_decl d)
+let pop_named id         = named_context_app (Sign.pop_named_decl id)
+
+let reset_context env =
+  { env with
+      env_named_context = empty_named_context;
+      env_rel_context = empty_rel_context }
+
+let reset_with_named_context ctxt env =
+  { env with
+      env_named_context = ctxt;
+      env_rel_context = empty_rel_context }
 
 let fold_named_context f env ~init =
   snd (Sign.fold_named_context
-	 (fun d (env,e) -> (push_named_decl d env, f env d e))
+	 (fun d (env,e) -> (push_named d env, f env d e))
          (named_context env) ~init:(reset_context env,init))
 
 let fold_named_context_reverse f ~init env =
   Sign.fold_named_context_reverse f ~init:init (named_context env) 
 
-(* Universe constraints *)
-let set_universes g env =
-  if env.env_universes == g then env else { env with env_universes = g }
-
-let add_constraints c env =
-  if c == Constraint.empty then 
-    env 
-  else 
-    { env with env_universes = merge_constraints c env.env_universes }
-
 (* Global constants *)
+let lookup_constant sp env =
+  Spmap.find sp env.env_globals.env_constants
+
 let add_constant sp cb env =
   let _ =
     try
@@ -140,7 +138,35 @@ let add_constant sp cb env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
+(* constant_type gives the type of a constant *)
+let constant_type env sp =
+  let cb = lookup_constant sp env in
+  cb.const_type  
+
+type const_evaluation_result = NoBody | Opaque
+
+exception NotEvaluableConst of const_evaluation_result
+
+let constant_value env sp =
+  let cb = lookup_constant sp env in
+  if cb.const_opaque then raise (NotEvaluableConst Opaque);
+  match cb.const_body with
+    | Some body -> body
+    | None -> raise (NotEvaluableConst NoBody)
+
+let constant_opt_value env cst =
+  try Some (constant_value env cst)
+  with NotEvaluableConst _ -> None
+
+(* A global const is evaluable if it is defined and not opaque *)
+let evaluable_constant cst env =
+  try let _  = constant_value env cst in true
+  with Not_found | NotEvaluableConst _ -> false
+
 (* Mutual Inductives *)
+let lookup_mind sp env =
+  Spmap.find sp env.env_globals.env_inductives
+
 let add_mind sp mib env =
   let _ =
     try 
@@ -154,6 +180,16 @@ let add_mind sp mib env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
+(* Universe constraints *)
+let set_universes g env =
+  if env.env_universes == g then env else { env with env_universes = g }
+
+let add_constraints c env =
+  if c == Constraint.empty then 
+    env 
+  else 
+    { env with env_universes = merge_constraints c env.env_universes }
+
 (* Lookup of section variables *)
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
@@ -219,50 +255,6 @@ let keep_hyps env needed =
 
 (* Constants *)
 
-let opaque_constant env sp = (lookup_constant sp env).const_opaque
-
-(* constant_type gives the type of a constant *)
-let constant_type env sp =
-  let cb = lookup_constant sp env in
-  cb.const_type  
-
-type const_evaluation_result = NoBody | Opaque
-
-exception NotEvaluableConst of const_evaluation_result
-
-let constant_value env sp =
-  let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque);
-  match cb.const_body with
-    | Some body -> body
-    | None -> raise (NotEvaluableConst NoBody)
-
-let constant_opt_value env cst =
-  try Some (constant_value env cst)
-  with NotEvaluableConst _ -> None
-
-(* A global const is evaluable if it is defined and not opaque *)
-let evaluable_constant env cst =
-  try let _  = constant_value env cst in true
-  with Not_found | NotEvaluableConst _ -> false
-
-(* A local const is evaluable if it is defined and not opaque *)
-let evaluable_named_decl env id =
-  try 
-    match lookup_named id env with
-        (_,Some _,_) -> true
-      | _ -> false
-  with Not_found -> 
-    false
-
-let evaluable_rel_decl env n =
-  try
-    match lookup_rel n env with
-        (_,Some _,_) -> true
-      | _ -> false
-  with Not_found -> 
-    false
-
 (*s Modules (i.e. compiled environments). *)
 
 type compiled_env = {
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ecaa4d108..a7670f46e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -12,7 +12,6 @@
 open Names
 open Term
 open Declarations
-open Univ
 open Sign
 (*i*)
 
@@ -21,29 +20,45 @@ open Sign
    informations added in environments, and that is why we speak here
    of ``unsafe'' environments. *)
 
+(* Environments have the following components:
+   - a context for de Bruijn variables
+   - a context for section variables and goal assumptions
+   - a context for global constants and axioms
+   - a context for inductive definitions
+   - a set of universe constraints *)
+
 type env
 
 val empty_env : env
 
-val universes : env -> universes
-val rel_context : env -> rel_context
+val universes     : env -> Univ.universes
+val rel_context   : env -> rel_context
 val named_context : env -> named_context
 
-(* This forgets named and rel contexts *)
-val reset_context : env -> env
-(* This forgets rel context and sets a new named context *)
-val reset_with_named_context : named_context -> env -> env
+(***********************************************************************)
+(*s Context of de Bruijn variables (rel_context) *)
+val push_rel         : rel_declaration -> env -> env
+val push_rel_context :     rel_context -> env -> env
+val push_rec_types   : rec_declaration -> env -> env
 
-(*s This concerns only local vars referred by names [named_context] *)
-val push_named_decl : named_declaration -> env -> env
-val pop_named_decl : identifier -> env -> env
+(* Looks up in the context of local vars referred by indice ([rel_context]) *)
+(* raises [Not_found] if the index points out of the context *)
+val lookup_rel    : int -> env -> rel_declaration
+val evaluable_rel : int -> env -> bool
 
-(*s This concerns only local vars referred by indice [rel_context] *)
-val push_rel : rel_declaration -> env -> env
-val push_rel_context : rel_context -> env -> env
+(*s Recurrence on [rel_context] *)
+val fold_rel_context :
+  (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-(*s Push the types of a (co-)fixpoint to [rel_context] *)
-val push_rec_types : rec_declaration -> env -> env
+(***********************************************************************)
+(* Context of variables (section variables and goal assumptions) *)
+val push_named : named_declaration -> env -> env
+val pop_named  : identifier -> env -> env
+
+(* Looks up in the context of local vars referred by names ([named_context]) *)
+(* raises [Not_found] if the identifier is not found *)
+val lookup_named    : variable -> env -> named_declaration
+val evaluable_named : variable -> env -> bool
 
 (*s Recurrence on [named_context]: older declarations processed first *)
 val fold_named_context :
@@ -53,37 +68,20 @@ val fold_named_context :
 val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
 
-(*s Recurrence on [rel_context] *)
-val fold_rel_context :
-  (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
-
-(*s add entries to environment *)
-val set_universes : universes -> env -> env
-val add_constraints : constraints -> env -> env
-val add_constant : 
-  constant -> constant_body -> env -> env
-val add_mind : 
-  section_path -> mutual_inductive_body -> env -> env
-
-(*s Lookups in environment *)
-
-(* Looks up in the context of local vars referred by indice ([rel_context]) *)
-(* raises [Not_found] if the index points out of the context *)
-val lookup_rel : int -> env -> rel_declaration
-
-val evaluable_rel_decl : env -> int -> bool
-
-(* Looks up in the context of local vars referred by names ([named_context]) *)
-(* raises [Not_found] if the identifier is not found *)
-val lookup_named : variable -> env -> named_declaration
+(* This forgets named and rel contexts *)
+val reset_context : env -> env
+(* This forgets rel context and sets a new named context *)
+val reset_with_named_context : named_context -> env -> env
 
-val evaluable_named_decl : env -> variable -> bool
+(***********************************************************************)
+(*s Global constants *)
+(*s Add entries to global environment *)
+val add_constant : constant -> constant_body -> env -> env
 
 (* Looks up in the context of global constant names *)
 (* raises [Not_found] if the required path is not found *)
-val lookup_constant : constant -> env -> constant_body
-
-val evaluable_constant : env -> constant -> bool
+val lookup_constant    : constant -> env -> constant_body
+val evaluable_constant : constant -> env -> bool
 
 (*s [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
@@ -91,23 +89,34 @@ val evaluable_constant : env -> constant -> bool
 type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 
-val constant_value : env -> constant -> constr
-val constant_type : env -> constant -> types
+val constant_value     : env -> constant -> constr
+val constant_type      : env -> constant -> types
 val constant_opt_value : env -> constant -> constr option
 
+(***********************************************************************)
+(*s Inductive types *)
+val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
+
 (* Looks up in the context of global inductive names *)
 (* raises [Not_found] if the required path is not found *)
-val lookup_mind : section_path -> env -> mutual_inductive_body
+val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
+(***********************************************************************)
+(*s Universe constraints *)
+val set_universes   :   Univ.universes -> env -> env
+val add_constraints : Univ.constraints -> env -> env
 
-(* [global_vars_set c] returns the list of [id]'s occurring as [VAR
-    id] in [c] *)
+(***********************************************************************)
+(* Sets of referred section variables *)
+(* [global_vars_set env c] returns the list of [id]'s occurring as
+   [VAR id] in [c] *)
 val global_vars_set : env -> constr -> Idset.t
 (* the constr must be an atomic construction *)
 val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
 
+(***********************************************************************)
 (*s Modules. *)
 
 type compiled_env
@@ -115,12 +124,13 @@ type compiled_env
 val export : env -> dir_path -> compiled_env
 val import : compiled_env -> env -> env
 
+(***********************************************************************)
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
   type. *)
 
 type unsafe_judgment = { 
-  uj_val : constr;
+  uj_val  : constr;
   uj_type : types }
 
 val make_judge : constr -> types -> unsafe_judgment
@@ -128,5 +138,11 @@ val j_val  : unsafe_judgment -> constr
 val j_type : unsafe_judgment -> types
 
 type unsafe_type_judgment = { 
-  utj_val : constr;
+  utj_val  : constr;
   utj_type : sorts }
+
+
+
+
+
+
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d98adbb37..16ff717e9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -572,7 +572,7 @@ let check_one_fix renv recpos def =
       | Const sp as c -> 
           (try List.for_all (check_rec_call renv) l
            with (FixGuardError _ ) as e ->
-             if evaluable_constant renv.env sp then 
+             if evaluable_constant sp renv.env then 
 	       check_rec_call renv
                  (applist(constant_value renv.env sp, l))
 	     else raise e)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f96ff1fd9..f284d774d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -54,7 +54,7 @@ let push_rel_or_named_def push (id,b,topt) env =
   let env'' = push (id,Some j.uj_val,typ) env' in
   (cst,env'')
 
-let push_named_def = push_rel_or_named_def push_named_decl
+let push_named_def = push_rel_or_named_def push_named
 let push_rel_def = push_rel_or_named_def push_rel
 
 let push_rel_or_named_assum push (id,t) env =
@@ -64,7 +64,7 @@ let push_rel_or_named_assum push (id,t) env =
   let env'' = push (id,None,t) env' in
   (cst,env'')
 
-let push_named_assum = push_rel_or_named_assum push_named_decl
+let push_named_assum = push_rel_or_named_assum push_named
 let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env)
 
 let push_rels_with_univ vars env =
@@ -126,7 +126,7 @@ let add_constraints = Environ.add_constraints
 let rec pop_named_decls idl env =
   match idl with 
     | [] -> env
-    | id::l -> pop_named_decls l (Environ.pop_named_decl id env)
+    | id::l -> pop_named_decls l (Environ.pop_named id env)
 
 let export = export
 let import = import
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a53ecf535..c556f998e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -160,7 +160,7 @@ let split_evar_to_arrow sigma (ev,args) =
   let (sigma1,dom) = new_type_var evenv sigma in
   let hyps = evd.evar_hyps in
   let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
-  let newenv = push_named_decl (nvar, None, dom) evenv in
+  let newenv = push_named (nvar, None, dom) evenv in
   let (sigma2,rng) = new_type_var newenv sigma1 in
   let x = named_hd newenv dom Anonymous in
   let prod = mkProd (x, dom, subst_var nvar rng) in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 151525c31..ad7e02b77 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -749,7 +749,7 @@ let abstract_scheme env (locc,a,ta) t =
   if occur_meta a then 
     mkLambda (na,ta,t)
   else 
-    mkLambda (na, ta,subst_term_occ locc a t)
+    mkLambda (na, ta,subst_term_occ env locc a t)
 
 
 let pattern_occs loccs_trm_typ env sigma c =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 8958d1f58..867bbf50f 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -13,9 +13,9 @@ open Util
 open Names
 open Nameops
 open Term
+open Sign
 open Environ
 open Nametab
-open Sign
 
 let print_sort = function
   | Prop Pos -> (str "Set")
@@ -86,7 +86,7 @@ let push_named_rec_types (lna,typarray,_) env =
 	   | Anonymous -> anomaly "Fix declarations must be named")
       lna typarray in
   Array.fold_left
-    (fun e assum -> push_named_decl assum e) env ctxt
+    (fun e assum -> push_named assum e) env ctxt
 
 let rec lookup_rel_id id sign = 
   let rec lookrec = function
@@ -335,25 +335,34 @@ let dependent m t =
 (*  substitution functions *)                         
 (***************************)
 
+let rec subst_meta bl c = 
+  match kind_of_term c with
+    | Meta i -> (try List.assoc i bl with Not_found -> c)
+    | _ -> map_constr (subst_meta bl) c
+
 (* Equality modulo let reduction *)
-let rec whd_rel hyps c =
+let rec whd_locals env c =
   match kind_of_term c with
       Rel i ->
         (try
-          (match Sign.lookup_rel i hyps with
-              (_,Some v,_) -> whd_rel hyps (lift i v)
+          (match lookup_rel i env with
+              (_,Some v,_) -> whd_locals env (lift i v)
+            | _ -> c)
+         with Not_found -> c)
+    | Var id ->
+        (try
+          (match lookup_named id env with
+              (_,Some v,_) -> whd_locals env v
             | _ -> c)
          with Not_found -> c)
     | _ -> c
 
 (* Expand de Bruijn indices bound to a value *)
-let rec nf_rel hyps c =
-  map_constr_with_full_binders Sign.add_rel_decl nf_rel hyps (whd_rel hyps c)
+let rec nf_locals env c =
+  map_constr_with_full_binders push_rel nf_locals env (whd_locals env c)
 
-(* [m] is not evaluated because it is called only with terms for [m] which
-   have been lifted of the length of [hyps], hence [nf_rel] would have no
-   effect. *)
-let compare_zeta hyps m n = zeta_eq_constr m (nf_rel hyps n)
+(* compare terms modulo expansion of let and local variables *)
+let compare_zeta env m n = zeta_eq_constr m (nf_locals env n)
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
@@ -388,7 +397,7 @@ let my_prefix_application eq_fun (e,k,c) (by_c : constr) (t : constr) =
    term [c] in a term [t] *)
 (*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
 
-let subst_term_gen eq_fun c t = 
+let subst_term_gen eq_fun env c t = 
   let rec substrec (e,k,c as kc) t =
     match prefix_application eq_fun kc t with
       | Some x -> x
@@ -396,43 +405,38 @@ let subst_term_gen eq_fun c t =
     (if eq_fun e c t then mkRel k
      else
        map_constr_with_full_binders
-         (fun d (e,k,c) -> (Sign.add_rel_decl d e,k+1,lift 1 c))
+         (fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c))
          substrec kc t)
   in 
-  substrec (empty_rel_context,1,c) t
+  substrec (env,1,nf_locals env c) t
 
 (* Recognizing occurrences of a given (closed) subterm in a term :
    [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed)
    term [c1] in a term [t] *)
 (*i Meme remarque : a priori [c] n'est pas forcement clos i*)
 
-let replace_term_gen eq_fun c by_c in_t = 
+let replace_term_gen eq_fun env c by_c in_t = 
   let rec substrec (e,k,c as kc) t =
     match my_prefix_application eq_fun kc by_c t with
       | Some x -> x
       | None ->
     (if eq_fun e c t then (lift k by_c) else
       map_constr_with_full_binders
-	(fun d (e,k,c) -> (Sign.add_rel_decl d e,k+1,lift 1 c))
+	(fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c))
 	substrec kc t)
   in 
-  substrec (empty_rel_context,0,c) in_t
+  substrec (env,0,nf_locals env c) in_t
 
-let subst_term = subst_term_gen (fun _ -> eq_constr)
+let subst_term = subst_term_gen (fun _ -> eq_constr) empty_env
 
-let replace_term = replace_term_gen (fun _ -> eq_constr)
-
-let rec subst_meta bl c = 
-  match kind_of_term c with
-    | Meta i -> (try List.assoc i bl with Not_found -> c)
-    | _ -> map_constr (subst_meta bl) c
+let replace_term = replace_term_gen (fun _ -> eq_constr) empty_env
 
 (* Substitute only a list of locations locs, the empty list is
    interpreted as substitute all, if 0 is in the list then no
    substitution is done. The list may contain only negative occurrences
    that will not be substituted. *)
 
-let subst_term_occ_gen locs occ c t =
+let subst_term_occ_gen env locs occ c t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
   let check = ref true in
@@ -452,34 +456,34 @@ let subst_term_occ_gen locs occ c t =
       in incr pos; r
     else
       map_constr_with_binders_left_to_right
-	(fun d (e,k,c) -> (Sign.add_rel_decl d e,k+1,lift 1 c))
+	(fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c))
         substrec kc t
   in
-  let t' = substrec (empty_rel_context,1,c) t in
+  let t' = substrec (env,1,nf_locals env c) t in
   (!pos, t')
 
-let subst_term_occ locs c t = 
+let subst_term_occ env locs c t = 
   if locs = [] then
-    subst_term_gen compare_zeta c t
+    subst_term_gen compare_zeta env c t
   else if List.mem 0 locs then 
     t
   else 
-    let (nbocc,t') = subst_term_occ_gen locs 1 c t in
+    let (nbocc,t') = subst_term_occ_gen env locs 1 c t in
     if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
       errorlabstrm "subst_term_occ" (str "Too few occurences");
     t'
 
-let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
+let subst_term_occ_decl env locs c (id,bodyopt,typ as d) =
   match bodyopt with
-    | None -> (id,None,subst_term_occ locs c typ)
+    | None -> (id,None,subst_term_occ env locs c typ)
     | Some body -> 
 	if locs = [] then
 	  (id,Some (subst_term c body),type_app (subst_term c) typ)
 	else if List.mem 0 locs then 
 	  d
 	else 
-	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
-	  let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in
+	  let (nbocc,body') = subst_term_occ_gen env locs 1 c body in
+	  let (nbocc',t') = subst_term_occ_gen env locs nbocc c typ in
 	  if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
 	    errorlabstrm "subst_term_occ_decl" (str "Too few occurences");
 	  (id,Some body',t')
@@ -685,37 +689,6 @@ let eta_eq_constr =
   in aux
 
 
-(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name env l env_names n c =
-  if n = Anonymous & noccurn 1 c then
-    (None,l)
-  else
-    let fresh_id = next_name_not_occuring env n l env_names c in
-    let idopt = if noccurn 1 c then None else (Some fresh_id) in
-    (idopt, fresh_id::l)
-
-let concrete_let_name env l env_names n c =
-  let fresh_id = next_name_not_occuring env n l env_names c in
-  (Name fresh_id, fresh_id::l)
-
-let global_vars env ids = Idset.elements (global_vars_set env ids)
-
-let rec rename_bound_var env l c =
-  match kind_of_term c with
-  | Prod (Name s,c1,c2)  ->
-      if noccurn 1 c2 then
-        let env' = push_rel (Name s,None,c1) env in
-	mkProd (Name s, c1, rename_bound_var env' l c2)
-      else 
-        let s' = next_ident_away s (global_vars env c2@l) in
-        let env' = push_rel (Name s',None,c1) env in
-        mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
-  | Prod (Anonymous,c1,c2) ->
-        let env' = push_rel (Anonymous,None,c1) env in
-        mkProd (Anonymous, c1, rename_bound_var env' l c2)
-  | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
-  | x -> c
-
 (* iterator on rel context *)
 let process_rel_context f env =
   let sign = named_context env in
@@ -755,3 +728,40 @@ let make_all_name_different env =
        avoid := id::!avoid;
        push_rel (Name id,c,t) newenv)
     env
+
+let global_vars env ids = Idset.elements (global_vars_set env ids)
+
+let global_vars_set_of_decl env = function
+  | (_,None,t) -> global_vars_set env (body_of_type t)
+  | (_,Some c,t) ->
+      Idset.union (global_vars_set env (body_of_type t))
+        (global_vars_set env c)
+
+(* Remark: Anonymous var may be dependent in Evar's contexts *)
+let concrete_name env l env_names n c =
+  if n = Anonymous & noccurn 1 c then
+    (None,l)
+  else
+    let fresh_id = next_name_not_occuring env n l env_names c in
+    let idopt = if noccurn 1 c then None else (Some fresh_id) in
+    (idopt, fresh_id::l)
+
+let concrete_let_name env l env_names n c =
+  let fresh_id = next_name_not_occuring env n l env_names c in
+  (Name fresh_id, fresh_id::l)
+
+let rec rename_bound_var env l c =
+  match kind_of_term c with
+  | Prod (Name s,c1,c2)  ->
+      if noccurn 1 c2 then
+        let env' = push_rel (Name s,None,c1) env in
+	mkProd (Name s, c1, rename_bound_var env' l c2)
+      else 
+        let s' = next_ident_away s (global_vars env c2@l) in
+        let env' = push_rel (Name s',None,c1) env in
+        mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
+  | Prod (Anonymous,c1,c2) ->
+        let env' = push_rel (Anonymous,None,c1) env in
+        mkProd (Anonymous, c1, rename_bound_var env' l c2)
+  | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
+  | x -> c
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ae28029c5..1bb74a303 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -69,21 +69,28 @@ val occur_var_in_decl :
   identifier -> 'a * types option * types -> bool
 val free_rels : constr -> Intset.t
 
+(* Substitution of metavariables *)
+val subst_meta : (int * constr) list -> constr -> constr
+
+(* Expansion of local definitions *)
+val whd_locals : env -> constr -> constr
+val nf_locals  : env -> constr -> constr
+
 (* substitution of an arbitrary large term. Uses equality modulo
    reduction of let *)
 val dependent : constr -> constr -> bool
 val subst_term_gen :
-  (rel_context -> constr -> constr -> bool) -> constr -> constr -> constr
+  (env -> constr -> constr -> bool) -> env -> constr -> constr -> constr
 val replace_term_gen :
-  (rel_context -> constr -> constr -> bool) -> constr -> constr -> constr -> constr
+  (env -> constr -> constr -> bool) ->
+    env -> constr -> constr -> constr -> constr
 val subst_term : constr -> constr -> constr
 val replace_term : constr -> constr -> constr -> constr
-val subst_meta : (int * constr) list -> constr -> constr
 val subst_term_occ_gen :
-  int list -> int -> constr -> types -> int * types
-val subst_term_occ : int list -> constr -> types -> types
+  env -> int list -> int -> constr -> types -> int * types
+val subst_term_occ : env -> int list -> constr -> types -> types
 val subst_term_occ_decl :
-  int list -> constr -> named_declaration -> named_declaration
+  env -> int list -> constr -> named_declaration -> named_declaration
 
 (* Alternative term equalities *)
 val zeta_eq_constr : constr -> constr -> bool
@@ -136,7 +143,6 @@ val concrete_name :
 val concrete_let_name :
   env -> identifier list -> name list ->
   name -> constr -> name * identifier list
-val global_vars : env -> constr -> identifier list
 val rename_bound_var : env -> identifier list -> types -> types
 
 (* other signature iterators *)
@@ -144,7 +150,10 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val fold_named_context_both_sides :
-  ('a -> named_declaration -> named_context -> 'a) ->
+  ('a -> named_declaration -> named_declaration list -> 'a) ->
     named_context -> init:'a -> 'a
 val mem_named_context : identifier -> named_context -> bool
 val make_all_name_different : env -> env
+
+val global_vars : env -> constr -> identifier list
+val global_vars_set_of_decl : env -> named_declaration -> Idset.t
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index be9bd638a..3350b247b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -998,7 +998,7 @@ let abstract_scheme env c l lname_typ =
     (fun t (locc,a) (na,ta) ->
        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))
+       else lambda_name env (na,ta,subst_term_occ env locc a t))
     c
     (List.rev l)
     lname_typ
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 23b512bcb..85c0a0297 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -29,19 +29,7 @@ open Coqast
 open Declare
 open Retyping
 open Evarutil
-
-(* Will only be used on terms given to the Refine rule which have meta 
-variables only in Application and Case *)
-
-let collect_meta_variables c = 
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | Cast(c,_) -> collrec acc c
-    | (App _| Case _) -> fold_constr collrec acc c
-    | _ -> acc
-  in 
-  List.rev(collrec [] c)
-
+ 
 type refiner_error =
 
   (* Errors raised by the refiner *)
@@ -70,6 +58,8 @@ let catchable_exception = function
 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 true
 
 let without_check tac gl =
@@ -78,6 +68,223 @@ let without_check tac gl =
   let r = tac gl in
   check := c;
   r
+   
+(***********************************************************************)
+(***********************************************************************)
+(* Implementation of the structural rules (moving and deleting
+   hypotheses around) *)
+
+let check_clear_forward cleared_ids used_ids whatfor =
+  if !check && cleared_ids<>[] then
+    Idset.iter
+      (fun id' ->
+        if List.mem id' cleared_ids then
+          error (string_of_id id'^" is used in "^whatfor))
+      used_ids
+
+(* The Clear tactic: it scans the context for hypotheses to be removed
+   (instead of iterating on the list of identifier to be removed, which
+   forces the user to give them in order). *)
+let clear_hyps ids gl =
+  let env = Global.env() in
+  let (nhyps,subst,rmv) =
+    Sign.fold_named_context
+      (fun (id,c,ty as d) (hyps,subst,rmv) ->
+        if List.mem id ids then
+          match c with
+            | Some def -> (hyps,(id,def)::subst,rmv)
+            | None -> (hyps,subst,id::rmv)
+        else begin
+          let d' =
+            (id, option_app (replace_vars subst) c, replace_vars subst ty) in
+          check_clear_forward rmv (global_vars_set_of_decl env d')
+            ("hypothesis "^string_of_id id);
+          (add_named_decl d' hyps, subst, rmv)
+        end)
+      gl.evar_hyps
+      ~init:(empty_named_context,[],[]) in
+  let ncl = replace_vars subst gl.evar_concl in
+  check_clear_forward rmv (global_vars_set env ncl) "conclusion";
+  mk_goal nhyps ncl
+
+(* The ClearBody tactic *)
+
+(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
+   returns [tail::(f head (id,_,_) tail)] *)
+let apply_to_hyp sign id f =
+  let found = ref false in
+  let sign' =
+    fold_named_context_both_sides
+      (fun head (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f head d tail
+	 end else 
+	   add_named_decl d head)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign' else error "No such assumption"
+
+(* Same but with whole environment *)
+let apply_to_hyp2 env id f =
+  let found = ref false in
+  let env' =
+    fold_named_context_both_sides
+      (fun env (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f env d tail
+	 end else 
+	   push_named d env)
+      (named_context env) ~init:(reset_context env)
+  in
+  if (not !check) || !found then env' else error "No such assumption"
+
+let apply_to_hyp_and_dependent_on sign id f g =
+  let found = ref false in
+  let sign =
+    Sign.fold_named_context
+      (fun (idc,_,_ as d) oldest ->
+         if idc = id then (found := true; add_named_decl (f d) oldest)
+         else if !found then add_named_decl (g d) oldest
+         else add_named_decl d oldest)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign else error "No such assumption"
+
+let recheck_typability (what,id) env sigma t =
+  try let _ = type_of env sigma t in ()
+  with _ ->
+    let s = match what with
+      | None -> "the conclusion"
+      | Some id -> "hypothesis "^(string_of_id id) in
+    error
+      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
+  
+let remove_hyp_body env sigma id =
+  apply_to_hyp2 env id
+    (fun env (_,c,t) tail ->
+       match c with
+         | None -> error ((string_of_id id)^" is not a local definition")
+         | Some c ->
+             let env' = push_named (id,None,t) env in
+             if !check then 
+               ignore
+                 (Sign.fold_named_context 
+                    (fun (id',c,t as d) env'' ->
+                       (match c with
+                          | None -> 
+                              recheck_typability (Some id',id) env'' sigma t
+                          | Some b ->
+                              let b' = mkCast (b,t) in
+                              recheck_typability (Some id',id) env'' sigma b');
+                       push_named d env'')
+                    (List.rev tail) ~init:env');
+             env')
+
+
+(* Auxiliary functions for primitive MOVE tactic
+ *
+ * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves
+ * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the 
+ * left side [left] of the full signature if [toleft=true] or to the hyps 
+ * on the right side [right] if [toleft=false].
+ * If [with_dep] then dependent hypotheses are moved accordingly. *)
+
+let split_sign hfrom hto l =
+  let rec splitrec left toleft = function
+    | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom))
+    | (hyp,c,typ) as d :: right ->
+      	if hyp = hfrom then 
+	  (left,right,d,toleft) 
+      	else 
+	  splitrec (d::left) (toleft or (hyp = hto)) right
+  in 
+  splitrec [] false l
+
+let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
+  let env = Global.env() in
+  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
+    if toleft
+    then occur_var_in_decl env hyp2 d
+    else occur_var_in_decl env hyp d2
+  in
+  let rec moverec first middle = function
+    | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
+    | (hyp,_,_) as d :: right ->
+	let (first',middle') =
+      	  if List.exists (test_dep d) middle then 
+	    if with_dep & (hyp <> hto) then 
+	      (first, d::middle)
+            else 
+	      error 
+		("Cannot move "^(string_of_id idfrom)^" after "
+		 ^(string_of_id hto)
+		 ^(if toleft then ": it occurs in " else ": it depends on ")
+		 ^(string_of_id hyp))
+          else 
+	    (d::first, middle)
+	in
+      	if hyp = hto then 
+	  (List.rev first')@(List.rev middle')@right
+      	else 
+	  moverec first' middle' right
+  in
+  if toleft then 
+    List.rev_append (moverec [] [declfrom] left) right
+  else 
+    List.rev_append left (moverec [] [declfrom] right)
+
+let check_backward_dependencies sign d =
+  if not (Idset.for_all
+	    (fun id -> mem_named_context id sign)
+	    (global_vars_set_of_decl (Global.env()) d))
+  then
+    error "Can't introduce at that location: free variable conflict"
+
+
+let check_forward_dependencies id tail =
+  let env = Global.env() in
+  List.iter
+    (function (id',_,_ as decl) ->
+       if occur_var_in_decl env id decl then
+	 error ((string_of_id id) ^ " is used in hypothesis " 
+		^ (string_of_id id')))
+    tail
+
+
+let rename_hyp id1 id2 sign =
+  apply_to_hyp_and_dependent_on sign id1
+    (fun (_,b,t) -> (id2,b,t))
+    (map_named_declaration (replace_vars [id1,mkVar id2]))
+
+let replace_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign _ tail ->
+       if !check then
+	 (check_backward_dependencies sign d;
+	  check_forward_dependencies id tail);
+       add_named_decl d sign)
+
+let insert_after_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign d' _ ->
+       if !check then check_backward_dependencies sign d;
+       add_named_decl d (add_named_decl d' sign))
+
+(***********************************************************************)
+(***********************************************************************)
+(* Implementation of the logical rules *)
+
+(* Will only be used on terms given to the Refine rule which have meta 
+variables only in Application and Case *)
+
+let collect_meta_variables c = 
+  let rec collrec acc c = match kind_of_term c with
+    | Meta mv -> mv::acc
+    | Cast(c,_) -> collrec acc c
+    | (App _| Case _) -> fold_constr collrec acc c
+    | _ -> acc
+  in 
+  List.rev(collrec [] c)
 
 let conv_leq_goal env sigma arg ty conclty =
   if not (is_conv_leq env sigma ty conclty) then 
@@ -182,124 +389,6 @@ let error_use_instantiate () =
   errorlabstrm "Logic.prim_refiner"
     (str"cannot intro when there are open metavars in the domain type" ++
        spc () ++ str"- use Instantiate")
-    
-(* Auxiliary functions for primitive MOVE tactic
- *
- * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves
- * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the 
- * left side [left] of the full signature if [toleft=true] or to the hyps 
- * on the right side [right] if [toleft=false].
- * If [with_dep] then dependent hypotheses are moved accordingly. *)
-
-let split_sign hfrom hto l =
-  let rec splitrec left toleft = function
-    | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom))
-    | (hyp,c,typ) as d :: right ->
-      	if hyp = hfrom then 
-	  (left,right,d,toleft) 
-      	else 
-	  splitrec (d::left) (toleft or (hyp = hto)) right
-  in 
-  splitrec [] false l
-
-let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
-  let env = Global.env() in
-  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
-    if toleft
-    then occur_var_in_decl env hyp2 d
-    else occur_var_in_decl env hyp d2
-  in
-  let rec moverec first middle = function
-    | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
-    | (hyp,_,_) as d :: right ->
-	let (first',middle') =
-      	  if List.exists (test_dep d) middle then 
-	    if with_dep & (hyp <> hto) then 
-	      (first, d::middle)
-            else 
-	      error 
-		("Cannot move "^(string_of_id idfrom)^" after "
-		 ^(string_of_id hto)
-		 ^(if toleft then ": it occurs in " else ": it depends on ")
-		 ^(string_of_id hyp))
-          else 
-	    (d::first, middle)
-	in
-      	if hyp = hto then 
-	  (List.rev first')@(List.rev middle')@right
-      	else 
-	  moverec first' middle' right
-  in
-  if toleft then 
-    List.rev_append (moverec [] [declfrom] left) right
-  else 
-    List.rev_append left (moverec [] [declfrom] right)
-
-(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
-   returns [tail::(f head (id,_,_) tail)] *)
-let apply_to_hyp sign id f =
-  let found = ref false in
-  let sign' =
-    fold_named_context_both_sides
-      (fun head (idc,c,ct as d) tail ->
-	 if idc = id then begin
-	   found := true; f head d tail
-	 end else 
-	   add_named_decl d head)
-      sign ~init:empty_named_context
-  in
-  if (not !check) || !found then sign' else error "No such assumption"
-
-(* Same but with whole environment *)
-let apply_to_hyp2 env id f =
-  let found = ref false in
-  let env' =
-    fold_named_context_both_sides
-      (fun env (idc,c,ct as d) tail ->
-	 if idc = id then begin
-	   found := true; f env d tail
-	 end else 
-	   push_named_decl d env)
-      (named_context env) ~init:(reset_context env)
-  in
-  if (not !check) || !found then env' else error "No such assumption"
-
-exception Found of int
-
-let apply_to_hyp_and_dependent_on sign id f g =
-  let found = ref false in
-  let sign =
-    Sign.fold_named_context
-      (fun (idc,_,_ as d) oldest ->
-         if idc = id then (found := true; add_named_decl (f d) oldest)
-         else if !found then add_named_decl (g d) oldest
-         else add_named_decl d oldest)
-      sign ~init:empty_named_context
-  in
-  if (not !check) || !found then sign else error "No such assumption"
-
-let global_vars_set_of_var = function
-  | (_,None,t) -> global_vars_set (Global.env()) (body_of_type t)
-  | (_,Some c,t) ->
-      let env =Global.env() in
-      Idset.union (global_vars_set env (body_of_type t))
-        (global_vars_set env c)
-
-let check_backward_dependencies sign d =
-  if not (Idset.for_all
-	    (fun id -> mem_named_context id sign)
-	    (global_vars_set_of_var d))
-  then
-    error "Can't introduce at that location: free variable conflict"
-
-let check_forward_dependencies id tail =
-  let env = Global.env() in
-  List.iter
-    (function (id',_,_ as decl) ->
-       if occur_var_in_decl env id decl then
-	 error ((string_of_id id) ^ " is used in hypothesis " 
-		^ (string_of_id id')))
-    tail
 
 let convert_hyp sign sigma id b =
   apply_to_hyp sign id
@@ -334,61 +423,8 @@ let convert_def inbody sign sigma id c =
 	     add_named_decl (idc,Some b,t) sign)
 
 
-let rename_hyp id1 id2 sign =
-  apply_to_hyp_and_dependent_on sign id1
-    (fun (_,b,t) -> (id2,b,t))
-    (map_named_declaration (replace_vars [id1,mkVar id2]))
-
-let replace_hyp sign id d =
-  apply_to_hyp sign id
-    (fun sign _ tail ->
-       if !check then
-	 (check_backward_dependencies sign d;
-	  check_forward_dependencies id tail);
-       add_named_decl d sign)
-
-let insert_after_hyp sign id d =
-  apply_to_hyp sign id
-    (fun sign d' _ ->
-       if !check then check_backward_dependencies sign d;
-       add_named_decl d (add_named_decl d' sign))
-
-let remove_hyp env id =
-  apply_to_hyp env id
-    (fun env _ tail ->
-       if !check then check_forward_dependencies id tail;
-       env)
-
-let recheck_typability (what,id) env sigma t =
-  try let _ = type_of env sigma t in ()
-  with _ ->
-    let s = match what with
-      | None -> "the conclusion"
-      | Some id -> "hypothesis "^(string_of_id id) in
-    error
-      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
-  
-let remove_hyp_body env sigma id =
-  apply_to_hyp2 env id
-    (fun env (_,c,t) tail ->
-       match c with
-         | None -> error ((string_of_id id)^" is not a local definition")
-         | Some c ->
-             let env' = push_named_decl (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_decl d env'')
-                    tail ~init:env');
-             env')
-
+(***********************************************************************)
+(***********************************************************************)
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
@@ -396,6 +432,7 @@ let prim_refiner r sigma goal =
   let sign = goal.evar_hyps in
   let cl = goal.evar_concl in
   match r with
+    (* Logical rules *)
     | { name = Intro; newids = [id] } ->
     	if !check && mem_named_context id sign then
 	  error "New variable is already declared";
@@ -538,6 +575,7 @@ let prim_refiner r sigma goal =
 	let sgl = List.rev sgl in
 	sgl
 
+    (* Conversion rules *)
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sigma cl' in
 	if is_conv_leq env sigma cl' cl then
@@ -555,15 +593,8 @@ let prim_refiner r sigma goal =
     | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } ->
 	[mk_goal (convert_def false sign sigma id ty) cl]
 
-    | { name = Thin; hypspecs = ids } ->
-	let clear_aux sign id =
-          if !check && occur_var env id cl then
-            error ((string_of_id id) ^ " is used in the conclusion.");
-          remove_hyp sign id 
-	in
-	let sign' = List.fold_left clear_aux sign ids in
-     	let sg = mk_goal sign' cl in
-     	[sg]
+    (* And now the structural rules *)
+    | { name = Thin; hypspecs = ids } -> [clear_hyps ids goal]
 
     | { name = ThinBody; hypspecs = ids } ->
 	let clear_aux env id =
@@ -592,6 +623,10 @@ let prim_refiner r sigma goal =
 
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
+(***********************************************************************)
+(***********************************************************************)
+(* Extracting a proof term from the proof tree *)
+
 (* Util *)
 let rec rebind id1 id2 = function
   | [] -> []
@@ -666,7 +701,8 @@ let prim_extractor subfun vl pft =
 	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
 	let cc = subst_vars vl c in 
 	plain_instance metamap cc
-	  
+
+    (* Structural and conversion rules do not produce any proof *)
     | {ref=Some(Prim{name=Convert_concl;terms=[c]},[pf])} ->
 	subfun vl pf
 	
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9911e449f..674b090c3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -752,10 +752,10 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	(tclTRY_sign decomp_empty_term extra_sign)
 	::
 	(List.map 
-	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
-		(tclTHEN 
-		   (clear_one id)
-		   (search_gen decomp p db_list local_db [])))
+	   (fun id -> tclTHENSEQ
+               [decomp_unary_term (mkVar id);
+                clear [id];
+		search_gen decomp p db_list local_db []])
 	   (pf_ids_of_hyps goal)) 
   in
   let intro_tac = 
@@ -881,12 +881,9 @@ let compileAutoArg contac = function
            (List.map 
               (fun (id,_,typ) -> 
                 let cl = snd (decompose_prod (body_of_type typ)) in
-                 if (Hipattern.is_conjunction cl)
+                 if Hipattern.is_conjunction cl
 		 then 
-		   (tclTHEN
-                      (tclTHEN (simplest_elim (mkVar id)) 
-                         (clear_one id))
-                      contac) 
+		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] 
                  else 
 		   tclFAIL 0) ctx) g)
   | UsingTDB ->  
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ce26640c0..4008f10f7 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -71,7 +71,7 @@ and general_decompose recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
-	  tclTHEN (clear_one id)
+	  tclTHEN (clear [id])
 	    (tclMAP (general_decompose_on_hyp recognizer)
                (ids_of_named_context bas.assums))))
     id
@@ -86,10 +86,11 @@ let up_to_delta = ref false (* true *)
 let general_decompose recognizer c gl = 
   let typc = pf_type_of gl c in  
   (tclTHENS (cut typc) 
-     [(tclTHEN (intro_using tmphyp_name)
-         (onLastHyp
-	    (ifOnHyp recognizer (general_decompose recognizer) clear_one)));
-      (exact_no_check c)]) gl
+    [tclTHEN (intro_using tmphyp_name)
+      (onLastHyp
+	(ifOnHyp recognizer (general_decompose recognizer)
+          (fun id -> clear [id])));
+     exact_no_check c]) gl
 
 let head_in gls indl t =
   try
@@ -176,8 +177,9 @@ let induction_trailer abs_i abs_j bargs =
 	      ([],fvty) possible_bring_hyps
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
-	  (tclTHEN (tclTHEN (bring_hyps hyps) (clear_clauses ids))
-             (simple_elimination (mkVar id))) gls))
+	  (tclTHENSEQ
+            [bring_hyps hyps; clear ids; simple_elimination (mkVar id)])
+          gls))
 
 let double_ind abs_i abs_j gls =
   let cl = pf_concl gls in 
@@ -200,18 +202,17 @@ let _ = add_tactic "DoubleInd" dyn_double_ind
 (*****************************)
 
 let rec intro_pattern p = 
-  let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
-  and case_last  = (tclLAST_HYP h_simplest_case) in  
+  let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
+  and case_last  = tclLAST_HYP h_simplest_case in  
   match p with
-    | WildPat    -> (tclTHEN intro clear_last)
+    | WildPat    -> tclTHEN intro clear_last
     | IdPat  id  -> intro_mustbe_force id
-    | DisjPat l  -> (tclTHEN introf
+    | DisjPat l  -> tclTHEN introf
                        (tclTHENS 
 			  (tclTHEN case_last clear_last)
-			  (List.map intro_pattern l)))
-    | ConjPat l  -> (tclTHEN introf
-                       (tclTHEN (tclTHEN  case_last clear_last)
-                          (intros_pattern l)))
+			  (List.map intro_pattern l))
+    | ConjPat l  ->
+        tclTHENSEQ [introf; case_last; clear_last; intros_pattern l]
     | ListPat l  ->  intros_pattern l
 
 and intros_pattern l = tclMAP intro_pattern l
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d2d2dadd5..be301af0e 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -47,16 +47,17 @@ open Coqlib
    Eduardo Gimenez (30/3/98).
 *)
 
-let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
+let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
 
 let mkBranches = 
-        (tclTHEN  intro 
-        (tclTHEN (tclLAST_HYP h_simplest_elim)
-        (tclTHEN  clear_last
-        (tclTHEN  intros 
-        (tclTHEN (tclLAST_HYP h_simplest_case)
-        (tclTHEN  clear_last
-                  intros))))))
+  tclTHENSEQ
+    [intro; 
+     tclLAST_HYP h_simplest_elim;
+     clear_last;
+     intros ;
+     tclLAST_HYP h_simplest_case;
+     clear_last;
+     intros]
 
 let solveRightBranch  = (tclTHEN h_simplest_right h_discrConcl)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 985db4302..763ca14c3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -541,7 +541,7 @@ let discr id gls =
 	 errorlabstrm "discr" (str" Not a discriminable equality")
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "ee") gls in
-	 let e_env = push_named_decl (e,None,t) env in
+	 let e_env = push_named (e,None,t) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (indt,_) = find_mrectype env sigma t in 
@@ -790,7 +790,7 @@ let inj id gls =
 	   (str"Nothing to do, it is an equality between convertible terms")
     | Inr posns ->
 	let e = pf_get_new_id (id_of_string "e") gls in
-	let e_env = push_named_decl (e,None,t) env in
+	let e_env = push_named (e,None,t) env in
 	let injectors =
 	  map_succeed
 	    (fun (cpath,t1_0,t2_0) ->
@@ -844,7 +844,7 @@ let decompEqThen ntac id gls =
   (match find_positions env sigma t1 t2 with
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "e") gls in
-	 let e_env = push_named_decl (e,None,t) env in
+	 let e_env = push_named (e,None,t) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (pf, absurd_term) =
@@ -858,7 +858,7 @@ let decompEqThen ntac id gls =
 	   (str"Nothing to do, it is an equality between convertible terms")
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
-	  let e_env = push_named_decl (e,None,t) env in
+	  let e_env = push_named (e,None,t) env in
 	  let injectors =
 	    map_succeed
 	      (fun (cpath,t1_0,t2_0) ->
@@ -873,7 +873,7 @@ let decompEqThen ntac id gls =
 	  if injectors = [] then
 	    errorlabstrm "Equality.decompEqThen" 
               (str "Discriminate failed to decompose the equality");
-	  ((tclTHEN
+	  (tclTHEN
 	      (tclMAP (fun (injfun,resty) ->
 			 let pf = applist(lbeq.congr (),
 					  [t;resty;injfun;t1;t2;
@@ -882,7 +882,7 @@ let decompEqThen ntac id gls =
 			 ((tclTHENS (cut ty) 
 			     ([tclIDTAC;refine pf]))))
 		 (List.rev injectors))
-	      (ntac (List.length injectors))))
+	      (ntac (List.length injectors)))
 	  gls))
 
 let decompEq = decompEqThen (fun x -> tclIDTAC)
@@ -1212,7 +1212,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
 			(reduce (Pattern [(list_int nb_occ 1 [],l2,
 					   pf_type_of gls l2)]) []))
 		     (general_rewrite_bindings lft2rgt (c,lb))) 
-		  [(tclTHEN (clear_one id) (introduction id))]) gls)
+		  [(tclTHEN (clear [id]) (introduction id))]) gls)
 
 let dyn_rewrite_in lft2rgt = function
   | [Identifier id;(Command com);(Bindings binds)] -> 
@@ -1699,89 +1699,3 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
         (fun l -> validation_gen nlvalid l)
     in
     (repackage sigr gl,validation_fun)
-
-(*Collects the arguments of AutoRewrite ast node*)
-(*let dyn_autorewrite largs=
-  let rec explicit_base largs =
-    let tacargs = List.map cvt_arg largs in 
-    List.map 
-      (function
-	 | Redexp ("LR", [Coqast.Node(_,"Command", [ast])]) -> ast, true
-	 | Redexp ("RL", [Coqast.Node(_,"Command", [ast])]) -> ast, false
-	 | _ -> anomaly "Equality.explicit_base") 
-      tacargs
-  and list_bases largs =
-    let tacargs = List.map cvt_arg largs in 
-    List.map 
-      (function 
-	 | Redexp ("ByName", [Coqast.Nvar(_,s)]) -> 
-	     By_name (id_of_string s)
-	 | Redexp ("Explicit", l) ->
-	     Explicit (explicit_base l)
-	 | _ -> anomaly "Equality.list_bases") 
-      tacargs
-  and int_arg=function
-    | [(Integer n)] -> n
-    | _ -> anomalylabstrm "dyn_autorewrite" 
-	  (str "Bad call of int_arg (not an INTEGER)")
-  and list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-    (orest,evorest) (depth,evdepth) = function
-      | [] -> (lstep,ostep,lrest,orest,depth)
-      | (Redexp (s,l))::tail ->
-	  if s="Step" & not evstep then
-            list_args_rest ((List.map Tacinterp.interp l),true) (ostep,evostep)
-              (lrest,evrest) (orest,evorest) (depth,evdepth) tail
-	  else if s="SolveStep" & not evostep then
-            list_args_rest (lstep,evstep) (Solve,true) (lrest,evrest)
-              (orest,evorest) (depth,evdepth) tail
-	  else if s="Use" & not evostep then
-            list_args_rest (lstep,evstep) (Use,true) (lrest,evrest) 
-	      (orest,evorest) (depth,evdepth) tail
-	  else if s="All" & not evostep then
-            list_args_rest (lstep,evstep) (All,true) (lrest,evrest) 
-	      (orest,evorest) (depth,evdepth) tail
-	  else if s="Rest" & not evrest then
-            list_args_rest (lstep,evstep) (ostep,evostep) 
-	      ((List.map Tacinterp.interp l),true) (orest,evorest) 
-	      (depth,evdepth) tail
-	  else if s="SolveRest" & not evorest then
-            list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-              (false,true) (depth,evdepth) tail
-	  else if s="Cond" & not evorest then
-            list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-              (true,true) (depth,evdepth) tail
-	  else if s="Depth" & not evdepth then
-            (let dth = int_arg (List.map cvt_arg l) in
-             if dth > 0 then
-               list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-		 (orest,evorest) (dth,true) tail
-             else
-               errorlabstrm "dyn_autorewrite" 
-		 (str "Depth value lower or equal to 0"))
-	  else
-            anomalylabstrm "dyn_autorewrite" 
-	      (str "Bad call of list_args_rest")
-      | _ -> 
-	  anomalylabstrm "dyn_autorewrite" 
-	    (str "Bad call of list_args_rest")
-  and list_args = function
-    | (Redexp (s,lbases))::tail ->
-	if s = "BaseList" then
-          (let (lstep,ostep,lrest,orest,depth) = 
-	     list_args_rest ([],false) (Solve,false) ([],false) (false,false) 
-	       (100,false) tail
-           in
-           autorewrite (list_bases lbases) 
-	     (if lstep = [] then None else Some lstep) 
-	     ostep (if lrest=[] then None else Some lrest) orest depth)
-	else
-          anomalylabstrm "dyn_autorewrite" 
-	    (str "Bad call of list_args (not a BaseList tagged REDEXP)")
-    | _ ->
-	anomalylabstrm "dyn_autorewrite" 
-	  (str "Bad call of list_args (not a REDEXP)")
-  in
-  list_args largs*)
-
-(*Adds and hides the AutoRewrite tactic*)
-(*let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite*)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 32fc1a365..b372b8bdf 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -34,6 +34,41 @@ open Equality
 open Typing
 open Pattern
 
+let collect_meta_variables c = 
+  let rec collrec acc c = match kind_of_term c with
+    | Meta mv -> mv::acc
+    | _ -> fold_constr collrec acc c
+  in 
+  collrec [] c
+
+let check_no_metas clenv ccl =
+  if occur_meta ccl then
+    let metas = List.map (fun n -> Intmap.find n clenv.namenv)
+		  (collect_meta_variables ccl) in
+    errorlabstrm "inversion" 
+      (str ("Cannot find an instantiation for variable"^
+	       (if List.length metas = 1 then " " else "s ")) ++
+	 prlist_with_sep pr_coma pr_id metas
+	 (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *))
+
+let dest_match_eq gls eqn =
+  try 
+    pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn
+  with PatternMatchingFailure -> 
+    (try 
+       pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn
+     with PatternMatchingFailure -> 
+       (try 
+	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
+        with PatternMatchingFailure ->
+	  errorlabstrm "dest_match_eq" 
+	    (str "no primitive equality here")))
+
+let var_occurs_in_pf gl id =
+  let env = pf_env gl in
+  occur_var env id (pf_concl gl) or
+  List.exists (occur_var_in_decl env id) (pf_hyps gl)
+
 (* [make_inv_predicate (ity,args) C]
   
    is given the inductive type, its arguments, both the global
@@ -60,23 +95,6 @@ open Pattern
 
  *)
 
-let dest_match_eq gls eqn =
-  try 
-    pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn
-  with PatternMatchingFailure -> 
-    (try 
-       pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn
-     with PatternMatchingFailure -> 
-       (try 
-	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
-        with PatternMatchingFailure ->
-	  errorlabstrm "dest_match_eq" 
-	    (str "no primitive equality here")))
-    
-(* Environment management *)
-let push_rels vars env =
-  List.fold_right push_rel vars env
-
 type inversion_status = Dep of constr option | NoDep
 
 let compute_eqn env sigma n i ai =
@@ -93,7 +111,7 @@ let make_inv_predicate env sigma ind id status concl =
 	  let hyps_arity,_ = get_arity env indf in
 	  (hyps_arity,concl)
       | Dep dflt_concl ->
-	  if not (dependent (mkVar id) concl) then
+	  if not (occur_var env id concl) then
 	    errorlabstrm "make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id);
           (* We abstract the conclusion of goal with respect to
@@ -111,7 +129,7 @@ let make_inv_predicate env sigma ind id status concl =
 	  (hyps,lift nrealargs bodypred)
   in
   let nhyps = List.length hyps in
-  let env' = push_rels hyps env in
+  let env' = push_rel_context hyps env in
   let realargs' = List.map (lift nhyps) realargs in
   let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
   (* Now the arity is pushed, and we need to construct the pairs
@@ -178,8 +196,6 @@ let make_inv_predicate env sigma ind id status concl =
    the equality, using Injection and Discriminate, and applying it to
    the concusion *)
 
-let introsReplacing = intros_replacing (* déplacé *)
-
 (* Computes the subset of hypothesis in the local context whose
    type depends on t (should be of the form (mkVar id)), then
    it generalizes them, applies tac to rewrite all occurrencies of t,
@@ -196,45 +212,12 @@ let rec dependent_hyps id idlist sign =
   in 
   dep_rec idlist 
 
-let generalizeRewriteIntros tac depids id gls = 
-  let dids = dependent_hyps id depids (pf_env gls) in
-  (tclTHEN (bring_hyps dids)
-     (tclTHEN tac
-	(introsReplacing (ids_of_named_context dids))))
-  gls
-
-let var_occurs_in_pf gl id =
-  let env = pf_env gl in
-  occur_var env id (pf_concl gl) or
-  List.exists (occur_var_in_decl env id) (pf_hyps gl)
-
 let split_dep_and_nodep hyps gl =
   List.fold_right 
     (fun (id,_,_ as d) (l1,l2) ->
        if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2))
     hyps ([],[])
 
-(*
-let split_dep_and_nodep hyps gl =
-  let env = pf_env gl in
-  let cl = pf_concl gl in
-  let l1,l2 =
-    List.fold_left
-      (fun (l1,l2) (id,_,_ as d) ->
-         if
-           occur_var env id cl
-           or List.exists (occur_var_in_decl env id) hyps
-           or List.exists (fun (id,_,_) -> occur_var_in_decl env id d) l1
-         then (d::l1,l2)
-         else (l1,d::l2))
-      ([],[]) hyps
-  in (List.rev l1,List.rev l2)
-*)
-
-(* invariant: ProjectAndApply is responsible for erasing the clause
-   which it is given as input
-   It simplifies the clause (an equality) to use it as a rewrite rule and then
-   erases the result of the simplification. *)
 
 let dest_eq gls t =
   match dest_match_eq gls t with
@@ -242,6 +225,16 @@ let dest_eq gls t =
         (x,pf_whd_betadeltaiota gls y, pf_whd_betadeltaiota gls z)
     | _ -> error "dest_eq: should be an equality"
 
+let generalizeRewriteIntros tac depids id gls = 
+  let dids = dependent_hyps id depids (pf_env gls) in
+  (tclTHENSEQ
+    [bring_hyps dids; tac; intros_replacing (ids_of_named_context dids)])
+  gls
+
+(* invariant: ProjectAndApply is responsible for erasing the clause
+   which it is given as input
+   It simplifies the clause (an equality) to use it as a rewrite rule and then
+   erases the result of the simplification. *)
 (* invariant: ProjectAndApplyNoThining simplifies the clause (an equality) .
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
@@ -266,57 +259,56 @@ let projectAndApply thin id depids gls =
   match (thin, kind_of_term t1, kind_of_term t2) with
     | (true, Var id1,  _) ->
         generalizeRewriteIntros
-          (tclTHEN (subst_hyp_LR id) (clear_clause id)) depids id1 gls
+          (tclTHEN (subst_hyp_LR id) (clear [id])) depids id1 gls
     | (false, Var id1,  _) ->
         generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
     | (true, _ , Var id2) ->
         generalizeRewriteIntros
-          (tclTHEN (subst_hyp_RL id) (clear_clause id)) depids id2 gls
+          (tclTHEN (subst_hyp_RL id) (clear [id])) depids id2 gls
     | (false, _ , Var id2) ->
         generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
     | (true, _, _) ->
         let deq_trailer neqns =
           tclDO neqns
-            (tclTHEN intro (tclTHEN subst_hyp (onLastHyp clear_clause)))
+            (tclTHENSEQ
+              [intro; subst_hyp; onLastHyp (fun id -> clear [id])])
         in 
-	(tclTHEN (tclTRY (dEqThen deq_trailer (Some id))) (clear_one id)) gls
+	(tclTHEN (tclTRY (dEqThen deq_trailer (Some id))) (clear [id])) gls
     | (false, _, _) -> 
         let deq_trailer neqns = tclDO neqns (tclTHEN intro subst_hyp) in 
-	(tclTHEN (dEqThen deq_trailer (Some id)) (clear_one id)) gls
+	(tclTHEN (dEqThen deq_trailer (Some id)) (clear [id])) gls
 
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
-let case_trailer_gene othin neqns ba gl =
+let rewrite_equations_gene othin neqns ba gl =
   let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
   let rewrite_eqns =
     match othin with
       | Some thin ->
           onLastHyp
             (fun last ->
-               (tclTHEN
-                  (tclDO neqns
+              tclTHENSEQ
+                [tclDO neqns
                      (tclTHEN intro
                         (onLastHyp
                            (fun id ->
-                              tclTRY (projectAndApply thin id depids)))))
-		  (tclTHEN
-                     (onHyps (compose List.rev (afterHyp last)) bring_hyps)
-                     (onHyps (afterHyp last)
-                        (compose clear ids_of_named_context)))))
+                              tclTRY (projectAndApply thin id depids))));
+                 onHyps (compose List.rev (afterHyp last)) bring_hyps;
+                 onHyps (afterHyp last)
+                   (compose clear ids_of_named_context)])
       | None -> tclIDTAC
   in
-  (tclTHEN (tclDO neqns intro)
-     (tclTHEN (bring_hyps nodepids)
-	(tclTHEN (clear_clauses (ids_of_named_context nodepids))
-	   (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
-	      (tclTHEN (onHyps (nLastHyps neqns)
-                          (compose clear_clauses ids_of_named_context))
-		 (tclTHEN rewrite_eqns
-		    (tclMAP (fun (id,_,_ as d) ->
-			       (tclORELSE (clear_clause id)
-				  (tclTHEN (bring_hyps [d])
-				     (clear_one id))))
-		       depids)))))))
+  (tclTHENSEQ
+    [tclDO neqns intro;
+     bring_hyps nodepids;
+     clear (ids_of_named_context nodepids);
+     onHyps (compose List.rev (nLastHyps neqns)) bring_hyps;
+     onHyps (nLastHyps neqns) (compose clear ids_of_named_context);
+     rewrite_eqns;
+     tclMAP (fun (id,_,_ as d) ->
+               (tclORELSE (clear [id])
+                 (tclTHEN (bring_hyps [d]) (clear [id]))))
+       depids])
   gl
 
 (* Introduction of the equations on arguments
@@ -324,49 +316,40 @@ let case_trailer_gene othin neqns ba gl =
      None: the equations are introduced, but not rewritten
      Some thin: the equations are rewritten, and cleared if thin is true *)
 
-let case_trailer othin neqns ba gl =
+let rewrite_equations othin neqns ba gl =
   let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
   let rewrite_eqns =
     match othin with
       | Some thin ->
-          (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
-             (tclTHEN (onHyps (nLastHyps neqns) 
-                         (compose clear_clauses ids_of_named_context))
-		(tclTHEN
-		   (tclDO neqns
-                      (tclTHEN intro
-			 (onLastHyp
-			    (fun id -> 
-			       tclTRY (projectAndApply thin id depids)))))
-		   (tclTHEN (tclDO (List.length nodepids) intro)
-		      (tclMAP (fun (id,_,_) -> 
-				 tclTRY (clear_clause id)) depids)))))
+          tclTHENSEQ
+            [onHyps (compose List.rev (nLastHyps neqns)) bring_hyps;
+             onHyps (nLastHyps neqns) (compose clear ids_of_named_context);
+	     tclDO neqns
+               (tclTHEN intro
+		 (onLastHyp
+		   (fun id -> tclTRY (projectAndApply thin id depids))));
+	     tclDO (List.length nodepids) intro;
+	     tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids]
       | None -> tclIDTAC
   in
-  (tclTHEN (tclDO neqns intro)
-     (tclTHEN (bring_hyps nodepids)
-	(tclTHEN (clear_clauses (ids_of_named_context nodepids))
-	   rewrite_eqns)))
+  (tclTHENSEQ
+    [tclDO neqns intro;
+     bring_hyps nodepids;
+     clear (ids_of_named_context nodepids);
+     rewrite_eqns])
   gl
 
-let collect_meta_variables c = 
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | _ -> fold_constr collrec acc c
-  in 
-  collrec [] c
+let rewrite_equations_tac (gene, othin) id neqns ba =
+  let tac =
+    if gene then rewrite_equations_gene othin neqns ba
+    else rewrite_equations othin neqns ba in
+  if othin = Some true (* if Inversion_clear, clear the hypothesis *) then 
+    tclTHEN tac (tclTRY (clear [id]))
+  else 
+    tac
 
-let check_no_metas clenv ccl =
-  if occur_meta ccl then
-    let metas = List.map (fun n -> Intmap.find n clenv.namenv)
-		  (collect_meta_variables ccl) in
-    errorlabstrm "res_case_then" 
-      (str ("Cannot find an instantiation for variable"^
-	       (if List.length metas = 1 then " " else "s ")) ++
-	 prlist_with_sep pr_coma pr_id metas
-	 (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *))
 
-let res_case_then gene thin indbinding id status gl =
+let raw_inversion inv_kind indbinding id status gl =
   let env = pf_env gl and sigma = project gl in
   let c = mkVar id in
   let (wc,kONT) = startWalk gl in
@@ -379,7 +362,7 @@ let res_case_then gene thin indbinding id status gl =
   let (IndType (indf,realargs) as indt) =
     try find_rectype env sigma ccl
     with Not_found ->
-      errorlabstrm "res_case_then"
+      errorlabstrm "raw_inversion"
 	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let (elim_predicate,neqns) =
     make_inv_predicate env sigma indt id status (pf_concl gl) in
@@ -389,12 +372,9 @@ let res_case_then gene thin indbinding id status gl =
     else 
       applist(elim_predicate,realargs),case_nodep_then_using 
   in
-  let case_trailer_tac =
-    if gene then case_trailer_gene thin neqns else case_trailer thin neqns
-  in
   (tclTHENS
      (true_cut_anon cut_concl)
-     [case_tac (introCaseAssumsThen case_trailer_tac)
+     [case_tac (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
         (Some elim_predicate) ([],[]) newc;
       onLastHyp
         (fun id ->
@@ -435,15 +415,12 @@ let wrap_inv_error id = function
   | Not_found  ->  errorlabstrm "Inv" (not_found_message [id]) 
   | e -> raise e
 
-let inv gene thin status id =
-  let inv_tac = res_case_then gene thin [] id status in
-  let tac =
-    if thin = Some true (* if Inversion_clear, clear the hypothesis *) then 
-      tclTHEN inv_tac (tclTRY (clear_clause id))
-    else 
-      inv_tac
-  in 
-  fun gls -> try tac gls with e -> wrap_inv_error id e
+(* The most general inversion tactic *)
+let inversion inv_kind status id gls =
+  try (raw_inversion inv_kind [] id status) gls
+  with e -> wrap_inv_error id e
+
+(* Specializing it... *)
 
 let hinv_kind = Quoted_string "HalfInversion"
 let inv_kind = Quoted_string "Inversion"
@@ -460,7 +437,9 @@ let (half_inv_tac, inv_tac, inv_clear_tac) =
     hide_tactic "Inv"
       (function
 	 | ic :: [id_or_num] ->
-	     tactic_try_intros_until (inv false (com_of_id ic) NoDep) id_or_num
+	     tactic_try_intros_until
+               (inversion (false, com_of_id ic) NoDep)
+               id_or_num
 	 | l -> bad_tactic_args "Inv" l)
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
@@ -473,7 +452,7 @@ let named_inv =
   let gentac =
     hide_tactic "NamedInv"
       (function
-	 | [ic; Identifier id] -> inv true (com_of_id ic) NoDep id
+	 | [ic; Identifier id] -> inversion (true, com_of_id ic) NoDep id
 	 | l -> bad_tactic_args "NamedInv" l)
   in 
   (fun ic id -> gentac [ic; Identifier id])
@@ -484,7 +463,8 @@ let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
     hide_tactic "DInv"
       (function
 	 | ic :: [id_or_num] ->
-	     tactic_try_intros_until (inv false (com_of_id ic) (Dep None))
+	     tactic_try_intros_until
+               (inversion (false, com_of_id ic) (Dep None))
 	       id_or_num
 	 | l -> bad_tactic_args "DInv" l)
   in
@@ -500,12 +480,13 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
 	 | [ic; id_or_num; Command com] ->
 	     tactic_try_intros_until
                (fun id gls -> 
-		  inv false (com_of_id ic)
-		    (Dep (Some (pf_interp_constr gls com))) id gls)
+		 inversion (false, com_of_id ic)
+		   (Dep (Some (pf_interp_constr gls com))) id gls)
 	       id_or_num
 	 | [ic; id_or_num; Constr c] ->
 	     tactic_try_intros_until
-               (fun id gls -> inv false (com_of_id ic) (Dep (Some c)) id gls)
+               (fun id gls ->
+                 inversion (false, com_of_id ic) (Dep (Some c)) id gls)
 	       id_or_num
 	 | l -> bad_tactic_args "DInvWith" l)
   in
@@ -525,14 +506,13 @@ let invIn com id ids gls =
       nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init)
     in 
     if nb_of_new_hyp < 1 then 
-      introsReplacing ids gls
+      intros_replacing ids gls
     else 
-      tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids) gls
+      tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls
   in
   try 
-    (tclTHEN (bring_hyps hyps)
-       (tclTHEN (inv false com NoDep id)
-          (intros_replace_ids)))
+    (tclTHENSEQ
+      [bring_hyps hyps; inversion (false, com) NoDep id; intros_replace_ids])
     gls
   with e -> wrap_inv_error id e
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1344e009b..343361815 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -137,11 +137,11 @@ let rec add_prods_sign env sigma t =
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named_decl (id,None,c1) env) sigma b'
+        add_prods_sign (push_named (id,None,c1) env) sigma b'
     | LetIn (na,c1,t1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named_decl (id,Some c1,t1) env) sigma b'
+        add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -186,7 +186,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
-  let extenv = push_named_decl (p,None,npty) env in
+  let extenv = push_named (p,None,npty) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
diff --git a/tactics/refine.ml b/tactics/refine.ml
index cc90f4b23..7567ae35e 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -150,7 +150,7 @@ let rec compute_metamap env gmm c = match kind_of_term c with
    *    où x est une variable FRAICHE *)
   | Lambda (name,c1,c2) ->
       let v = fresh env name in
-      let env' = push_named_decl (v,None,c1) env in
+      let env' = push_named (v,None,c1) env in
       begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -164,7 +164,7 @@ let rec compute_metamap env gmm c = match kind_of_term c with
       if occur_meta c1 then 
 	error "Refine: body of let-in cannot contain existentials";
       let v = fresh env name in
-      let env' = push_named_decl (v,Some c1,t1) env in
+      let env' = push_named (v,Some c1,t1) env in
       begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 70716cde2..78e80a0ec 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -48,6 +48,9 @@ let tclDO            = Tacmach.tclDO
 let tclPROGRESS      = Tacmach.tclPROGRESS
 let tclWEAK_PROGRESS = Tacmach.tclWEAK_PROGRESS
 
+(* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
+let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
+
 (* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
 (* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
 let tclMAP tacfun l = 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index a984d791f..af0ea2a66 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -29,6 +29,7 @@ val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
 val tclTHENSi        : tactic -> tactic list -> (int -> tactic) -> tactic
+val tclTHENSEQ       : tactic list -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b338e1c70..5623e3899 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -739,7 +739,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl =
   let abstract ((depdecls,marks as accu),lhyp) (hyp,_,_ as d) =
     try
       let occ = if everywhere then [] else List.assoc hyp occ_hyps in
-      let newdecl = subst_term_occ_decl occ c d in
+      let newdecl = subst_term_occ_decl env occ c d in
       if d = newdecl then
 	if not everywhere then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	else (accu, Some hyp)
@@ -754,7 +754,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl =
   let occ_ccl = if everywhere then Some [] else occ_ccl in
   let ccl = match occ_ccl with
     | None -> pf_concl gl
-    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl))
+    | Some occ -> subst1 (mkVar id) (subst_term_occ env occ c (pf_concl gl))
   in
   (depdecls,marks,ccl)
 
@@ -874,7 +874,6 @@ let dyn_assumption = function
  * goal. *)                                                               
 
 let clear ids gl    = thin ids gl
-let clear_one id gl = clear [id] gl
 let dyn_clear = function
   | [Clause ids] ->
       let out = function InHyp id -> id | _ -> assert false in
@@ -888,20 +887,6 @@ let dyn_clear_body = function
       clear_body (List.map out ids)
   | l -> bad_tactic_args "clear_body" l
 
-(* Clears a list of identifiers clauses form the context *)
-(*
-let clear_clauses clsl =
-  clear (List.map 
-           (function 
-	      | Some id -> id
-              | None    -> error "ThinClauses") clsl)
-*)
-let clear_clauses = clear
-
-(* Clears one identifier clause from the context *)
-
-let clear_clause cls = clear_clauses [cls]
-
 
 (*   Takes a list of booleans, and introduces all the variables 
  *  quantified in the goal which are associated with a value
@@ -911,7 +896,8 @@ let rec intros_clearing = function
   | []          -> tclIDTAC
   | (false::tl) -> tclTHEN intro (intros_clearing tl)
   | (true::tl)  ->
-      tclTHENLIST [ intro; onLastHyp clear_clause; intros_clearing tl]
+      tclTHENLIST
+        [ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl]
 
 (* Adding new hypotheses  *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 568ce9c48..3f611f831 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -152,15 +152,11 @@ val pattern_option    :
 (*s Modification of the local context. *)
 
 val clear         : identifier list -> tactic
-val clear_one     : identifier -> tactic
 val dyn_clear     : tactic_arg list -> tactic
 
 val clear_body    : identifier list -> tactic
 val dyn_clear_body : tactic_arg list -> tactic
 
-val clear_clauses : identifier list -> tactic
-val clear_clause  : identifier -> tactic
-
 val new_hyp       : int option ->constr -> constr substitution -> tactic
 val dyn_new_hyp   : tactic_arg list -> tactic
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e34d6b919..9c1192112 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -276,7 +276,7 @@ let build_recursive lnameargsardef =
            let arity = interp_type sigma env0 raw_arity in
            let _ = declare_variable recname
 	     (Lib.cwd(),SectionLocalAssum arity, NeverDischarge) in
-           (Environ.push_named_decl (recname,None,arity) env, (arity::arl)))
+           (Environ.push_named (recname,None,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
       States.unfreeze fs; raise e in
@@ -340,7 +340,7 @@ let build_corecursive lnameardef =
 	   let arity = arj.utj_val in
            let _ = declare_variable recname
 	     (Lib.cwd(),SectionLocalAssum arj.utj_val,NeverDischarge) in
-           (Environ.push_named_decl (recname,None,arity) env, (arity::arl)))
+           (Environ.push_named (recname,None,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
       States.unfreeze fs; raise e in 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5beedfff8..457a8eaf5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -56,14 +56,14 @@ let typecheck_params_and_field ps fs =
     List.fold_left
       (fun (env,newps) (id,t) -> 
          let decl = interp_decl Evd.empty env (id,true,t) in
-         (push_named_decl decl env,decl::newps))
+         (push_named decl env,decl::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) d ->
          let decl = interp_decl Evd.empty env d in
-         (push_named_decl decl env, decl::newfs))
+         (push_named decl env, decl::newfs))
       (env1,[]) fs
   in
   newps, newfs