Abstraction de constr

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

44 files changed, 378 insertions, 483 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9b770512a0..678bdd8b39 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -489,8 +489,8 @@ let occurence path (t : constr) =
   loop path t
 
 let abstract_path typ path t =
-  let term_occur = ref (Rel 0) in
-  let abstract = context (fun i t -> term_occur:= t; Rel i) path t in
+  let term_occur = ref (mkRel 0) in
+  let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
   mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path gl =
@@ -565,9 +565,9 @@ let clever_rewrite_base_poly typ p result theorem gl =
 	  mkArrow typ mkProp,
           mkLambda
 	    (Name (id_of_string "H"),
-	     applist (Rel 1,[result]),
+	     applist (mkRel 1,[result]),
 	     mkAppL (Lazy.force coq_eq_ind_r, 
-		       [| typ; result; Rel 2; Rel 1; occ; theorem |]))),
+		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
        [abstracted]) 
   in
   exact (applist(t,[mkNewMeta()])) gl
@@ -1214,7 +1214,7 @@ let replay_history tactic_normalisation =
 		      mkLambda
 			(Name(id_of_string v),
 			 Lazy.force coq_Z,
-			 mk_eq (Rel 1) eq1) |])
+			 mk_eq (mkRel 1) eq1) |])
 	  in
 	  let mm = mk_integer m in
 	  let p_initial = [P_APP 2;P_TYPE] in
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 633be8d914..f16b6049ed 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -198,7 +198,7 @@ let compute_lhs typ i nargsi =
 let compute_rhs bodyi index_of_f =
   let rec aux c = 
     match decomp_term c with
-      | IsAppL (Rel j, args) when j = index_of_f (* recursive call *) -> 
+      | IsAppL (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
           let i = destRel (array_last args) in mkMeta i
       | IsAppL (f,args) ->
           mkAppL (f, Array.map aux args)
@@ -209,8 +209,9 @@ let compute_rhs bodyi index_of_f =
 
 (*s Now the function [compute_ivs] itself *)
 
-let compute_ivs gl f cs = 
-  let body = constant_value (Global.env()) f in
+let compute_ivs gl f cs =
+  let cst = try destConst f with _ -> i_can't_do_that () in
+  let body = constant_value (Global.env()) cst in
   match decomp_term body with
     | IsFix(([| len |], 0), ([| typ |], [ name ], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
@@ -233,8 +234,9 @@ let compute_ivs gl f cs =
                                       i nargsi)
            (* Then we test if the RHS is the RHS for variables *)
                    else begin match decomp_app bodyi with 
-                     | vmf, [_; _; Rel ri; Rel rj]
-                         when pf_conv_x gl vmf 
+                     | vmf, [_; _; a3; a4 ]
+                         when isRel a3 & isRel a4 &
+			   pf_conv_x gl vmf 
                            (Lazy.force coq_varmap_find)->
                              v_lhs := Some (compute_lhs 
                                               (snd (List.hd args3))
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index b628956af7..f5a8746b97 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -15,7 +15,8 @@ open Printer
 open Equality
 open Vernacinterp
 open Libobject
-open Closure 
+open Closure
+open Tacred
 open Tactics
 open Pattern 
 open Hiddentac
@@ -518,26 +519,21 @@ module SectionPathSet =
 	     let compare = Pervasives.compare
 	   end)
 
+(* Avec l'uniformisation des red_kind, on perd ici sur la structure
+   SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
 let constants_to_unfold = 
-  List.fold_right SectionPathSet.add 
+(*  List.fold_right SectionPathSet.add *)
     [ path_of_string "#Ring_normalize#interp_cs.cci";
       path_of_string "#Ring_normalize#interp_var.cci";
       path_of_string "#Ring_normalize#interp_vl.cci";
       path_of_string "#Ring_abstract#interp_acs.cci";
       path_of_string "#Ring_abstract#interp_sacs.cci";
       path_of_string "#Quote#varmap_find.cci" ]
-    SectionPathSet.empty 
+(*    SectionPathSet.empty *)
 
 (* Unfolds the functions interp and find_btree in the term c of goal gl *)
 let polynom_unfold_tac =
-  let flags = 
-    (UNIFORM,
-     { r_beta = true;
-       r_delta = (function
-                    | Const sp -> SectionPathSet.mem sp constants_to_unfold
-                    | _ -> false);
-       r_iota = true })
-  in
+  let flags = (UNIFORM, red_add betaiota_red (CONST constants_to_unfold)) in
   reduct_in_concl (cbv_norm_flags flags)
       
 (* lc : constr list *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 257cba2b14..803d197f18 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -9,7 +9,6 @@ open Univ
 (* open Generic *)
 open Term
 open Declarations
-open Abstraction
 
 (* The type of environments. *)
 
@@ -17,12 +16,11 @@ type checksum = int
 
 type import = string * checksum
 
-type global = Constant | Inductive | Abstraction
+type global = Constant | Inductive
 
 type globals = {
   env_constants : constant_body Spmap.t;
   env_inductives : mutual_inductive_body Spmap.t;
-  env_abstractions : abstraction_body Spmap.t;
   env_locals : (global * section_path) list;
   env_imports : import list }
 
@@ -44,7 +42,6 @@ let empty_env = {
   env_globals = {
     env_constants = Spmap.empty;
     env_inductives = Spmap.empty;
-    env_abstractions = Spmap.empty;
     env_locals = [];
     env_imports = [] };
   env_universes = initial_universes }
@@ -110,7 +107,7 @@ let push_rels_to_vars env =
     (fun (na,c,t) (subst,avoid,sign) ->
        let na = if na = Anonymous then Name(id_of_string"_") else na in
        let id = next_name_away na avoid in
-       ((VAR id)::subst,id::avoid,
+       ((mkVar id)::subst,id::avoid,
 	add_var (id,option_app (substl subst) c,typed_app (substl subst) t)
 	  sign))
     env.env_context.env_rel_context ([],ids_of_var_context sign0,sign0)
@@ -166,15 +163,6 @@ let add_mind sp mib env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
-let add_abstraction sp ab env =
-  let new_abs = Spmap.add sp ab env.env_globals.env_abstractions in
-  let new_locals = (Abstraction,sp)::env.env_globals.env_locals in
-  let new_globals = 
-    { env.env_globals with 
-	env_abstractions = new_abs;
-	env_locals = new_locals } in
-  { env with env_globals = new_globals }
-
 let meta_ctr=ref 0;;
 
 let new_meta ()=incr meta_ctr;!meta_ctr;;
@@ -201,9 +189,6 @@ let lookup_constant sp env =
 let lookup_mind sp env =
   Spmap.find sp env.env_globals.env_inductives
 
-let lookup_abst sp env =
-  Spmap.find sp env.env_globals.env_abstractions
-
 (* First character of a constr *)
 
 let lowercase_first_char id = String.lowercase (first_char id)
@@ -311,12 +296,12 @@ let make_all_name_different env =
     env
 
 (* Constants *)
-let defined_constant env = function
-  | DOPN (Const sp, _) -> is_defined (lookup_constant sp env)
+let defined_constant env c = match kind_of_term c with
+  | IsConst (sp, _) -> is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
 
-let opaque_constant env = function
-  | DOPN (Const sp, _) -> is_opaque (lookup_constant sp env)
+let opaque_constant env c = match kind_of_term c with
+  | IsConst (sp, _) -> is_opaque (lookup_constant sp env)
   | _ -> invalid_arg "opaque_constant"
 
 (* A const is evaluable if it is defined and not opaque *)
@@ -333,15 +318,13 @@ type compiled_env = {
   cenv_stamp : checksum;
   cenv_needed : import list;
   cenv_constants : (section_path * constant_body) list;
-  cenv_inductives : (section_path * mutual_inductive_body) list;
-  cenv_abstractions : (section_path * abstraction_body) list }
+  cenv_inductives : (section_path * mutual_inductive_body) list }
 
 let exported_objects env =
   let gl = env.env_globals in
   let separate (cst,ind,abs) = function
     | (Constant,sp) -> (sp,Spmap.find sp gl.env_constants)::cst,ind,abs
     | (Inductive,sp) -> cst,(sp,Spmap.find sp gl.env_inductives)::ind,abs
-    | (Abstraction,sp) -> cst,ind,(sp,Spmap.find sp gl.env_abstractions)::abs
   in
   List.fold_left separate ([],[],[]) gl.env_locals
 
@@ -351,8 +334,7 @@ let export env id =
     cenv_stamp = 0;
     cenv_needed = env.env_globals.env_imports;
     cenv_constants = cst;
-    cenv_inductives = ind;
-    cenv_abstractions = abs }
+    cenv_inductives = ind }
 
 let check_imports env needed =
   let imports = env.env_globals.env_imports in
@@ -380,7 +362,6 @@ let import cenv env =
   let new_globals = 
     { env_constants = add_list gl.env_constants cenv.cenv_constants;
       env_inductives = add_list gl.env_inductives cenv.cenv_inductives;
-      env_abstractions = add_list gl.env_abstractions cenv.cenv_abstractions;
       env_locals = gl.env_locals;
       env_imports = (cenv.cenv_id,cenv.cenv_stamp) :: gl.env_imports }
   in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 840d10ab76..e9270c5583 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -5,7 +5,6 @@
 open Names
 open Term
 open Declarations
-open Abstraction
 open Univ
 open Sign
 (*i*)
@@ -74,9 +73,6 @@ val add_constant :
   section_path -> constant_body -> env -> env
 val add_mind : 
   section_path -> mutual_inductive_body -> env -> env
-val add_abstraction : 
-  section_path -> abstraction_body -> env -> env
-
 val new_meta : unit -> int
 
 (*s Looks up in environment *)
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 6853fc9c46..b482f94538 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -66,6 +66,7 @@ let is_defined sigma ev =
   not (info.evar_body = Evar_empty)
 
 let evar_hyps ev = var_context ev.evar_env
+let evar_body ev = ev.evar_body
 
 let id_of_existential ev =
   id_of_string ("?" ^ string_of_int ev)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 3ae00f6519..4315994964 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -49,5 +49,6 @@ val is_evar : 'a evar_map -> evar -> bool
 val is_defined : 'a evar_map -> evar -> bool
 
 val evar_hyps : 'a evar_info -> var_context
+val evar_body : 'a evar_info -> evar_body
 
 val id_of_existential : evar -> identifier
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b8649ffb2e..ee58603117 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -128,16 +128,16 @@ let explain_ind_err ntyp env0 nbpar c err =
   let env = push_rels lpar env0 in
   match err with
     | LocalNonPos kt -> 
-	raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
+	raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
     | LocalNotEnoughArgs kt -> 
 	raise (InductiveError 
-		 (NotEnoughArgs (env,c',Rel (kt+nbpar))))
+		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
     | LocalNotConstructor ->
 	raise (InductiveError 
-		 (NotConstructor (env,c',Rel (ntyp+nbpar))))
+		 (NotConstructor (env,c',mkRel (ntyp+nbpar))))
     | LocalNonPar (n,l) ->
 	raise (InductiveError 
-		 (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
+		 (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
 
 let failwith_non_pos_vect n ntypes v =
   for i = 0 to Array.length v - 1 do
@@ -153,8 +153,9 @@ let check_correct_par env nparams ntypes n l largs =
     raise (IllFormedInd (LocalNotEnoughArgs l));
   let (lpar,largs') = array_chop nparams largs in
   for k = 0 to nparams - 1 do
-    if not ((Rel (n-k-1))= whd_betadeltaiotaeta env Evd.empty lpar.(k)) then
-      raise (IllFormedInd (LocalNonPar (k+1,l)))
+    match kind_of_term (whd_betadeltaiotaeta env Evd.empty lpar.(k)) with
+      | IsRel w when (n-k-1 = w) -> ()
+      | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
   done;
   if not (array_for_all (noccur_between n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
@@ -166,7 +167,7 @@ let abstract_mind_lc env ntyps npars lc =
   else 
     let make_abs = 
       list_tabulate
-	(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps 
+	(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps 
     in 
     Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2f5e02ad43..33d15798a4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -67,7 +67,7 @@ let mis_type_nf_mconstruct i mispec =
   let specif = mis_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
@@ -75,7 +75,7 @@ let mis_type_mconstruct i mispec =
   let specif = mis_typed_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index ed625a22f0..7888afd390 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -12,8 +12,8 @@ open Declarations
 open Environ
 
 let is_id_inst inst =
-  let is_id = function
-    | id, VAR id' -> id = id'
+  let is_id (id,c) = match kind_of_term c with
+    | IsVar id' -> id = id'
     | _ -> false
   in
   List.for_all is_id inst
@@ -36,15 +36,14 @@ let constant_type env sigma (sp,args) =
   (* TODO: check args *)
   instantiate_type cb.const_hyps cb.const_type (Array.to_list args)
 
-type const_evaluation_error = NotDefinedConst | OpaqueConst
+type const_evaluation_result = NoBody | Opaque
 
-exception NotEvaluableConst of const_evaluation_error
+exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env cst =
-  let (sp,args) = destConst cst in
+let constant_value env (sp,args) =
   let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst OpaqueConst) else
-  if not (is_defined cb) then raise (NotEvaluableConst NotDefinedConst) else
+  if cb.const_opaque then raise (NotEvaluableConst Opaque) else
+  if not (is_defined cb) then raise (NotEvaluableConst NoBody) else
   match cb.const_body with
     | Some v -> 
 	let body = cook_constant v in
@@ -53,6 +52,10 @@ let constant_value env cst =
 	anomalylabstrm "termenv__constant_value"
 	  [< 'sTR "a defined constant with no body." >]
 
+let constant_opt_value env cst =
+  try Some (constant_value env cst)
+  with NotEvaluableConst _ -> None
+
 (* Existentials. *)
 
 let name_of_existential n = id_of_string ("?" ^ string_of_int n)
@@ -63,23 +66,17 @@ let existential_type sigma (n,args) =
   (* TODO: check args [this comment was in Typeops] *)
   instantiate_constr hyps info.evar_concl (Array.to_list args)
 
+exception NotInstantiatedEvar
+
 let existential_value sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
-  match info.evar_body with
+  match evar_body info with
     | Evar_defined c ->
 	instantiate_constr hyps c (Array.to_list args)
     | Evar_empty ->
-	anomaly "a defined existential with no body"
-
-let const_evar_opt_value env sigma c =
-  match c with
-    | DOPN(Const sp,_) ->
-	if evaluable_constant env c then Some (constant_value env c) else None
-    | DOPN(Evar ev,args) ->
-	if Evd.is_defined sigma ev then 
-	  Some (existential_value sigma (ev,args)) 
-	else 
-	  None
-    | _ -> invalid_arg "const_abst_opt_value"
+	raise NotInstantiatedEvar
 
+let existential_opt_value sigma ev =
+  try Some (existential_value sigma ev)
+  with NotInstantiatedEvar -> None
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 0d8c2a3039..f0719d2f1e 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -16,15 +16,21 @@ val instantiate_constr :
 val instantiate_type : 
   var_context -> typed_type -> constr list -> typed_type
 
-type const_evaluation_error = NotDefinedConst | OpaqueConst
-exception NotEvaluableConst of const_evaluation_error
+(*s [constant_value env c] raises [NotEvaluableConst Opaque] if
+   [c] is opaque and [NotEvaluableConst NoBody] if it has no
+   body and [Not_found] if it does not exist in [env] *)
 
-(* [constant_value env c] raises [NotEvaluableConst OpaqueConst] if
-   [c] is opaque and [NotEvaluableConst NotDefinedConst] if undefined *)
-val constant_value : env -> constr -> constr
+type const_evaluation_result = NoBody | Opaque
+exception NotEvaluableConst of const_evaluation_result
+
+val constant_value : env -> constant -> constr
 val constant_type : env -> 'a evar_map -> constant -> typed_type
+val constant_opt_value : env -> constant -> constr option
+
+(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+no body and [Not_found] if it does not exist in [sigma] *)
 
+exception NotInstantiatedEvar
 val existential_value : 'a evar_map -> existential -> constr
 val existential_type : 'a evar_map -> existential -> constr
-
-val const_evar_opt_value : env -> 'a evar_map -> constr -> constr option
+val existential_opt_value : 'a evar_map -> existential -> constr option
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 58295ee35e..d3b8383262 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -25,14 +25,14 @@ let typed_type_of_judgment env sigma j = j.uj_type
 
 (* This should be a type intended to be assumed *)
 let assumption_of_judgment env sigma j =
-  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) -> make_typed j.uj_val s
+  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    | IsSort s -> make_typed j.uj_val s
     | _ -> error_assumption CCI env j.uj_val
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env sigma j =
-  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) -> {utj_val = j.uj_val; utj_type = s }
+  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    | IsSort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type CCI env j
 
 let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
@@ -42,7 +42,7 @@ let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
 let relative env sigma n = 
   try
     let (_,typ) = lookup_rel_type n env in
-    { uj_val  = Rel n;
+    { uj_val  = mkRel n;
       uj_type = typed_app (lift n) typ }
   with Not_found -> 
     error_unbound_rel CCI env sigma n
@@ -141,7 +141,7 @@ let is_correct_arity env sigma kelim (c,p) indf (pt,t) =
 	    raise (Arity None)
       | IsProd (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env sigma a2 in 
-          let ksort = (match k with DOP0(Sort s) -> s 
+          let ksort = (match kind_of_term k with IsSort s -> s 
 			 | _ -> raise (Arity None)) in
 	  let ind = build_dependent_inductive indf in
           if is_conv env sigma a1 ind then
@@ -219,12 +219,12 @@ let type_of_case env sigma ci pj cj lfj =
 (* Prop and Set *)
 
 let judge_of_prop =
-  { uj_val = DOP0(Sort prop);
-    uj_type = make_typed (DOP0(Sort type_0)) type_1 }
+  { uj_val = mkSort prop;
+    uj_type = make_typed (mkSort type_0) type_1 }
 
 let judge_of_set =
-  { uj_val = DOP0(Sort spec);
-    uj_type = make_typed (DOP0(Sort type_0)) type_1 }
+  { uj_val = mkSort spec;
+    uj_type = make_typed (mkSort type_0) type_1 }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
@@ -234,14 +234,14 @@ let judge_of_prop_contents = function
 
 let judge_of_type u =
   let (uu,uuu,c) = super_super u in
-  { uj_val = DOP0 (Sort (Type u));
-    uj_type = make_typed (DOP0(Sort (Type uu))) (Type uuu) },
+  { uj_val = mkSort (Type u);
+    uj_type = make_typed (mkSort (Type uu)) (Type uuu) },
   c
 
 let type_of_sort c =
-  match c with
-    | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in Type uu, cst
-    | DOP0 (Sort (Prop _)) -> Type prop_univ, Constraint.empty
+  match kind_of_term c with
+    | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst
+    | IsSort (Prop _) -> Type prop_univ, Constraint.empty
     | _ -> invalid_arg "type_of_sort"
 
 (* Type of a lambda-abstraction. *)
@@ -290,8 +290,8 @@ let abs_rel env sigma name var j =
 
 let gen_rel env sigma name varj j =
   let var = assumption_of_type_judgment varj in
-  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) ->
+  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    | IsSort s ->
 	let (s',g) = sort_of_product varj.utj_type s (universes env) in
 	let res_type = mkSort s' in
 	let (res_kind,g') = type_of_sort res_type in
diff --git a/library/declare.ml b/library/declare.ml
index 33fb0f284a..0393f54237 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -247,16 +247,6 @@ let global_operator kind id =
   let sp = Nametab.sp_of_id kind id in
   global_sp_operator (Global.env()) sp id
 
-(*
-let construct_sp_reference env sp id =
-  let (oper,hyps) = global_sp_operator env sp id in
-  let hyps' = Global.var_context () in
-  if not (hyps_inclusion env Evd.empty hyps hyps') then
-    error_reference_variables CCI env id;
-  let ids = ids_of_sign hyps in
-  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
-*)
-
 let occur_decl env (id,c,t) hyps =
   try
     let (c',t') = Sign.lookup_id id hyps in
@@ -296,7 +286,12 @@ let construct_sp_reference env sp id =
   let hyps0 = Global.var_context () in
   let env0 = Environ.reset_context env in
   let args = List.map mkVar (ids_of_var_context hyps) in
-  let body = DOPN(oper,Array.of_list args) in
+  let body = match oper with
+    | Const sp -> mkConst (sp,Array.of_list args)
+    | MutConstruct sp -> mkMutConstruct (sp,Array.of_list args)
+    | MutInd sp -> mkMutInd (sp,Array.of_list args)
+    | _ -> assert false
+  in
   find_common_hyps_then_abstract body env0 hyps0 hyps
 
 let construct_reference env kind id =
@@ -304,7 +299,7 @@ let construct_reference env kind id =
     let sp = Nametab.sp_of_id kind id in
     construct_sp_reference env sp id
   with Not_found -> 
-    VAR (let _ = Environ.lookup_var id env in id)
+    mkVar (let _ = Environ.lookup_var id env in id)
 
 let global_sp_reference sp id = 
   construct_sp_reference (Global.env()) sp id
@@ -322,7 +317,7 @@ let global_reference_imps kind id =
     | _ -> assert false
 (*
 let global env id =
-  try let _ = lookup_glob id (Environ.context env) in VAR id
+  try let _ = lookup_glob id (Environ.context env) in mkVar id
   with Not_found -> global_reference CCI id
 *)
 let is_global id =
@@ -362,7 +357,7 @@ let declare_eliminations sp i =
   if not (list_subset ids (ids_of_var_context (Global.var_context ()))) then
     error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
-  let ctxt = Array.of_list (List.map (fun id -> VAR id) ids) in
+  let ctxt = Array.of_list (List.map mkVar ids) in
   let mispec = Global.lookup_mind_specif ((sp,i),ctxt) in 
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
diff --git a/library/indrec.ml b/library/indrec.ml
index 59e11cbff8..b39f834f4e 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -57,14 +57,14 @@ let mis_make_case_com depopt env sigma mispec kind =
        	(lambda_create env'
            (build_dependent_inductive ind,
             mkMutCase (ci,
-		       Rel (nbprod+nbargsprod),
-		       Rel 1,
+		       mkRel (nbprod+nbargsprod),
+		       mkRel 1,
 		       rel_vect nbargsprod k)))
        	lnamesar
     else
       let cs = lift_constructor (k+1) constrs.(k) in
       mkLambda_string "f"
-	(build_branch_type env' dep (Rel (k+1)) cs)
+	(build_branch_type env' dep (mkRel (k+1)) cs)
 	(add_branch (k+1))
   in
   let indf = make_ind_family (mispec,rel_list 0 nparams) in
@@ -100,7 +100,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
 	    let (_,realargs) = list_chop nparams largs in 
 	    let base = applist (lift i pk,realargs) in       
             if depK then 
-	      mkAppL (base, [|appvect (Rel (i+1),rel_vect 0 i)|])
+	      mkAppL (base, [|appvect (mkRel (i+1),rel_vect 0 i)|])
             else 
 	      base
       	| _ -> assert false 
@@ -124,13 +124,13 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
           (match optionpos with 
 	     | None -> 
 		 make_prod env (n,t,process_constr (i+1) c_0 rest 
-				  (mkAppL (lift 1 co, [|Rel 1|])))
+				  (mkAppL (lift 1 co, [|mkRel 1|])))
              | Some(dep',p) -> 
 		 let nP = lift (i+1+decP) p in
 		 let t_0 = process_pos dep' nP (lift 1 t) in 
 		 make_prod_dep (dep or dep') env
                    (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
-				       (mkAppL (lift 2 co, [|Rel 2|])))))
+				       (mkAppL (lift 2 co, [|mkRel 2|])))))
       | IsMutInd ((_,tyi),_) -> 
       	  let nP = match depPvect.(tyi) with 
 	    | Some(_,p) -> lift (i+decP) p
@@ -150,7 +150,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
 	| IsProd (n,t,c) -> lambda_name env (n,t,prec (i+1) c)
      	| IsMutInd _ -> 
             let (_,realargs) = list_chop nparams largs
-            and arg = appvect (Rel (i+1),rel_vect 0 i) in 
+            and arg = appvect (mkRel (i+1),rel_vect 0 i) in 
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -170,14 +170,14 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
            | None -> 
 	       lambda_name env
 		 (n,incast_type t,process_constr (i+1)
-		    (whd_beta (applist (lift 1 f, [(Rel 1)])))
+		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
 	       let arg = process_pos nF (lift 1 (body_of_type t)) in 
                lambda_name env
 		 (n,incast_type t,process_constr (i+1)
-		    (whd_beta (applist (lift 1 f, [(Rel 1); arg])))
+		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
     | (n,Some c,t)::cprest, rest -> failwith "TODO"
     | [],[] -> f
@@ -199,7 +199,7 @@ let mis_make_indrec env sigma listdepkind mispec =
       assign k = function 
 	| [] -> ()
         | (mispeci,dep,_)::rest -> 
-            (Array.set depPvec (mis_index mispeci) (Some(dep,Rel k));
+            (Array.set depPvec (mis_index mispeci) (Some(dep,mkRel k));
              assign (k-1) rest)
     in 
     assign nrec listdepkind  
@@ -230,7 +230,7 @@ let mis_make_indrec env sigma listdepkind mispec =
 		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
                 vecfi constrs recargsvec.(tyi) in
 	    let j = (match depPvec.(tyi) with 
-		       | Some (_,Rel j) -> j 
+		       | Some (_,c) when isRel c -> destRel c 
 		       | _ -> assert false) in
 	    let indf = make_ind_family
 			 (mispeci,rel_list (nrec+nbconstruct) nparams) in
@@ -240,7 +240,7 @@ let mis_make_indrec env sigma listdepkind mispec =
 		   (build_dependent_inductive
 		      (lift_inductive_family nrec indf),
 		    mkMutCase (make_default_case_info mispeci,
-			       Rel (dect+j+1), Rel 1, branches)))
+			       mkRel (dect+j+1), mkRel 1, branches)))
 		(lift_context nrec lnames)
 	    in
 	    let typtyi = 
@@ -248,9 +248,9 @@ let mis_make_indrec env sigma listdepkind mispec =
 		(prod_create env
 		   (build_dependent_inductive indf,
 		    (if dep then 
-		       appvect (Rel (nbconstruct+nar+j+1), rel_vect 0 (nar+1)) 
+		       appvect (mkRel (nbconstruct+nar+j+1), rel_vect 0 (nar+1)) 
 		     else 
-		       appvect (Rel (nbconstruct+nar+j+1), rel_vect 1 nar))))
+		       appvect (mkRel (nbconstruct+nar+j+1), rel_vect 1 nar))))
           	lnames
 	    in 
 	    mrec (i+nctyi) (nar::ln) (typtyi::ltyp) (deftyi::ldef) rest
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index af2f73b130..8991286092 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -91,20 +91,11 @@ let ident_of_nvar loc s =
     user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
   else (id_of_string s)
 
-(*
-let rctxt_of_ctxt =
-  Array.map
-    (function
-       | VAR id -> RRef (dummy_loc,RVar id)
-       | _ ->
-     error "Astterm: arbitrary substitution of references not yet implemented")
-*)
-
 let ids_of_ctxt ctxt =
   Array.to_list
     (Array.map
-       (function
-	  | VAR id -> id
+       (function c -> match kind_of_term c with
+	  | IsVar id -> id
 	  | _ ->
       error
 	"Astterm: arbitrary substitution of references not yet implemented")
@@ -132,8 +123,8 @@ let dbize_ctxt ctxt =
 
 let dbize_constr_ctxt =
   Array.map
-    (function
-       | VAR id ->
+    (function c -> match kind_of_term c with
+       | IsVar id ->
 	   (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *)
 	   RRef (dummy_loc, RVar id)
        | _ -> anomaly "Bad ast for local ctxt of a global reference")
@@ -141,7 +132,7 @@ let dbize_constr_ctxt =
 let dbize_rawconstr_ctxt =
   Array.map
     (function
-       | RRef (_, RVar id) -> VAR id
+       | RRef (_, RVar id) -> mkVar id
        | _ -> anomaly "Bad ast for local ctxt of a global reference")
 
 let dbize_global loc = function
@@ -584,8 +575,7 @@ let interp_casted_constr1 sigma env lvar lmeta com typ =
 (* To process patterns, we need a translation from AST to term
    without typing at all. *)
 
-let ctxt_of_ids ids =
-  Array.of_list (List.map (function id -> VAR id) ids)
+let ctxt_of_ids ids = Array.of_list (List.map mkVar ids)
 
 let rec pat_of_ref metas vars = function
   | RConst (sp,ctxt) -> RConst (sp, dbize_rawconstr_ctxt ctxt)
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 47c1d5716d..2d989fafc6 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -73,7 +73,7 @@ let head_of_constr_reference c = match kind_of_term c with
 
 
 (* Second part : Given a term with second-order variables in it,
-   represented by Meta's, and possibly applied using XTRA[$SOAPP] to
+   represented by Meta's, and possibly applied using [SOAPP] to
    terms, this function will perform second-order, binding-preserving,
    matching, in the case where the pattern is a pattern in the sense
    of Dale Miller.
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index a6f4bdb0e6..cbfacf1388 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -437,7 +437,7 @@ let print_opaque_name name =
 	  let cb = Global.lookup_constant sp in
           if is_defined cb then
 	    let typ = constant_type env Evd.empty cst in
-            print_typed_value (constant_value env x, typ)
+            print_typed_value (constant_value env cst, typ)
           else 
 	    anomaly "print_opaque_name"
       | IsMutInd ((sp,_),_) ->
@@ -491,7 +491,7 @@ let fprint_judge {uj_val=trm;uj_type=typ} =
 
 let unfold_head_fconst = 
   let rec unfrec k = match kind_of_term k with
-    | IsConst _ -> constant_value (Global.env ()) k 
+    | IsConst cst -> constant_value (Global.env ()) cst 
     | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b)
     | IsAppL (f,v) -> appvect (unfrec f,v)
     | _ -> k
@@ -526,8 +526,8 @@ let print_extracted_name name =
           let cont = snd(infexecute sigma (sign,fsign) a.body) in 
 	  (match cont with  (* Cradingue *)
              | Inf {_VAL=t;_TYPE=k} -> 
-		 (match whd_betadeltaiota sigma k with
-		    | DOP0 (Sort s) ->
+		 (match kind_of_term (whd_betadeltaiota sigma k) with
+		    | IsSort s ->
 			fprint_var (string_of_id name) {body=t;typ=s})
              | _  -> error "Non informative term")
 	  
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b8a39e37fa..ca948f9ef1 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -70,8 +70,8 @@ let ids_of_rctxt ctxt =
 let ids_of_ctxt ctxt =
   Array.to_list
     (Array.map
-       (function
-	  | VAR id -> id
+       (function c -> match kind_of_term c with
+	  | IsVar id -> id
 	  | _ ->
        error
        "Termast: arbitrary substitution of references not yet implemented")
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0745081760..ac778ded80 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -132,8 +132,7 @@ let mssg_this_case_cannot_occur () =
 
 (* Utils *)
 
-let ctxt_of_ids ids =
-  Array.of_list (List.map (function id -> VAR id) ids)
+let ctxt_of_ids ids = Array.of_list (List.map mkVar ids)
 let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids)
 let inductive_of_rawconstructor c =
   inductive_of_constructor (constructor_of_rawconstructor c)
@@ -589,7 +588,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let predpred = lam_it (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
-      let predbody = mkMutCase (caseinfo, predpred, Rel 1, brs) in
+      let predbody = mkMutCase (caseinfo, predpred, mkRel 1, brs) in
       let pred = lam_it (lift (List.length sign) typn) sign in
       failwith "TODO4-2"; (true,pred)
 
@@ -631,11 +630,11 @@ let rec weaken_predicate n pred =
 		    anomaly "weaken_predicate: only product can be weakened"
     | PrProd ((dep,_,IsInd (_,IndType(indf,realargs))),pred) ->
 	(* To make it more uniform, we apply realargs but they not occur! *)
-	let copt = if dep then Some (Rel n) else None in
+	let copt = if dep then Some (mkRel n) else None in
 	PrLetIn ((realargs,copt), weaken_predicate (n-1)
 		   (lift_predicate (List.length realargs) pred))
     | PrProd ((dep,_,NotInd t),pred) ->
-	let copt = if dep then Some (Rel n) else None in
+	let copt = if dep then Some (mkRel n) else None in
 	PrLetIn (([],copt), weaken_predicate (n-1) pred)
 
 let rec extract_predicate = function
@@ -770,7 +769,7 @@ let build_branch pb defaults current eqns const_info =
        (List.map (lift const_info.cs_nargs) const_info.cs_params)
        @(rel_list 0 const_info.cs_nargs)) in
 
-  (* We replace [(Rel 1)] by its expansion [ci] *)
+  (* We replace [(mkRel 1)] by its expansion [ci] *)
   let updated_old_tomatch =
     lift_subst_tomatch const_info.cs_nargs (1,ci) pb.tomatch in
   { pb with
@@ -830,13 +829,13 @@ and match_current pb (n,tm) =
 and compile_further pb firstnext rest =
   (* We pop as much as possible tomatch not dependent one of the other *)
   let nexts,future = pop_next_tomatchs [firstnext] rest in
-  (* the next pattern to match is at the end of [nexts], it has ref (Rel n)
+  (* the next pattern to match is at the end of [nexts], it has ref (mkRel n)
      where n is the length of nexts *)
   let sign = List.map (fun ((na,t),_) -> (na,type_of_tomatch_type t)) nexts in
   let currents =
     list_map_i
       (fun i ((na,t),(_,rhsdep)) ->
-	 Pushed (insert_lifted ((Rel i, lift_tomatch_type i t), rhsdep)))
+	 Pushed (insert_lifted ((mkRel i, lift_tomatch_type i t), rhsdep)))
       1 nexts in
   let pb' = { pb with
 		env = push_rels sign pb.env;
diff --git a/pretyping/class.ml b/pretyping/class.ml
index ee759ad96d..21935be3c7 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -31,8 +31,8 @@ let stre_max (stre1,stre2) =
 let stre_max4 stre1 stre2 stre3 stre4 =
   stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4)))
 
-let id_of_varid = function
-  | VAR id -> id
+let id_of_varid c = match kind_of_term c with
+  | IsVar id -> id
   | _ -> anomaly "class__id_of_varid"
 
 let stre_of_VAR c = variable_strength (destVar c)
@@ -141,7 +141,7 @@ let constructor_at_head1 t =
 let uniform_cond nargs lt = 
   let rec aux = function
     | (0,[]) -> true
-    | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l))
+    | (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l))
     | _ -> false
   in 
   aux (nargs,lt)
@@ -216,10 +216,11 @@ let prods_of t =
 let build_id_coercion idf_opt ids =
   let env = Global.env () in
   let vs = construct_reference env CCI ids in 
-  let c = match (strip_outer_cast vs) with
-    | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' ->
-	(try Instantiate.constant_value env c'
-         with _ -> errorlabstrm "build_id_coercion"
+  let c = match kind_of_term (strip_outer_cast vs) with
+    | IsConst cst -> 
+	(try Instantiate.constant_value env cst
+         with Instantiate.NotEvaluableConst _ ->
+	   errorlabstrm "build_id_coercion"
              [< 'sTR(string_of_id ids);
 		'sTR" must be a transparent constant" >])
     | _ -> 
@@ -234,7 +235,7 @@ let build_id_coercion idf_opt ids =
     it_mkLambda_or_LetIn
       (mkLambda (Name (id_of_string "x"),
 		 applistc vs (rel_list 0 llams),
-		 Rel 1))
+		 mkRel 1))
        lams
   in
   let typ_f =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c298852f40..2892cddb43 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -144,7 +144,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
                let env1 = push_rel_decl (name,assu1) env in
                let h1 = 
 		 inh_conv_coerce_to_fail env isevars t1
-		   {uj_val = Rel 1; 
+		   {uj_val = mkRel 1; 
 		    uj_type = typed_app (fun _ -> u1) assu1 } in
                let h2 = inh_conv_coerce_to_fail env isevars u2  
 			 { uj_val = mkAppL (lift 1 v, [|h1.uj_val|]);
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0801d8f2c3..dd3022764a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -262,12 +262,7 @@ let lookup_index_as_renamed t n =
   in lookup n 1 t
 
 let rec detype avoid env t =
-  match collapse_appl t with
-    (* Not well-formed constructions *)
-    | DLAM _ | DLAMV _ -> error "Cannot detype"
-    (* Well-formed constructions *)
-    | regular_constr -> 
-    (match kind_of_term regular_constr with
+  match kind_of_term (collapse_appl t) with
     | IsRel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> RRef (dummy_loc, RVar id)
@@ -331,7 +326,7 @@ let rec detype avoid env t =
 	end
 	
     | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
-    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt)
+    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt
 
 and detype_fix fk avoid env cl lfn vt =
   let lfi = List.map (fun id -> next_name_away id avoid) lfn in
@@ -366,7 +361,7 @@ and detype_eqn avoid env constr_id construct_nargs branch =
 	| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
                   termes seront construits à partir de la syntaxe Cases *)
             (* nommage de la nouvelle variable *)
-	    let new_b = applist (lift 1 b, [Rel 1]) in
+	    let new_b = applist (lift 1 b, [mkRel 1]) in
             let pat,new_avoid,new_env,new_ids =
 	      make_pat Anonymous avoid env new_b ids in
 	    buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0a400a3a6d..d3b9c04f6f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -14,7 +14,7 @@ open Recordops
 open Evarutil
 
 (* Pb: Mach cannot type evar in the general case (all Const must be applied
- * to VARs). But evars may be applied to Rels or other terms! This is the
+ * to Vars). But evars may be applied to Rels or other terms! This is the
  * difference between type_of_const and type_of_const2.
  *)
 
@@ -128,36 +128,37 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f2]
 
-    | IsEvar (sp1,al1), IsConst (sp2,al2) ->
+    | IsEvar (sp1,al1), IsConst cst2 ->
 	let f1 () =
 	  (List.length l1 <= List.length l2) &
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
 	  solve_pb env isevars(pbty,term1,applist(term2,deb2))
           & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f4 () =
-          if evaluable_constant env term2 then
-            evar_eqappr_x env isevars pbty
-              appr1 (evar_apprec env isevars l2 (constant_value env term2))
-          else false
+	  match constant_opt_value env cst2 with
+	    | Some v2 ->
+		evar_eqappr_x env isevars pbty
+		  appr1 (evar_apprec env isevars l2 v2)
+	    | None -> false
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst (sp1,al1), IsEvar (sp2,al2) ->
+    | IsConst cst1, IsEvar (sp2,al2) ->
 	let f1 () =
        	  (List.length l2 <= List.length l1) &
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
 	  solve_pb env isevars(pbty,applist(term1,deb1),term2)
           & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	and f4 () =
-          if evaluable_constant env term1 then
-            evar_eqappr_x env isevars pbty
-              (evar_apprec env isevars l1 (constant_value env term1)) appr2
-          else 
-	    false
+	  match constant_opt_value env cst1 with
+	    | Some v1 ->
+		evar_eqappr_x env isevars pbty
+		  (evar_apprec env isevars l1 v1) appr2
+	    | None -> false
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst (sp1,al1), IsConst (sp2,al2) ->
+    | IsConst (sp1,al1 as cst1), IsConst (sp2,al2 as cst2) ->
 	let f2 () =
           (sp1 = sp2)
 	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
@@ -168,14 +169,16 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	      with Not_found -> check_conv_record appr2 appr1)
            with _ -> false)
 	and f4 () =
-          if evaluable_constant env term2 then
-            evar_eqappr_x env isevars pbty
-              appr1 (evar_apprec env isevars l2 (constant_value env term2))
-          else if evaluable_constant env term1 then
-            evar_eqappr_x env isevars pbty
-              (evar_apprec env isevars l1 (constant_value env term1)) appr2
-          else 
-	    false
+	  match constant_opt_value env cst2 with
+	    | Some v2 ->
+		evar_eqappr_x env isevars pbty
+		  appr1 (evar_apprec env isevars l2 v2)
+	    | None ->
+		match constant_opt_value env cst1 with
+		  | Some v1 ->
+		      evar_eqappr_x env isevars pbty
+			(evar_apprec env isevars l1 v1) appr2
+		  | None -> false
 	in 
 	ise_try isevars [f2; f3; f4]
 
@@ -191,25 +194,29 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	solve_pb env isevars(pbty,applist(term1,deb1),term2)
         & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 
-    | IsConst (_,_), _ ->
+    | IsConst cst1, _ ->
 	let f3 () =
 	  (try conv_record env isevars (check_conv_record appr1 appr2)
            with _ -> false)
-	and f4 () = 
-	  evaluable_constant env term1 &
- 	  evar_eqappr_x env isevars pbty
-            (evar_apprec env isevars l1 (constant_value env term1)) appr2
+	and f4 () =
+	  match constant_opt_value env cst1 with
+	    | Some v1 ->
+ 		evar_eqappr_x env isevars pbty
+		  (evar_apprec env isevars l1 v1) appr2
+	    | None -> false
 	in 
 	ise_try isevars [f3; f4]
 	     
-    | _ , IsConst (_,_) -> 
+    | _ , IsConst cst2 -> 
 	let f3 () = 
 	  (try (conv_record env isevars (check_conv_record appr2 appr1))
            with _ -> false)
 	and f4 () =
-          evaluable_constant env term2 &
- 	  evar_eqappr_x env isevars pbty
-            appr1 (evar_apprec env isevars l2 (constant_value env term2))
+	  match constant_opt_value env cst2 with
+	    | Some v2 ->
+ 		evar_eqappr_x env isevars pbty
+		  appr1 (evar_apprec env isevars l2 v2)
+	    | None -> false
 	in 
 	ise_try isevars [f3; f4]
 
@@ -287,12 +294,6 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	& (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
 	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-    (***
-    | (DOP0(Implicit),[]),(DOP0(Implicit),[]) -> true
-    (* added to compare easily the specification of fixed points
-     * But b (optional env) is not updated! *)
-    ***)
-
     | (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _), _ -> false
     | _, (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _) -> false
 
@@ -320,8 +321,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) =
        xs1 xs)
     & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
     & (evar_conv_x env isevars CONV t 
-	 (if ks=[] then c 
-	  else  (DOPN(AppL,Array.of_list(c::(List.rev ks))))))
+	 (if ks=[] then c else applist (c,(List.rev ks))))
   then
     (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
                               nbimplstruc:=!nbimplstruc+(List.length ks);true)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c360df8695..8afaf83692 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -174,7 +174,7 @@ let has_ise sigma t =
   with Uninstantiated_evar _ -> true
 
 (* We try to instanciate the evar assuming the body won't depend
- * on arguments that are not Rels or VARs, or appearing several times.
+ * on arguments that are not Rels or Vars, or appearing several times.
  *)
 (* Note: error_not_clean should not be an error: it simply means that the
  * conversion test that lead to the faulty call to [real_clean] should return
@@ -182,12 +182,12 @@ let has_ise sigma t =
  *)
 
 let real_clean isevars sp args rhs =
-  let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
+  let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
       |IsRel i ->
  	 if i<=k then t
- 	 else (try List.assoc (Rel (i-k)) subst with Not_found -> t)
+ 	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
       | IsVar _ -> (try List.assoc t subst with Not_found -> t)
       | _ -> map_constr_with_binders (fun na k -> k+1) subs k t
   in
@@ -195,30 +195,6 @@ let real_clean isevars sp args rhs =
   (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
   body
 
-(*
-let real_clean isevars sp args rhs =
-  let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
-  let rec subs k t =
-    match t with
-      Rel i ->
- 	if i<=k then t
- 	else (try List.assoc (Rel (i-k)) subst with Not_found -> t)
-    | VAR _ -> (try List.assoc t subst with Not_found -> t)
-    | DOP0 _ -> t
-    | DOP1(o,a) -> DOP1(o, subs k a)
-    | DOP2(o,a,b) -> DOP2(o, subs k a, subs k b)
-    | DOPN(o,v) -> restrict_hyps isevars (DOPN(o, Array.map (subs k) v))
-    | DLAM(n,a) -> DLAM(n, subs (k+1) a)
-    | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v)
-    | CLam (n,t,c)   -> CLam (n, typed_app (subs k) t, subs (k+1) c)  
-    | CPrd (n,t,c)   -> CPrd (n, typed_app (subs k) t, subs (k+1) c)
-    | CLet (n,b,t,c) -> CLet (n, subs k b, typed_app (subs k) t, subs (k+1) c)
-  in
-  let body = subs 0 rhs in
-  (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
-  body
-*)
-
 let make_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
   let vars = 
@@ -250,7 +226,7 @@ let new_isevar isevars env typ k =
   evar
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
- * evar, i.e. tries to find the body ?sp for lhs=mkConst (sp,args)
+ * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args)
  * ?sp [ sp.hyps \ args ]  unifies to rhs
  * ?sp must be a closed term, not referring to itself.
  * Not so trivial because some terms of args may be terms that are not
@@ -266,11 +242,15 @@ let new_isevar isevars env typ k =
  * cannot be done, as in  [x:?1; y:nat; z:(le y y)] x=z
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
+
+let keep_rels_and_vars c = match kind_of_term c with
+  | IsVar _ | IsRel _ -> c
+  | _ -> mkImplicit   (* Mettre mkMeta ?? *)
+
 let evar_define isevars lhs rhs =
   let (ev,argsv) = destEvar lhs in
   if occur_evar ev rhs then error_occur_check CCI empty_env ev rhs;
-  let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
-      (Array.to_list argsv) in 
+  let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
   (* the substitution to invert *)
   let worklist = make_subst evd.evar_env args in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5743d7d063..bb396f528a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,7 +42,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
       (mkAppliedInd indt) (mis_nconstr mispec);
   if mis_is_recursive_subset [tyi] mispec then
     let dep = find_case_dep_nparams env sigma (c,p) indf pt in 
-    let init_depFvec i = if i = tyi then Some(dep,Rel 1) else None in
+    let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
     let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
     let constrs = get_constructors indf in
     (* build now the fixpoint *)
@@ -64,7 +64,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 	(lambda_create env
 	   (applist (mI,List.append (List.map (lift (nar+1)) params)
                        (rel_list 0 nar)),
-            mkMutCase (ci, lift (nar+2) p, Rel 1, branches)))
+            mkMutCase (ci, lift (nar+2) p, mkRel 1, branches)))
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
@@ -91,14 +91,6 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 
 (***********************************************************************)
 
-(*
-let ctxt_of_ids ids =
-  Array.map
-    (function
-       | RRef (_,RVar id) -> VAR id
-       | _ -> error "pretyping: arbitrary subst of ref not implemented")
-    ids
-*)
 let ctxt_of_ids cl = cl
 
 let mt_evd = Evd.empty
@@ -164,11 +156,11 @@ let pretype_id loc env lvar id =
   with Not_found ->
   try
     let (n,typ) = lookup_rel_id id (rel_context env) in
-    { uj_val  = Rel n; uj_type = typed_app (lift n) typ }
+    { uj_val  = mkRel n; uj_type = typed_app (lift n) typ }
   with Not_found ->
   try
     let typ = lookup_id_type id (var_context env) in
-    { uj_val  = VAR id; uj_type = typ }
+    { uj_val  = mkVar id; uj_type = typ }
   with Not_found ->
     error_var_not_found_loc loc CCI id
 
@@ -442,9 +434,9 @@ let j_apply f env sigma j =
     uj_type= typed_app (strong f env sigma) j.uj_type }
 
 let utj_apply f env sigma j =
-  let under_outer_cast f env sigma = function
-    | DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t)
-    | c -> f env sigma c in
+  let under_outer_cast f env sigma c = match kind_of_term c with
+    | IsCast (b,t) -> mkCast (f env sigma b,f env sigma t)
+    | _ -> f env sigma c in
   { utj_val = strong (under_outer_cast f) env sigma j.utj_val;
     utj_type = j.utj_type }
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index fdece93e21..3b7c85b405 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -28,6 +28,7 @@ type refiner_error =
   | CannotGeneralize of constr
   | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
+  | IntroNeedsProduct
 
 exception RefinerError of refiner_error
 
@@ -310,7 +311,7 @@ let prim_refiner r sigma goal =
 		 mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in
 	       [sg]
 	   | _ ->
-	       if !check then error "Introduction needs a product"
+	       if !check then raise (RefinerError IntroNeedsProduct)
 	       else anomaly "Intro: expects a product")
 	
     | { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9247d4ff6e..eade902bab 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -43,6 +43,7 @@ type refiner_error =
   | CannotGeneralize of constr
   | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
+  | IntroNeedsProduct
 
 exception RefinerError of refiner_error
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 7375947f16..6a6a019fed 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -71,7 +71,7 @@ let rec constr_list goalopt = function
        | None -> constr_list goalopt tl
        | Some goal ->
          if mem_var_context id (pf_hyps goal) then
-           (id_of_string str,VAR id)::(constr_list goalopt tl)
+           (id_of_string str,mkVar id)::(constr_list goalopt tl)
          else
            constr_list goalopt tl))
   | _::tl -> constr_list goalopt tl
@@ -356,7 +356,7 @@ let apply_one_mhyp_context lmatch mhyp lhyps noccopt =
 (* Prepares the lfun list for constr substitutions *)
 let rec make_subs_list = function
   | (id,VArg (Identifier i))::tl ->
-    (id_of_string id,VAR i)::(make_subs_list tl)
+    (id_of_string id,mkVar i)::(make_subs_list tl)
   | (id,VArg (Constr c))::tl ->
     (id_of_string id,c)::(make_subs_list tl)
   | e::tl -> make_subs_list tl
@@ -748,57 +748,34 @@ and cvt_fold (evc,env,lfun,lmatch,goalopt) = function
 
 (* Interprets the reduction flags *)
 and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf =
-  let beta = ref false in
-  let delta = ref false in
-  let iota = ref false in
-  let idents = ref (None: (sorts oper -> bool) option) in
-  let set_flag = function
-    | Node(_,"Beta",[]) -> beta := true
-    | Node(_,"Delta",[]) -> delta := true
-    | Node(_,"Iota",[]) -> iota := true
-    | Node(loc,"Unf",l) ->
-        if !delta then
-          if !idents = None then
-            let idl=
-              List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
-                (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
-            in
-              idents := Some
-                (function
-                   | Const sp -> List.mem sp idl
-                   | _ -> false)
-          else user_err_loc(loc,"flag_of_ast",
-                  [<'sTR "Cannot specify identifiers to unfold twice">])
-        else user_err_loc(loc,"flag_of_ast",
-                  [<'sTR "Delta must be specified before">])
-    | Node(loc,"UnfBut",l) ->
-        if !delta then
-          if !idents = None then
-            let idl=
-              List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
-                (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
-            in
-              idents := Some
-                (function
-                   | Const sp -> not (List.mem sp idl)
-                   | _ -> false)
-          else user_err_loc(loc,"flag_of_ast",
-                  [<'sTR "Cannot specify identifiers to unfold twice">])
-        else user_err_loc(loc,"flag_of_ast",
-                  [<'sTR "Delta must be specified before">])
-    | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast")
+  let rec add_flag red = function
+    | [] -> red
+    | Node(_,"Beta",[])::lf -> add_flag (red_add red BETA) lf
+    | Node(_,"Delta",[])::lf ->
+	(match lf with
+	   | Node(loc,"Unf",l)::lf ->
+               let idl=
+		 List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
+		   (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
+	       in add_flag (red_add red (CONST idl)) lf
+	   | Node(loc,"UnfBut",l)::lf ->
+               let idl=
+		 List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
+                   (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
+               in add_flag (red_add red (CONSTBUT idl)) lf
+	   | _ -> add_flag (red_add red DELTA) lf)
+    | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf
+    | Node(loc,("Unf"|"UnfBut"),l)::_ ->
+	user_err_loc(loc,"flag_of_ast",
+                     [<'sTR "Delta must be specified before">])
+
+    | arg::_ -> invalid_arg_loc (Ast.loc arg,"flag_of_ast")
   in
-    List.iter set_flag lf;
-    { r_beta = !beta;
-      r_iota = !iota;
-      r_delta = match (!delta,!idents) with
-          (false,_) -> (fun _ -> false)
-        | (true,None) -> (fun _ -> true)
-        | (true,Some p) -> p }
+  add_flag no_red lf;
 
 (* Interprets a reduction expression *)
 and redexp_of_ast (evc,env,lfun,lmatch,goalopt) = function
-  | ("Red", []) -> Red
+  | ("Red", []) -> Red false
   | ("Hnf", []) -> Hnf
   | ("Simpl", []) -> Simpl
   | ("Unfold", ul) ->
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ae2ebc9eec..9234d90a27 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -74,7 +74,7 @@ val pf_compute        : goal sigma -> constr -> constr
 val pf_unfoldn        : (int list * section_path) list -> goal sigma 
                         -> constr -> constr
 
-val pf_const_value : goal sigma -> constr -> constr
+val pf_const_value : goal sigma -> constant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
@@ -205,7 +205,7 @@ val ctxt_type_of        : readable_constraints -> constr -> constr
 val w_whd_betadeltaiota : walking_constraints -> constr -> constr
 val w_hnf_constr        : walking_constraints -> constr -> constr
 val w_conv_x            : walking_constraints -> constr -> constr -> bool
-val w_const_value       : walking_constraints -> constr -> constr
+val w_const_value       : walking_constraints -> constant -> constr
 val w_defined_const     : walking_constraints -> constr -> bool
 val w_defined_evar      : walking_constraints -> int -> bool
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index acf0b6cc6b..953f2f74a8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -728,7 +728,7 @@ 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 (VAR id)) 
+	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
 		(tclTHEN 
 		   (clear_one id)
 		   (search_gen decomp p db_list local_db [])))
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index bad9866f63..93e8e6c3a3 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -18,7 +18,7 @@ open Auto
 
 let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl
 
-let assumption id = e_give_exact (VAR id)
+let assumption id = e_give_exact (mkVar id)
         
 let e_assumption gl = 
   tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
@@ -26,7 +26,7 @@ let e_assumption gl =
 let e_give_exact_constr = hide_constr_tactic "EExact" e_give_exact
 
 let registered_e_assumption gl = 
-  tclFIRST (List.map (fun id gl -> e_give_exact_constr (VAR id) gl) 
+  tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
               (pf_ids_of_hyps gl)) gl
     
 let e_resolve_with_bindings_tac  (c,lbind) gl = 
@@ -53,8 +53,7 @@ let vernac_e_resolve_constr =
 
 let one_step l gl =
   [Tactics.intro]
-  @ (List.map e_resolve_constr (List.map (fun x -> VAR x)
-				  (pf_ids_of_hyps gl)))
+  @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl)))
   @ (List.map e_resolve_constr l)
   @ (List.map assumption (pf_ids_of_hyps gl))
 
@@ -197,7 +196,7 @@ let e_possible_resolve db_list local_db gl =
 (* A version with correct (?) backtracking using operations on lists 
    of goals *)
 
-let assumption_tac_list id = apply_tac_list (e_give_exact_constr (VAR id))
+let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
 
 exception Nogoals
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 2cfcd8559c..fc0dec451e 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -54,7 +54,7 @@ Another example :
 *)
 
 let elimClauseThen tac idopt gl =
-  elimination_then tac ([],[]) (VAR (out_some idopt)) gl
+  elimination_then tac ([],[]) (mkVar (out_some idopt)) gl
 
 let rec general_decompose_clause recognizer =
   ifOnClause recognizer
@@ -145,14 +145,14 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHyp
        (fun idopt gls ->
 	  let id = out_some idopt in
-	  let idty = pf_type_of gls (VAR id) in
+	  let idty = pf_type_of gls (mkVar id) in
 	  let fvty = global_vars idty in
 	  let possible_bring_ids =
 	    (List.tl (List.map out_some (nLastHyps (abs_j - abs_i) gls)))
             @bargs.assums in
 	  let (ids,_) = List.fold_left 
 			  (fun (bring_ids,leave_ids) cid ->
-                             let cidty = pf_type_of gls (VAR cid) in
+                             let cidty = pf_type_of gls (mkVar cid) in
                              if not (List.mem cid leave_ids)
                              then (cid::bring_ids,leave_ids)
                              else (bring_ids,cid::leave_ids))
@@ -160,7 +160,7 @@ let induction_trailer abs_i abs_j bargs =
 	  in 
 	  (tclTHEN (tclTHEN (bring_hyps (List.map in_some ids))
 		      (clear_clauses (List.rev (List.map in_some ids))))
-             (simple_elimination (VAR id))) gls))
+             (simple_elimination (mkVar id))) gls))
 
 let double_ind abs_i abs_j gls =
   let cl = pf_concl gls in 
@@ -169,7 +169,7 @@ let double_ind abs_i abs_j gls =
        	(fun idopt ->
            elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j))
-             ([],[]) (VAR (out_some idopt))))) gls
+             ([],[]) (mkVar (out_some idopt))))) gls
 
 let dyn_double_ind = function
   | [Integer i; Integer j] -> double_ind i j
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2b9b230115..03e4688aab 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -94,10 +94,10 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
   and t2 = pf_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
     let (e,sym) = 
-      match hnf_type_of gl t1 with 
-        | DOP0(Sort(Prop(Pos))) -> (eq,sym_eq)
-        | DOP0(Sort(Type(_)))   -> (eqt,sym_eqt)
-        | _                     -> error "replace"
+      match kind_of_term (hnf_type_of gl t1) with 
+        | IsSort (Prop(Pos)) -> (eq,sym_eq)
+        | IsSort (Type(_))   -> (eqt,sym_eqt)
+        | _                  -> error "replace"
     in 
     (tclTHENL (elim_type (applist (e, [t1;c1;c2])))
        (tclORELSE assumption 
@@ -343,24 +343,25 @@ exception DiscrFound of (sorts oper * int) list * sorts oper * sorts oper
 
 let find_positions env sigma t1 t2 =
   let rec findrec posn t1 t2 =
-    match (whd_betadeltaiota_stack env sigma t1,
-           whd_betadeltaiota_stack env sigma t2) with
+    let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in
+    let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
+    match (kind_of_term hd1, kind_of_term hd2) with
   	
-      | ((DOPN(MutConstruct sp1 as oper1,_) as hd1,args1),
-	 (DOPN(MutConstruct sp2 as oper2,_) as hd2,args2)) ->
+      | IsMutConstruct (sp1,_), IsMutConstruct (sp2,_) ->
         (* both sides are constructors, so either we descend, or we can
            discriminate here. *)
 	  if sp1 = sp2 then
             List.flatten
 	      (list_map2_i
-		 (fun i arg1 arg2 -> findrec ((oper1,i)::posn) arg1 arg2)
+		 (fun i arg1 arg2 ->
+		    findrec ((MutConstruct sp1,i)::posn) arg1 arg2)
 		 0 args1 args2)
 	  else
-	    raise (DiscrFound(List.rev posn,oper1,oper2))
+	    raise (DiscrFound(List.rev posn,MutConstruct sp1,MutConstruct sp2))
 
-      | (t1_0,t2_0) ->
-	  let t1_0 = applist t1_0
-          and t2_0 = applist t2_0 in
+      | _ ->
+	  let t1_0 = applist (hd1,args1) 
+          and t2_0 = applist (hd2,args2) in
           if is_conv env sigma t1_0 t2_0 then 
 	    []
           else
@@ -524,7 +525,7 @@ let rec build_discriminator sigma env dirn c sort = function
       let _,arsort = get_arity indf in
       let nparams = mis_nparams (fst (dest_ind_family indf)) in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
-      let newc = Rel(cnum_nlams-(argnum-nparams)) in
+      let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       (match necessary_elimination arsort (destSort sort) with
          | Type_Type ->
@@ -546,7 +547,7 @@ let gen_absurdity id gl =
   if   (pf_is_matching gl (pat_False ()) (clause_type (Some id) gl)) 
     or (pf_is_matching gl (pat_EmptyT ()) (clause_type  (Some id) gl))
   then
-    simplest_elim (VAR id) gl
+    simplest_elim (mkVar id) gl
   else
     errorlabstrm "Equality.gen_absurdity" 
       [< 'sTR "Not the negation of an equality" >]
@@ -575,7 +576,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
 	let absurd_term = build_EmptyT () in
         let h = pf_get_new_id (id_of_string "HH")gls in
         let pred= mkNamedLambda e t 
-                    (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) 
+                    (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) 
 		       discriminator)
         in (applist(eq_elim, [t;t1;pred;i;t2]), absurd_term)
 	     
@@ -608,7 +609,7 @@ let discr id gls =
 	   push_var_decl (e,assumption_of_judgment env sigma tj) env
 	 in
 	 let discriminator =
-	   build_discriminator sigma e_env dirn (VAR e) sort cpath in
+	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (indt,_) = find_mrectype env sigma t in 
 	 let arity = Global.mind_arity indt in
 	 let (pf, absurd_term) =
@@ -616,7 +617,7 @@ let discr id gls =
 	 in
 	 tclCOMPLETE((tclTHENS (cut_intro absurd_term)
 			([onLastHyp (compose gen_absurdity out_some);
-			  refine (mkAppL (pf, [| VAR id |]))]))) gls
+			  refine (mkAppL (pf, [| mkVar id |]))]))) gls
      | _ -> assert false)
 
 let not_found_message id =
@@ -696,9 +697,9 @@ let find_sigma_data s =
 
    If [rty] depends on lind, then we will build the term
 
-     (existS A==[type_of(Rel lind)] P==(Lambda(na:type_of(Rel lind),
+     (existS A==[type_of(mkRel lind)] P==(Lambda(na:type_of(mkRel lind),
                                         [rty{1/lind}]))
-              [(Rel lind)] [rterm])
+              [(mkRel lind)] [rterm])
 
    which should have type (sigS A P) - we can verify it by
    typechecking at the end.
@@ -708,12 +709,12 @@ let make_tuple env sigma (rterm,rty) lind =
   if dependent (mkRel lind) rty then
     let {intro = exist_term; ex = sig_term} =
       find_sigma_data (get_sort_of env sigma rty) in
-    let a = type_of env sigma (Rel lind) in
-    (* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *)
-    let rty' = substnl [Rel 1] lind rty in
+    let a = type_of env sigma (mkRel lind) in
+    (* We replace (mkRel lind) by (mkRel 1) in rty then abstract on (na:a) *)
+    let rty' = substnl [mkRel 1] lind rty in
     let na = fst (lookup_rel_type lind env) in
     let p = mkLambda (na, a, rty') in
-    (applist(exist_term,[a;p;(Rel lind);rterm]),
+    (applist(exist_term,[a;p;(mkRel lind);rterm]),
      applist(sig_term,[a;p]))
   else
     (rterm,rty)
@@ -839,7 +840,7 @@ let rec build_injrec sigma env (t1,t2) c = function
       let (ity,_) = find_mrectype env sigma cty in
       let nparams = Global.mind_nparams ity in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
-      let newc = Rel(cnum_nlams-(argnum-nparams)) in
+      let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let (subval,tuplety,dfltval) =
       	build_injrec sigma cnum_env (t1,t2) newc l
       in
@@ -891,7 +892,7 @@ let inj id gls =
 	  map_succeed
 	    (fun (cpath,t1_0,t2_0) ->
 	       let (injbody,resty) =
-		 build_injector sigma e_env (t1_0,t2_0) (VAR e) cpath in
+		 build_injector sigma e_env (t1_0,t2_0) (mkVar e) cpath in
 	       let injfun = mkNamedLambda e t injbody in
 	       try 
 		 let _ = type_of env sigma injfun in (injfun,resty)
@@ -907,7 +908,7 @@ let inj id gls =
 			      [t;resty;injfun;
 			       try_delta_expand env sigma t1;
 			       try_delta_expand env sigma t2;
-			       VAR id]) 
+			       mkVar id]) 
 	     in
 	     let ty = pf_type_of gls pf in
 	     ((tclTHENS  (cut  ty) ([tclIDTAC;refine pf]))))
@@ -953,13 +954,13 @@ let decompEqThen ntac id gls =
 	 let e_env =
 	   push_var_decl (e,assumption_of_judgment env sigma tj) env in
 	 let discriminator =
-	   build_discriminator sigma e_env dirn (VAR e) sort cpath in
+	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (pf, absurd_term) =
 	   discrimination_pf e (t,t1,t2) discriminator lbeq gls in
 	 tclCOMPLETE
 	   ((tclTHENS (cut_intro absurd_term)
 	       ([onLastHyp (compose gen_absurdity out_some);
-		 refine (mkAppL (pf, [| VAR id |]))]))) gls
+		 refine (mkAppL (pf, [| mkVar id |]))]))) gls
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env =
@@ -968,7 +969,7 @@ let decompEqThen ntac id gls =
 	    map_succeed
 	      (fun (cpath,t1_0,t2_0) ->
 		 let (injbody,resty) =
-		   build_injector sigma e_env (t1_0,t2_0) (VAR e) cpath in
+		   build_injector sigma e_env (t1_0,t2_0) (mkVar e) cpath in
 		 let injfun = mkNamedLambda e t injbody in
 		 try 
 		   let _ = type_of env sigma injfun in (injfun,resty)
@@ -982,7 +983,7 @@ let decompEqThen ntac id gls =
 	      (tclMAP (fun (injfun,resty) ->
 			 let pf = applist(get_squel lbeq.congr,
 					  [t;resty;injfun;t1;t2;
-					   VAR id]) in
+					   mkVar id]) in
 			 let ty = pf_type_of gls pf in
 			 ((tclTHENS (cut ty) 
 			     ([tclIDTAC;refine pf]))))
@@ -1047,7 +1048,7 @@ let swapEquandsInConcl gls =
 let swapEquandsInHyp id gls =
   ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls)))
       ([tclIDTAC;
-      	(tclTHEN (swapEquandsInConcl) (exact (VAR id)))]))) gls
+      	(tclTHEN (swapEquandsInConcl) (exact (mkVar id)))]))) gls
 
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. It yields the boolean true wether
@@ -1070,19 +1071,19 @@ let find_elim  sort_of_gl  lbeq =
 
 (* builds a predicate [e:t][H:(lbeq t e t1)](body e)
    to be used as an argument for equality dependent elimination principle:
-   Preconditon: dependent body (Rel 1) *)
+   Preconditon: dependent body (mkRel 1) *)
 
 let build_dependent_rewrite_predicate (t,t1,t2) body lbeq gls =
   let e = pf_get_new_id  (id_of_string "e") gls in 
   let h = pf_get_new_id  (id_of_string "HH") gls in 
   let eq_term = get_squel lbeq.eq in
   (mkNamedLambda e t 
-     (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) 
+     (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) 
         (lift 1 body))) 
 
 (* builds a predicate [e:t](body e) ???
    to be used as an argument for equality non-dependent elimination principle:
-   Preconditon: dependent body (Rel 1) *)
+   Preconditon: dependent body (mkRel 1) *)
 
 let build_non_dependent_rewrite_predicate (t,t1,t2) body gls =
   lambda_create (pf_env gls) (t,body)
@@ -1113,13 +1114,13 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
    and B might contain instances of the ei, we will return the term:
 
    ([x1:ty(e1)]...[xn:ty(en)]B
-    (projS1 (Rel 1))
-    (projS1 (projS2 (Rel 1)))
+    (projS1 (mkRel 1))
+    (projS1 (projS2 (mkRel 1)))
     ... etc ...)
 
    That is, we will abstract out the terms e1...en+1 as usual, but
    will then produce a term in which the abstraction is on a single
-   term - the debruijn index [Rel 1], which will be of the same type
+   term - the debruijn index [mkRel 1], which will be of the same type
    as dep_pair.
 
    ALGORITHM for abstraction:
@@ -1168,7 +1169,7 @@ let decomp_tuple_term env c t =
     with e when catchable_exception e ->
       [((ex,exty),inner_code)]
   in
-  List.split (decomprec (Rel 1) c t)
+  List.split (decomprec (mkRel 1) c t)
 
 (*
 let whd_const_state namelist env sigma = 
@@ -1198,7 +1199,7 @@ let subst_tuple_term env sigma dep_pair b =
     List.fold_right
       (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
   let app_B = applist(abst_B,proj_list) in
-  (* inutile ?? les projs sont appliquées à (Rel 1) ?? *)
+  (* inutile ?? les projs sont appliquées à (mkRel 1) ?? *)
 (*
   let { proj1 = proj1_sp; proj2 = proj2_sp; elim = sig_elim_sp } =
     find_sigma_data (get_sort_of env sigma typ) in
@@ -1236,7 +1237,7 @@ let substInHyp eqn id gls =
   (tclTHENS (cut_replacing id (subst1 e2 body))
      ([tclIDTAC;
        (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
-          ([exact (VAR id);tclIDTAC]))])) gls
+          ([exact (mkVar id);tclIDTAC]))])) gls
 
 let revSubstInHyp eqn id gls =
   (tclTHENS (substInHyp (swap_equands gls eqn) id)
@@ -1500,10 +1501,10 @@ let hypSubst id cls gls =
   match cls with
     | None -> 
 	(tclTHENS (substInConcl (clause_type (Some id) gls))
-	   ([tclIDTAC; exact (VAR id)])) gls
+	   ([tclIDTAC; exact (mkVar id)])) gls
     | Some hypid -> 
 	(tclTHENS (substInHyp (clause_type (Some id) gls) hypid)
-	   ([tclIDTAC;exact (VAR id)])) gls
+	   ([tclIDTAC;exact (mkVar id)])) gls
 
 (* id:a=b |- (P a)
  * HypSubst id.
@@ -1555,10 +1556,10 @@ let revHypSubst id cls gls =
   match cls with
     | None -> 
 	(tclTHENS (revSubstInConcl (clause_type (Some id) gls))
-	   ([tclIDTAC; exact (VAR id)])) gls
+	   ([tclIDTAC; exact (mkVar id)])) gls
     | Some hypid -> 
 	(tclTHENS (revSubstInHyp (clause_type (Some id) gls) hypid)
-	   ([tclIDTAC;exact (VAR id)])) gls
+	   ([tclIDTAC;exact (mkVar id)])) gls
 
 (* id:a=b |- (P b)
  * HypSubst id.
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index cc88fbcd7a..d9d81238b8 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -67,8 +67,7 @@ let get_reference mods s =
 let soinstance squel arglist =
   let mvs,c = get_squel_core squel in
   let mvb = List.combine mvs arglist in 
-  Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) 
-		     empty_env Evd.empty c)
+  Reduction.local_strong (Reduction.whd_meta mvb) c
 
 let get_squel m =
   let mvs, c = get_squel_core m in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0a09c441bf..42dcb18f51 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -77,7 +77,7 @@ type inversion_status = Dep of constr option | NoDep
 
 let compute_eqn env sigma n i ai =
   (ai,get_type_of env sigma ai),
-  (Rel (n-i),get_type_of env sigma (Rel (n-i)))
+  (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
 
 let make_inv_predicate env sigma ind id status concl =
   let indf,realargs = dest_ind_type ind in
@@ -90,7 +90,7 @@ let make_inv_predicate env sigma ind id status concl =
 	  let env' = push_rels hyps_arity env in
 	  (hyps_arity,concl)
       | Dep dflt_concl ->
-	  if not (dependent (VAR id) concl) then
+	  if not (dependent (mkVar id) concl) then
 	    errorlabstrm "make_inv_predicate"
               [< 'sTR "Current goal does not depend on "; print_id id >];
           (* We abstract the conclusion of goal with respect to
@@ -102,7 +102,7 @@ let make_inv_predicate env sigma ind id status concl =
               | None ->
 		let sort = get_sort_of env sigma concl in
 		let p = make_arity env true indf sort in
-		abstract_list_all env sigma p concl (realargs@[VAR id])
+		abstract_list_all env sigma p concl (realargs@[mkVar id])
 	  in
 	  let hyps,_ = decompose_lam_n (nrealargs+1) pred in
 	  let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) 
@@ -114,9 +114,9 @@ let make_inv_predicate env sigma ind id status concl =
   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
-   * ai,Rel(n-i+1) *)
-  (* Now, we can recurse down this list, for each ai,(Rel k) whether to
-     push <Ai>(Rel k)=ai (when   Ai is closed).
+   * ai,mkRel(n-i+1) *)
+  (* Now, we can recurse down this list, for each ai,(mkRel k) whether to
+     push <Ai>(mkRel k)=ai (when   Ai is closed).
    In any case, we carry along the rest of pairs *)
   let rec build_concl eqns n = function
     | [] -> (prod_it concl eqns,n)
@@ -180,10 +180,10 @@ let make_inv_predicate env sigma ind id status concl =
 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 (VAR id)), then
+   type depends on t (should be of the form (mkVar id)), then
    it generalizes them, applies tac to rewrite all occurrencies of t,
    and introduces generalized hypotheis.
-   Precondition: t=(VAR id) *)
+   Precondition: t=(mkVar id) *)
     
 let rec dependent_hyps id idlist sign = 
   let rec dep_rec =function
@@ -229,22 +229,23 @@ let projectAndApply thin cls depids gls =
   let subst_hyp gls = 
     let orient_rule cls = 
       let (t,t1,t2) = dest_eq gls (clause_type cls gls) in
-      match (strip_outer_cast t1, strip_outer_cast t2) with
-        | (VAR id1, _) -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1
-        | (_, VAR id2) -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2
+      match (kind_of_term (strip_outer_cast t1),
+	     kind_of_term (strip_outer_cast t2)) with
+        | IsVar id1, _ -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1
+        | _, IsVar id2 -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2
         | _ -> subst_hyp_RL cls
     in 
     onLastHyp orient_rule gls 
   in
   let (t,t1,t2) = dest_eq gls (clause_type cls gls)  in
-  match (thin, strip_outer_cast t1, strip_outer_cast t2) with
-    | (true, VAR id1,  _) -> generalizeRewriteIntros
+  match (thin, kind_of_term (strip_outer_cast t1), kind_of_term (strip_outer_cast t2)) with
+    | (true, IsVar id1,  _) -> generalizeRewriteIntros
           (tclTHEN (subst_hyp_LR cls) (clear_clause cls)) depids id1 gls
-    | (false, VAR id1,  _) ->
+    | (false, IsVar id1,  _) ->
         generalizeRewriteIntros (subst_hyp_LR cls) depids id1 gls
-    | (true, _ , VAR id2) -> generalizeRewriteIntros
+    | (true, _ , IsVar id2) -> generalizeRewriteIntros
           (tclTHEN (subst_hyp_RL cls) (clear_clause cls)) depids id2 gls
-    | (false, _ , VAR id2) ->
+    | (false, _ , IsVar id2) ->
         generalizeRewriteIntros (subst_hyp_RL cls) depids id2 gls
     | (true, _, _) ->
         let deq_trailer neqns =
@@ -321,7 +322,7 @@ let case_trailer othin neqns ba gl =
 
 let res_case_then gene thin indbinding id status gl =
   let env = pf_env gl and sigma = project gl in
-  let c = VAR id in
+  let c = mkVar id in
   let (wc,kONT) = startWalk gl in
   let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
   let indclause = mk_clenv_from wc (c,t) in
@@ -348,7 +349,7 @@ let res_case_then gene thin indbinding id status gl =
      [onLastHyp
         (fun cls->
            (tclTHEN (applyUsing
-                       (applist(VAR (out_some cls),
+                       (applist(mkVar (out_some cls),
                                 list_tabulate
                                   (fun _ -> mkMeta(new_meta())) neqns)))
               Auto.default_auto));
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c5bf517713..1e115c671e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -127,12 +127,12 @@ let rec add_prods_sign env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
     | IsProd (na,c1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
-	let b'= subst1 (VAR id) b in
+	let b'= subst1 (mkVar id) b in
 	let j = Retyping.get_assumption_of env sigma c1 in
         add_prods_sign (Environ.push_var_decl (id,j) env) sigma b'
     | IsLetIn (na,c1,t1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
-	let b'= subst1 (VAR id) b in
+	let b'= subst1 (mkVar id) b in
 	let j = Retyping.get_assumption_of env sigma t1 in
         add_prods_sign (Environ.push_var_def (id,c1,j) env) sigma b'
     | _ -> (env,t)
@@ -158,7 +158,8 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
     if dep_option  then
       let pty = make_arity env true indf sort in
       let goal = 
-	mkProd (Anonymous, mkAppliedInd ind, applist(VAR p,realargs@[Rel 1]))
+	mkProd
+	  (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
       in
       pty,goal
     else
@@ -167,11 +168,11 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let revargs,ownsign =
 	fold_var_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
-             if List.mem id ivars then ((VAR id)::revargs,add_var d hyps)
+             if List.mem id ivars then ((mkVar id)::revargs,add_var d hyps)
 	     else (revargs,hyps))
           env ([],[]) in
       let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
-      let goal = mkArrow i (applist(VAR p, List.rev revargs)) in
+      let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
@@ -215,7 +216,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     List.fold_left
       (fun (avoid,sign,mvb) (mv,mvty) ->
          let h = next_ident_away (id_of_string "H") avoid in
-	 (h::avoid, add_var_decl (h,mvty) sign, (mv,VAR h)::mvb))
+	 (h::avoid, add_var_decl (h,mvty) sign, (mv,mkVar h)::mvb))
       (ids_of_context invEnv, ownSign, [])
       meta_types in
   let invProof = 
@@ -322,7 +323,7 @@ let lemInv id c gls =
   try
     let (wc,kONT) = startWalk gls in
     let clause = mk_clenv_type_of wc c in
-    let clause = clenv_constrain_with_bindings [(Abs (-1),VAR id)] clause in
+    let clause = clenv_constrain_with_bindings [(Abs (-1),mkVar id)] clause in
     res_pf kONT clause gls
   with 
 (* Ce n'est pas l'endroit pour cela
diff --git a/tactics/refine.ml b/tactics/refine.ml
index ce60df06a1..75f22c4ffc 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -134,13 +134,13 @@ let rec compute_metamap env c = match kind_of_term c with
   | IsCast (m,ty) when isMeta m -> TH (c,[destMeta m,ty],[None])
 
   (* abstraction => il faut décomposer si le terme dessous n'est pas pur
-   *    attention : dans ce cas il faut remplacer (Rel 1) par (VAR x)
+   *    attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
    *    où x est une variable FRAICHE *)
   | IsLambda (name,c1,c2) ->
       let v = fresh env name in
       let tj = Retyping.get_assumption_of env Evd.empty c1 in
       let env' = push_var_decl (v,tj) env in
-      begin match compute_metamap env' (subst1 (VAR v) c2) with
+      begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
 	(* terme de preuve incomplet *)    
@@ -162,14 +162,15 @@ let rec compute_metamap env c = match kind_of_term c with
 	  TH (c,[],[])
       end
 
-  | IsMutCase _ ->
+  | IsMutCase (ci,p,c,v) ->
       (* bof... *)
-      let op,v =
-	match c with DOPN(MutCase _ as op,v) -> (op,v) | _ -> assert false in
+      let v = Array.append [|p;c|] v in
       let a = Array.map (compute_metamap env) v in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env a in TH (DOPN(op,v'),mm,sgp)
+	  let v',mm,sgp = replace_in_array env a in
+	  let v'' = Array.sub v' 2 (Array.length v) in
+	  TH (mkMutCase (ci,v'.(0),v'.(1),v''),mm,sgp)
 	with NoMeta ->
 	  TH (c,[],[])
       end
@@ -185,7 +186,7 @@ let rec compute_metamap env c = match kind_of_term c with
       in
       let a = Array.map
 		(compute_metamap env')
-		(Array.map (substl (List.map (fun x -> VAR x) vi)) v) 
+		(Array.map (substl (List.map mkVar vi)) v) 
       in
       begin
 	try
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 60ea7e8d07..6c4665fd35 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -213,7 +213,7 @@ let dyn_change = function
 (* A function which reduces accordingly to a reduction expression,
    as the command Eval does. *)
 
-let reduce redexp cl goal = 
+let reduce redexp cl goal =
   redin_combinator (reduction_of_redexp redexp) cl goal
 
 let dyn_reduce = function
@@ -265,6 +265,7 @@ let default_id gl =
 	   | IsSort (Prop _) -> (id_of_name_with_default "H" name)
 	   | IsSort (Type _) -> (id_of_name_with_default "X" name)
 	   | _                   -> anomaly "Wrong sort")
+    | IsLetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name
     | _ -> error "Introduction needs a product"
 
 (* Non primitive introduction tactics are treated by central_intro
@@ -293,12 +294,12 @@ let rec central_intro name_flag move_flag force_flag gl =
       | None      -> introduction id gl
       | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) gl
     end
-  with (UserError ("Introduction needs a product",_)) as e ->
+  with RefinerError IntroNeedsProduct as e ->
     if force_flag then
       try
-        ((tclTHEN (reduce Red []) (central_intro name_flag move_flag
-				     force_flag)) gl)
-      with UserError ("Term not reducible",_) ->
+        ((tclTHEN (reduce (Red true) [])
+	    (central_intro name_flag move_flag force_flag)) gl)
+      with Redelimination ->
         errorlabstrm "Intro" 
 	  [<'sTR "No product even after head-reduction">]
     else
@@ -349,8 +350,8 @@ let rec intros_until s g =
     | Some depth -> tclDO depth intro g
     | None -> 
 	try
-	  ((tclTHEN (reduce Red []) (intros_until s)) g)
-	with UserError ("Term not reducible",_) ->
+	  ((tclTHEN (reduce (Red true) []) (intros_until s)) g)
+	with Redelimination ->
           errorlabstrm "Intros" 
 	    [<'sTR "No such hypothesis in current goal";
 	      'sTR " even after head-reduction" >]
@@ -360,8 +361,8 @@ let rec intros_until_n n g =
     | Some depth -> tclDO depth intro g
     | None ->
 	try
-	  ((tclTHEN (reduce Red []) (intros_until_n n)) g)
-	with UserError ("Term not reducible",_) ->
+	  ((tclTHEN (reduce (Red true) []) (intros_until_n n)) g)
+	with Redelimination ->
           errorlabstrm "Intros" 
 	    [<'sTR "No such hypothesis in current goal";
 	      'sTR " even after head-reduction" >]
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 171eea17b6..737ce8a33a 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1762,7 +1762,7 @@ let rec cci_of_tauto_fml () =
 
 let search env id =
   try
-    Rel (fst (lookup_rel_id id (Environ.rel_context env)))
+    mkRel (fst (lookup_rel_id id (Environ.rel_context env)))
   with Not_found ->
   if mem_var_context id (Environ.var_context env) then
     mkVar id
@@ -1783,7 +1783,7 @@ let cci_of_tauto_term env t =
   and ci     = global_reference CCI (id_of_string "I") 
   in  
   let rec ter_constr l = function
-    | TVar x            -> (try (try Rel(pos_lis x l)
+    | TVar x            -> (try (try mkRel(pos_lis x l)
                                  with TacticFailure -> 
                                    search env (id_of_string x))
                             with _ -> raise TacticFailure)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e23d3b7f95..d9193a8ff4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -124,13 +124,6 @@ let corecursive_message = function
   | l   -> hOV 0 [< prlist_with_sep pr_coma print_id l;
                     'sPC; 'sTR "are corecursively defined">]
 
-let put_DLAMSV_subst lid lc = 
-  match lid with
-    | [] -> anomaly "put_DLAM"
-    | id::lrest ->  
-        List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c)) 
-          (DLAMV(Name id,Array.map (subst_var id) lc)) lrest
-
 let build_mutual lparams lnamearconstrs finite =
   let allnames = 
     List.fold_left 
@@ -244,14 +237,18 @@ let build_recursive lnameargsardef =
     collect_non_rec lrecnames recdef (List.rev arityl) (Array.to_list nv) in
   let n = NeverDischarge in 
   if lnamerec <> [] then begin
-    let recvec = [|put_DLAMSV_subst (List.rev lnamerec)
-                       (Array.of_list ldefrec)|] in
+    let recvec = 
+      Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
     let varrec = Array.of_list (List.map incast_type larrec) in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
 	    { const_entry_body =
-		Cooked (mkFixDlam (Array.of_list nvrec) i varrec recvec);
+		Cooked 
+		  (mkFix ((Array.of_list nvrec,i),
+			  (varrec,List.map (fun id -> Name id) lnamerec,
+			   recvec)));
+		  (* (mkFixDlam (Array.of_list nvrec) i varrec recvec); *)
 	      const_entry_type = None } 
 	  in
 	  declare_constant fi (ce, n);
@@ -313,13 +310,15 @@ let build_corecursive lnameardef =
       if lnamerec = [] then 
 	[||] 
       else 
-	[|put_DLAMSV_subst (List.rev lnamerec) (Array.of_list ldefrec)|] 
-    in
+	Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
     let varrec = Array.of_list (List.map incast_type larrec) in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
-	    { const_entry_body = Cooked (mkCoFixDlam i varrec recvec);
+	    { const_entry_body =
+		Cooked 
+		  (mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec,
+			      recvec)));
 	      const_entry_type = None } 
 	  in
           declare_constant fi (ce,n);
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 3240e9db51..d136821a63 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -32,7 +32,12 @@ type modification_action = ABSTRACT | ERASE
 
 let interp_modif absfun oper (oper',modif) cl = 
   let rec interprec = function
-    | ([], cl) -> DOPN(oper',Array.of_list cl)
+    | ([], cl) -> 
+	(match oper' with
+	   | Const sp -> mkConst (sp,Array.of_list cl)
+	   | MutConstruct sp -> mkMutConstruct (sp,Array.of_list cl)
+	   | MutInd sp -> mkMutInd (sp,Array.of_list cl)
+	   | _ -> anomaly "not a reference operator")
     | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
     | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
     | _ -> assert false
@@ -64,10 +69,10 @@ let modify_opers replfun absfun oper_alist =
 	  (try
 	     match List.assoc (MutInd spi) oper_alist with
 	       | DO_ABSTRACT (MutInd spi',_) ->
-		   DOPN(MutCase(n,(spi',a,b,c,d)),cl')
+		   gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
 	       | _ -> raise Not_found
 	   with
-	     | Not_found -> DOPN(MutCase oper,cl'))
+	     | Not_found -> gather_constr (op,cl'))
 
       | OpMutInd spi ->
 	  (try
@@ -79,9 +84,9 @@ let modify_opers replfun absfun oper_alist =
 		    else 
 		      interp_modif absfun (MutInd spi) (oper',modif)
 			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (DOPN(MutInd spi,cl'))))
+		| DO_REPLACE -> assert false)
 	   with 
-	     | Not_found -> DOPN(MutInd spi,cl'))
+	     | Not_found -> mkMutInd (spi,cl'))
 
       | OpMutConstruct spi ->
 	  (try
@@ -93,9 +98,9 @@ let modify_opers replfun absfun oper_alist =
 		    else 
 		      interp_modif absfun (MutConstruct spi) (oper',modif)
 			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (DOPN(MutConstruct spi,cl'))))
+		| DO_REPLACE -> assert false)
 	   with 
-	     | Not_found -> DOPN(MutConstruct spi,cl'))
+	     | Not_found -> mkMutConstruct (spi,cl'))
 
       | OpConst sp ->
 	  (try
@@ -107,9 +112,9 @@ let modify_opers replfun absfun oper_alist =
 		    else 
 		      interp_modif absfun (Const sp) (oper',modif)
 			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (DOPN(Const sp,cl'))))
+		| DO_REPLACE -> substrec (replfun (sp,cl')))
 	   with 
-	     | Not_found -> DOPN(Const sp,cl'))
+	     | Not_found -> mkConst (sp,cl'))
   
     | _ -> gather_constr (op, cl')
   in 
@@ -117,18 +122,11 @@ let modify_opers replfun absfun oper_alist =
 
 (**)
 
-let under_dlams f = 
-  let rec apprec = function 
-    | DLAMV(na,c) -> DLAMV(na,Array.map f c)
-    | DLAM(na,c)  -> DLAM(na,apprec c)
-    | _           -> failwith "under_dlams"
-  in 
-  apprec 
-
 let abstract_inductive ids_to_abs hyps inds =
   let abstract_one_var d inds =
     let ntyp = List.length inds in 
-    let new_refs = list_tabulate (fun k -> applist(Rel (k+2),[Rel 1])) ntyp in 
+    let new_refs =
+      list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
     let inds' =
       List.map
       	(function (tname,arity,cnames,lc) -> 
@@ -191,8 +189,8 @@ let expmod_constr oldenv modlist c =
   let expfun cst = 
     try 
       constant_value oldenv cst
-    with Failure _ ->
-      let (sp,_) = destConst cst in
+    with NotEvaluableConst Opaque ->
+      let (sp,_) = cst in
       errorlabstrm "expmod_constr"
 	[< 'sTR"Cannot unfold the value of " ;
            'sTR(string_of_path sp) ; 'sPC;
@@ -200,13 +198,13 @@ let expmod_constr oldenv modlist c =
            'sTR"and then require that theorems which use them"; 'sPC;
            'sTR"be transparent" >];
   in
-  let under_casts f = function
-    | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t))
-    | c -> f c 
+  let under_casts f c = match kind_of_term c with
+    | IsCast (c,t) -> mkCast (f c,f t)
+    | _ -> f c 
   in
   let c' = modify_opers expfun (fun a b -> mkAppL (a, [|b|])) modlist c in
-  match c' with
-    | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ)
+  match kind_of_term c' with
+    | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
 let expmod_type oldenv modlist c = 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index cefa4d823d..773525ea43 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -268,7 +268,7 @@ let explain_occur_check k ctx ev rhs =
      'sTR" with term"; 'bRK(1,1); pt >]
 
 let explain_not_clean k ctx ev t =
-  let c = Rel (Intset.choose (free_rels t)) in
+  let c = mkRel (Intset.choose (free_rels t)) in
   let id = "?" ^ string_of_int ev in
   let var = prterm_env ctx c in
   [< 'sTR"Tried to define "; 'sTR id;
@@ -396,6 +396,9 @@ let explain_refiner_bad_tactic_args s l =
   [< 'sTR "Internal tactic "; 'sTR s; 'sTR " cannot be applied to ";
      Tacmach.pr_tactic (s,l) >]
 
+let explain_intro_needs_product () =
+  [< 'sTR "Introduction tactics needs products" >]
+
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
   | OccurMeta t -> explain_refiner_occur_meta t
@@ -404,6 +407,7 @@ let explain_refiner_error = function
   | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l
+  | IntroNeedsProduct -> explain_intro_needs_product ()
 
 let error_non_strictly_positive k env c v  =
   let pc = prterm_env env c in
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 7e2b1f5bd6..4305b61ce7 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -17,14 +17,13 @@ let (env : safe_environment ref) = ref empty_environment
 
 let lookup_var id =
   let rec look n = function
-    | [] -> VAR id
+    | [] -> mkVar id
     | (Name id')::_ when id = id' -> Rel n
     | _::r -> look (succ n) r
   in
   look 1
 
-let args sign = 
-  Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign))
+let args sign = Array.of_list (List.map mkVar (ids_of_var_context sign))
 
 let rec globalize bv c = match kind_of_term c with
   | IsVar id -> lookup_var id bv
@@ -36,26 +35,6 @@ let rec globalize bv c = match kind_of_term c with
       let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps)
   | _ -> map_constr_with_binders (fun na l -> na::l) globalize bv c
 
-(*
-let rec globalize bv = function
-  | VAR id -> lookup_var id bv
-  | DOP1 (op,c) -> DOP1 (op, globalize bv c)
-  | DOP2 (op,c1,c2) -> DOP2 (op, globalize bv c1, globalize bv c2)
-  | DOPN (Const sp as op, _) ->
-      let cb = lookup_constant sp !env in DOPN (op, args cb.const_hyps)
-  | DOPN (MutInd (sp,_) as op, _) ->
-      let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
-  | DOPN (MutConstruct ((sp,_),_) as op, _) ->
-      let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
-  | DOPN (op,v) -> DOPN (op, Array.map (globalize bv) v)
-  | DLAM (na,c) -> DLAM (na, globalize (na::bv) c)
-  | DLAMV (na,v) -> DLAMV (na, Array.map (globalize (na::bv)) v)
-  | CLam(n,t,c)   -> CLam (n, globalize bv t, globalize (n::bv) c)  
-  | CPrd(n,t,c)   -> CPrd (n, globalize bv t, globalize (n::bv) c)
-  | CLet(n,b,t,c) -> CLet (n,globalize bv b,globalize bv t,globalize (n::bv) c)
-  | Rel _ | DOP0 _ as c -> c
-*)
-
 let check c = 
   let c = globalize [] c in
   let (j,u) = safe_infer !env c in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index fbf2586525..faf1f34336 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -128,13 +128,13 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
            (None::sp_projs,fi::ids_not_ok,subst)
          end else 
 	   let p = mkLambda (x, rp2, replace_vars subst ti) in
-	   let branch = mk_LambdaCit newfs (VAR fi) in
+	   let branch = mk_LambdaCit newfs (mkVar fi) in
 	   let ci = Inductive.make_case_info
 		      (Global.lookup_mind_specif (destMutInd r))
 		      (Some PrintLet) [| RegularPat |] in
 	   let proj = mk_LambdaCit newps 
 			(mkLambda (x, rp1,
-				   mkMutCase (ci, p, Rel 1, [|branch|]))) in
+				   mkMutCase (ci, p, mkRel 1, [|branch|]))) in
 	   let ok = 
 	     try
 	       let cie =
@@ -152,7 +152,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
 	       Class.try_add_new_coercion_record fi NeverDischarge idstruc;
              let constr_fi = global_reference CCI fi in
              let constr_fip = (* Rel 1 refers to "x" *)
-               applist (constr_fi,(List.map (fun id -> VAR id) idps)@[Rel 1])
+               applist (constr_fi,(List.map mkVar idps)@[mkRel 1])
              in (Some(path_of_const constr_fi)::sp_projs,
 		 ids_not_ok, (fi,constr_fip)::subst)
 	   end)