Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.

14 files changed, 138 insertions, 169 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 17a488ddb..b548f8b92 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
       ( Proofview.Goal.enter { enter = begin fun gl ->
           let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
-          let nf c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) in
+          let nf c = Evarutil.nf_evar sigma c in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
           let hyp = Context.Named.Declaration.map_constr nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ef67d28f9..55fda1c7d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -521,14 +521,14 @@ let evars_to_goals p evm =
 (** Making local hints  *)
 let make_resolve_hyp env sigma st flags only_classes pri decl =
   let id = NamedDecl.get_id decl in
-  let cty = Evarutil.nf_evar sigma (EConstr.of_constr (NamedDecl.get_type decl)) in
+  let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
   let rec iscl env ty =
     let ctx, ar = decompose_prod_assum sigma ty in
       match EConstr.kind sigma (fst (decompose_app sigma ar)) with
       | Const (c,_) -> is_class (ConstRef c)
       | Ind (i,_) -> is_class (IndRef i)
       | _ ->
-          let env' = Environ.push_rel_context ctx env in
+          let env' = push_rel_context ctx env in
           let ty' = Reductionops.whd_all env' sigma ar in
                if not (EConstr.eq_constr sigma ty' ar) then iscl env' ty'
                else false
@@ -562,7 +562,7 @@ let make_hints g st only_classes sign =
         let consider =
           try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in
               (* Section variable, reindex only if the type changed *)
-              not (Term.eq_constr t (NamedDecl.get_type hyp))
+              not (EConstr.eq_constr (project g) (EConstr.of_constr t) (NamedDecl.get_type hyp))
           with Not_found -> true
         in
         if consider then
@@ -617,7 +617,7 @@ module V85 = struct
     then
       cached_hints
     else
-      let hints = make_hints g st only_classes (Environ.named_context_of_val sign)
+      let hints = make_hints g st only_classes (EConstr.named_context_of_val sign)
       in
       cache := (only_classes, sign, hints); hints
 
@@ -634,7 +634,7 @@ module V85 = struct
       let gls' =
         List.map (fun g' ->
             let env = Goal.V82.env s g' in
-            let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
+            let context = EConstr.named_context_of_val (Goal.V82.hyps s g') in
             let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
               (true,false,false) info.only_classes None (List.hd context) in
             let ldb = Hint_db.add_list env s hint info.hints in
@@ -937,9 +937,10 @@ module Search = struct
     let sign = Goal.hyps g in
     let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
     let cwd = Lib.cwd () in
+    let eq c1 c2 = EConstr.eq_constr (project g) c1 c2 in
     if DirPath.equal cwd dir &&
          (onlyc == only_classes) &&
-           Context.Named.equal Constr.equal sign sign' &&
+           Context.Named.equal eq sign sign' &&
              Hint_db.transparent_state cached_hints == st
     then cached_hints
     else
@@ -1033,8 +1034,9 @@ module Search = struct
           Feedback.msg_debug
             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
                pr_ev s' (Proofview.Goal.goal gl'));
+        let eq c1 c2 = EConstr.eq_constr s' c1 c2 in
         let hints' =
-          if b && not (Context.Named.equal Constr.equal (Goal.hyps gl') (Goal.hyps gl))
+          if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
           then
             let st = Hint_db.transparent_state info.search_hints in
             make_autogoal_hints info.search_only_classes ~st gl'
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 7173fb4fd..0e28aa980 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -51,7 +51,7 @@ let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5
 let filter_hyp f tac =
   let rec seek = function
     | [] -> Proofview.tclZERO Not_found
-    | d::rest when f (EConstr.of_constr (NamedDecl.get_type d)) -> tac (NamedDecl.get_id d)
+    | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
     | _::rest -> seek rest in
   Proofview.Goal.enter { enter = begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
@@ -66,7 +66,7 @@ let contradiction_context =
       | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | d :: rest ->
           let id = NamedDecl.get_id d in
-          let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in
+          let typ = nf_evar sigma (NamedDecl.get_type d) in
 	  let typ = whd_all env sigma typ in
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 072da995d..122b64777 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -13,12 +13,12 @@ open Names
 open Nameops
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
 open Inductive
 open Inductiveops
-open Environ
 open Libnames
 open Globnames
 open Reductionops
@@ -47,10 +47,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-let nlocal_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  NamedDecl.LocalAssum (na, inj t)
-
 (* Options *)
 
 let discriminate_introduction = ref true
@@ -333,7 +329,7 @@ let jmeq_same_dom gl = function
   | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
   | Some t ->
     let rels, t = decompose_prod_assum (project gl) t in
-    let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
+    let env = push_rel_context rels (Proofview.Goal.env gl) in
     match decompose_app (project gl) t with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
@@ -857,16 +853,19 @@ let descend_then env sigma head dirn =
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
-  let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in
+  let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
       let deparsign = make_arity_signature env true indf in
+      let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	it_mkLambda_or_LetIn result (name_context env cstr.(i-1).cs_args) in
+	let args = name_context env cstr.(i-1).cs_args in
+	let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in
+	it_mkLambda_or_LetIn result args in
       let brl =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
@@ -907,11 +906,13 @@ let build_selector env sigma dirn c ind special default =
   let typ = Retyping.get_type_of env sigma default in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
+  let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
   let p = it_mkLambda_or_LetIn typ deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
     let endpt = if Int.equal i dirn then special else default in
-    it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
+    let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstrs.(i-1).cs_args in
+    it_mkLambda_or_LetIn endpt args in
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
@@ -995,7 +996,7 @@ let apply_on_clause (f,t) clause =
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (nlocal_assum (e, t)) env in
+  let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
   let discriminator =
     build_discriminator e_env sigma dirn (mkVar e) cpath in
   let sigma,(pf, absurd_term), eff = 
@@ -1372,7 +1373,7 @@ let simplify_args env sigma t =
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (nlocal_assum (e,t)) env in
+  let e_env = push_named (LocalAssum (e,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
@@ -1696,7 +1697,7 @@ let is_eq_x gl x d =
     | Var id' -> Id.equal id id'
     | _ -> false
     in
-    let c = pf_nf_evar gl (EConstr.of_constr (NamedDecl.get_type d)) in
+    let c = pf_nf_evar gl (NamedDecl.get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
     if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
     if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1793,7 +1794,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let select_equation_name decl =
       try
-        let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in
+        let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
@@ -1817,7 +1818,6 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
-    let c = EConstr.of_constr c in
     let _,_,(_,x,y) = find_eq_data_decompose c in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
@@ -1890,7 +1890,7 @@ let rewrite_assumption_cond cond_eq_term cl =
         let id = NamedDecl.get_id hyp in
 	begin
 	  try
-            let dir = cond_eq_term (EConstr.of_constr (NamedDecl.get_type hyp)) gl in
+            let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
 	    general_rewrite_clause dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ef97b0b33..ffd19ac6e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -875,7 +875,7 @@ let make_resolve_hyp env sigma decl =
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (c, EConstr.of_constr (NamedDecl.get_type decl), Univ.ContextSet.empty)]
+       (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
@@ -1335,7 +1335,7 @@ let make_local_hint_db env sigma ts eapply lems =
     (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
-  let sign = Environ.named_context env in
+  let sign = EConstr.named_context env in
   let ts = match ts with
     | None -> Hint_db.transparent_state (searchtable_map "core") 
     | Some ts -> ts
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 344827e03..0d6dd434e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -29,7 +29,7 @@ val decompose_app_bound : evar_map -> constr -> global_reference * constr array
 
 type debug = Debug | Info | Off
 
-val secvars_of_hyps : Context.Named.t -> Id.Pred.t
+val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
 
 (** Pre-created hint databases *)
 
@@ -209,7 +209,7 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp :
-  env -> evar_map -> Context.Named.Declaration.t -> hint_entry list
+  env -> evar_map -> named_declaration -> hint_entry list
 
 (** [make_extern pri pattern tactic_expr] *)
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 607d6d2a9..8e4654c02 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -107,8 +107,8 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
 	    List.for_all
 	      (fun decl -> let c = RelDecl.get_type decl in
 	                   is_local_assum decl &&
-			   Term.isRel c &&
-                           Int.equal (Term.destRel c) mib.mind_nparams) ctx
+			   isRel sigma c &&
+                           Int.equal (destRel sigma c) mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
@@ -117,7 +117,6 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
-	    let cargs = List.map EConstr.of_constr cargs in
 	    Some (hdapp,List.rev cargs)
 	  else
 	      None
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 426749a75..ecb8eedac 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,10 +13,10 @@ open Names
 open Nameops
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
-open Environ
 open Inductiveops
 open Printer
 open Retyping
@@ -75,6 +75,7 @@ let make_inv_predicate env evd indf realargs id status concl =
       | NoDep ->
 	  (* We push the arity and leave concl unchanged *)
 	  let hyps_arity,_ = get_arity env indf in
+	  let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in
 	    (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (occur_var env !evd id concl) then
@@ -132,6 +133,10 @@ let make_inv_predicate env evd indf realargs id status concl =
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
+  let name_context env ctx =
+    let map f c = List.map (fun d -> Termops.map_rel_decl f d) c in
+    map EConstr.of_constr (name_context env (map EConstr.Unsafe.to_constr ctx))
+  in
   let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in
   let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a05b4fbf3..d7c396179 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
@@ -20,7 +21,6 @@ open Printer
 open Reductionops
 open Entries
 open Inductiveops
-open Environ
 open Tacmach.New
 open Clenv
 open Declare
@@ -32,14 +32,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-let nlocal_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  NamedDecl.LocalAssum (na, inj t)
-
-let nlocal_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  NamedDecl.LocalDef (na, inj b, inj t)
-
 let no_inductive_inconstr env sigma constr =
   (str "Cannot recognize an inductive predicate in " ++
      pr_leconstr_env env sigma constr ++
@@ -129,11 +121,11 @@ let rec add_prods_sign env sigma t =
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (nlocal_assum (id,c1)) env) sigma b'
+        add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
 	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (nlocal_def (id,c1,t1)) env) sigma b'
+        add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates whether the inversion lemma is dependent or not.
@@ -168,6 +160,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let revargs,ownsign =
 	fold_named_context
 	  (fun env d (revargs,hyps) ->
+            let d = map_named_decl EConstr.of_constr d in
              let id = NamedDecl.get_id d in
              if Id.List.mem id ivars then
 	       ((mkVar id)::revargs, Context.Named.add d hyps)
@@ -180,7 +173,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_all env sigma pty in
-  let extenv = push_named (nlocal_assum (p,npty)) env in
+  let extenv = push_named (LocalAssum (p,npty)) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -218,6 +211,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ownSign = ref begin
     fold_named_context
       (fun env d sign ->
+        let d = map_named_decl EConstr.of_constr d in
          if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
 	 else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
@@ -231,7 +225,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
-	ownSign := Context.Named.add (nlocal_assum (h,ty)) !ownSign;
+	ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign;
 	applist (mkVar h, inst)
     | _ -> EConstr.map sigma fill_holes c
   in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9cf3c4187..94f22f903 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -158,7 +158,7 @@ type branch_args = {
 
 type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
-  assums    : Context.Named.t}   (* the list of assumptions introduced *)
+  assums    : named_context}   (* the list of assumptions introduced *)
 
 open Misctypes
 
@@ -625,7 +625,6 @@ module New = struct
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
       isrec allnames tac predicate ind (c, t) =
-    let open EConstr in
     Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2b07d937e..e9f623100 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -60,29 +60,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
 val onNthHypId       : int -> (Id.t -> tactic) -> tactic
 val onNthHyp         : int -> (constr -> tactic) -> tactic
-val onNthDecl        : int -> (Context.Named.Declaration.t -> tactic) -> tactic
+val onNthDecl        : int -> (named_declaration -> tactic) -> tactic
 val onLastHypId      : (Id.t -> tactic) -> tactic
 val onLastHyp        : (constr -> tactic) -> tactic
-val onLastDecl       : (Context.Named.Declaration.t -> tactic) -> tactic
+val onLastDecl       : (named_declaration -> tactic) -> tactic
 val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
 val onNLastHyps      : int -> (constr list -> tactic) -> tactic
-val onNLastDecls     : int -> (Context.Named.t -> tactic) -> tactic
+val onNLastDecls     : int -> (named_context -> tactic) -> tactic
 
 val lastHypId   : goal sigma -> Id.t
 val lastHyp     : goal sigma -> constr
-val lastDecl    : goal sigma -> Context.Named.Declaration.t
+val lastDecl    : goal sigma -> named_declaration
 val nLastHypsId : int -> goal sigma -> Id.t list
 val nLastHyps   : int -> goal sigma -> constr list
-val nLastDecls  : int -> goal sigma -> Context.Named.t
+val nLastDecls  : int -> goal sigma -> named_context
 
-val afterHyp    : Id.t -> goal sigma -> Context.Named.t
+val afterHyp    : Id.t -> goal sigma -> named_context
 
 val ifOnHyp     : (Id.t * types -> bool) ->
                   (Id.t -> tactic) -> (Id.t -> tactic) ->
 		   Id.t -> tactic
 
-val onHyps      : (goal sigma -> Context.Named.t) ->
-                  (Context.Named.t -> tactic) -> tactic
+val onHyps      : (goal sigma -> named_context) ->
+                  (named_context -> tactic) -> tactic
 
 (** {6 Tacticals applying to goal components } *)
 
@@ -110,7 +110,7 @@ type branch_args = private {
 
 type branch_assumptions = private {
   ba        : branch_args;       (** the branch args *)
-  assums    : Context.Named.t}   (** the list of assumptions introduced *)
+  assums    : named_context}   (** the list of assumptions introduced *)
 
 (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate
    error message if |pats| <> |branchsign|; extends them if no pattern is given
@@ -229,7 +229,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
+  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
@@ -238,11 +238,11 @@ module New : sig
   val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
   val onLastHypId      : (identifier -> unit tactic) -> unit tactic
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
-  val onLastDecl       : (Context.Named.Declaration.t -> unit tactic) -> unit tactic
+  val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `NF ], Context.Named.t) Proofview.Goal.enter ->
-                    (Context.Named.t -> unit tactic) -> unit tactic
-  val afterHyp    : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic
+  val onHyps      : ([ `NF ], named_context) Proofview.Goal.enter ->
+                    (named_context -> unit tactic) -> unit tactic
+  val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
   val tryAllHyps          : (identifier -> unit tactic) -> unit tactic
   val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8260c14ad..4bf848a9c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -15,6 +15,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Find_subterm
@@ -22,7 +23,6 @@ open Namegen
 open Declarations
 open Inductiveops
 open Reductionops
-open Environ
 open Globnames
 open Evd
 open Pfedit
@@ -170,26 +170,6 @@ let _ =
 (*           Primitive tactics            *)
 (******************************************)
 
-let local_assum (na, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
-let nlocal_assum (na, t) =
-  let open Context.Named.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let nlocal_def (na, b, t) =
-  let open Context.Named.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
 let unsafe_intro env store decl b =
@@ -217,8 +197,8 @@ let introduction ?(check=true) id =
     in
     let open Context.Named.Declaration in
     match EConstr.kind sigma concl with
-    | Prod (_, t, b) -> unsafe_intro env store (nlocal_assum (id, t)) b
-    | LetIn (_, c, t, b) -> unsafe_intro env store (nlocal_def (id, c, t)) b
+    | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
+    | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
     | _ -> raise (RefinerError IntroNeedsProduct)
   end }
 
@@ -321,7 +301,6 @@ let clear_gen fail = function
       try clear_hyps_in_evi env evdref (named_context_val env) concl ids
       with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
     in
-    let concl = EConstr.of_constr concl in
     let env = reset_with_named_context hyps env in
     let tac = Refine.refine ~unsafe:true { run = fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
@@ -397,18 +376,16 @@ let rename_hyp repl =
         with Not_found -> ()
       in
       (** All is well *)
-      let make_subst (src, dst) = (src, Constr.mkVar dst) in
+      let make_subst (src, dst) = (src, mkVar dst) in
       let subst = List.map make_subst repl in
-      let subst c = CVars.replace_vars subst c in
+      let subst c = Vars.replace_vars subst c in
       let map decl =
         decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
              |> NamedDecl.map_constr subst
       in
       let nhyps = List.map map hyps in
-      let concl = EConstr.Unsafe.to_constr concl in
       let nconcl = subst concl in
-      let nconcl = EConstr.of_constr nconcl in
-      let nctx = Environ.val_of_named_context nhyps in
+      let nctx = val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~unsafe:true { run = begin fun sigma ->
         Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
@@ -435,11 +412,14 @@ let id_of_name_with_default id = function
 let default_id_of_sort s =
   if Sorts.is_small s then default_small_ident else default_type_ident
 
+let id_of_name_using_hdchar env c name =
+  id_of_name_using_hdchar env (EConstr.Unsafe.to_constr c) name
+
 let default_id env sigma decl =
   let open Context.Rel.Declaration in
   match decl with
   | LocalAssum (name,t) ->
-      let dft = default_id_of_sort (Retyping.get_sort_of env sigma (EConstr.of_constr t)) in
+      let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
       id_of_name_with_default dft name
   | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name
 
@@ -478,7 +458,7 @@ let find_name mayrepl decl naming gl = match naming with
 let assert_before_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let id = find_name b (local_assum (Anonymous,t)) naming gl in
+    let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
     Tacticals.New.tclTHENLAST
       (Proofview.V82.tactic
          (fun gl ->
@@ -497,7 +477,7 @@ let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
 let assert_after_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let id = find_name b (local_assum (Anonymous,t)) naming gl in
+    let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
     Tacticals.New.tclTHENFIRST
       (Proofview.V82.tactic
          (fun gl ->
@@ -534,7 +514,7 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
     with Not_found -> error "Cannot do a fixpoint on a non inductive type."
   else
     let open Context.Rel.Declaration in
-    check_mutind (push_rel (local_assum (na, c1)) env) sigma (pred k) b
+    check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
 | _ -> error "Not enough products."
 
 (* Refine as a fixpoint *)
@@ -548,13 +528,14 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
   let rec mk_sign sign = function
   | [] -> sign
   | (f, n, ar) :: oth ->
+    let open Context.Named.Declaration in
     let (sp', u')  = check_mutind env sigma n ar in
     if not (eq_mind sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
         (str "Name " ++ pr_id f ++ str " already used in the environment");
-    mk_sign (push_named_context_val (nlocal_assum (f, ar)) sign) oth
+    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine { run = begin fun sigma ->
@@ -584,7 +565,8 @@ let rec check_is_mutcoind env sigma cl =
   let b = whd_all env sigma cl in
   match EConstr.kind sigma b with
   | Prod (na, c1, b) ->
-    check_is_mutcoind (push_rel (local_assum (na,c1)) env) sigma b
+    let open Context.Rel.Declaration in
+    check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b
   | _ ->
     try
       let _ = find_coinductive env sigma b in ()
@@ -602,9 +584,10 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
   let rec mk_sign sign = function
   | [] -> sign
   | (f, ar) :: oth ->
+    let open Context.Named.Declaration in
     if mem_named_context_val f sign then
       error "Name already used in the environment.";
-    mk_sign (push_named_context_val (nlocal_assum (f, ar)) sign) oth
+    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine { run = begin fun sigma ->
@@ -640,16 +623,13 @@ let pf_reduce_decl redfun where decl gl =
   let redfun' c = Tacmach.New.pf_apply redfun gl c in
   match decl with
   | LocalAssum (id,ty) ->
-      let ty = EConstr.of_constr ty in
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
-      nlocal_assum (id,redfun' ty)
+      LocalAssum (id,redfun' ty)
   | LocalDef (id,b,ty) ->
-      let b = EConstr.of_constr b in
-      let ty = EConstr.of_constr ty in
       let b' = if where != InHypTypeOnly then redfun' b else b in
       let ty' =	if where != InHypValueOnly then redfun' ty else ty in
-      nlocal_def (id,b',ty')
+      LocalDef (id,b',ty')
 
 (* Possibly equip a reduction with the occurrences mentioned in an
    occurrence clause *)
@@ -744,17 +724,14 @@ let pf_e_reduce_decl redfun where decl gl =
   let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in
   match decl with
   | LocalAssum (id,ty) ->
-      let ty = EConstr.of_constr ty in
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = redfun sigma ty in
-    Sigma (nlocal_assum (id, ty'), sigma, p)
+    Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
-      let b = EConstr.of_constr b in
-      let ty = EConstr.of_constr ty in
       let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in
       let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in
-      Sigma (nlocal_def (id, b', ty'), sigma, p +> q)
+      Sigma (LocalDef (id, b', ty'), sigma, p +> q)
 
 let e_reduct_in_concl ~check (redfun, sty) =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
@@ -787,21 +764,18 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   let open Context.Named.Declaration in
   match decl with
   | LocalAssum (id,ty) ->
-      let ty = EConstr.of_constr ty in
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
-    Sigma (nlocal_assum (id, ty'), sigma, p)
+    Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
-      let b = EConstr.of_constr b in
-      let ty = EConstr.of_constr ty in
       let Sigma (b', sigma, p) =
 	if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma
       in
       let Sigma (ty', sigma, q) =
 	if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma
       in
-      Sigma (nlocal_def (id,b',ty'), sigma, p +> q)
+      Sigma (LocalDef (id,b',ty'), sigma, p +> q)
 
 let e_change_in_hyp redfun (id,where) =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -974,10 +948,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     match EConstr.kind sigma concl with
     | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
-        let name = find_name false (local_assum (name,t)) name_flag gl in
+        let name = find_name false (LocalAssum (name,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
-        let name = find_name false (local_def (name,b,t)) name_flag gl in
+        let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | _ ->
 	begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
@@ -1382,11 +1356,11 @@ let enforce_prop_bound_names rename tac =
                 Name (add_suffix Namegen.default_prop_ident s)
               else
                 na in
-            mkProd (na,t,aux (push_rel (local_assum (na,t)) env) sigma (i-1) t')
+            mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t')
         | Prod (Anonymous,t,t') ->
-            mkProd (Anonymous,t,aux (push_rel (local_assum (Anonymous,t)) env) sigma (i-1) t')
+            mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t')
         | LetIn (na,c,t,t') ->
-            mkLetIn (na,c,t,aux (push_rel (local_def (na,c,t)) env) sigma (i-1) t')
+            mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
         | _ -> assert false in
       let rename_branch i =
         Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -1619,11 +1593,11 @@ let make_projection env sigma params cstr sign elim i n c u =
   let elim = match elim with
   | NotADefinedRecordUseScheme elim ->
       (* bugs: goes from right to left when i increases! *)
-      let decl = List.nth cstr.cs_args i in
+      let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.cs_args in
+      let decl = List.nth cs_args i in
       let t = RelDecl.get_type decl in
-      let t = EConstr.of_constr t in
-      let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> EConstr.of_constr b in
-      let branch = it_mkLambda_or_LetIn b cstr.cs_args in
+      let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in
+      let branch = it_mkLambda_or_LetIn b cs_args in
       if
 	(* excludes dependent projection types *)
 	noccur_between sigma 1 (n-i-1) t
@@ -1890,7 +1864,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
   let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
-  let targetid = find_name true (local_assum (Anonymous,t')) naming gl in
+  let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
   let rec aux idstoclear with_destruct c =
     Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -2017,7 +1991,6 @@ let assumption =
     else Tacticals.New.tclZEROMSG (str "No such assumption.")
   | decl::rest ->
     let t = NamedDecl.get_type decl in
-    let t = EConstr.of_constr t in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let (sigma, is_same_type) =
@@ -2058,13 +2031,13 @@ let check_is_type env sigma ty =
 
 let check_decl env sigma decl =
   let open Context.Named.Declaration in
-  let ty = EConstr.of_constr (NamedDecl.get_type decl) in
+  let ty = NamedDecl.get_type decl in
   let evdref = ref sigma in
   try
     let _ = Typing.e_sort_of env evdref ty in
     let _ = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,c,_) -> Typing.e_check env evdref (EConstr.of_constr c) ty
+    | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
     in
     !evdref
   with e when CErrors.noncritical e ->
@@ -2146,6 +2119,7 @@ let keep hyps =
   let sigma = Tacmach.New.project gl in
   let cl,_ =
     fold_named_context_reverse (fun (clear,keep) decl ->
+      let decl = map_named_decl EConstr.of_constr decl in
       let hyp = NamedDecl.get_id decl in
       if Id.List.mem hyp hyps
         || List.exists (occur_var_in_decl env sigma hyp) keep
@@ -2692,6 +2666,7 @@ let insert_before decls lasthyp env =
   | Some id ->
   Environ.fold_named_context
     (fun _ d env ->
+      let d = map_named_decl EConstr.of_constr d in
       let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in
       push_named d env)
     ~init:(reset_context env) env
@@ -2701,8 +2676,8 @@ let insert_before decls lasthyp env =
 let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
   let open Context.Named.Declaration in
   let t = match ty with Some t -> t | _ -> typ_of env sigma c in
-  let decl = if dep then nlocal_def (id,c,t)
-	     else nlocal_assum (id,t)
+  let decl = if dep then LocalDef (id,c,t)
+	     else LocalAssum (id,t)
   in
   match with_eq with
   | Some (lr,(loc,ido)) ->
@@ -2721,7 +2696,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let refl = EConstr.of_constr refl in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
-      let newenv = insert_before [nlocal_assum (heq,eq); decl] lastlhyp env in
+      let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
       let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in
       Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r)
   | None ->
@@ -2822,8 +2797,8 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name sigma c t ids cl' na in
   let decl = match b with
-    | None -> local_assum (na,t)
-    | Some b -> local_def (na,b,t)
+    | None -> LocalAssum (na,t)
+    | Some b -> LocalDef (na,b,t)
   in
   mkProd_or_LetIn decl cl', sigma'
 
@@ -2838,7 +2813,7 @@ let old_generalize_dep ?(with_let=false) c gl =
   let sign = pf_hyps gl in
   let sigma = project gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
-  let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) =
+  let seek (d:named_declaration) (toquant:named_context) =
     if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant
       || dependent_in_decl sigma c d then
       d::toquant
@@ -2862,7 +2837,6 @@ let old_generalize_dep ?(with_let=false) c gl =
       | _ -> None
     else None
   in
-  let body = Option.map EConstr.of_constr body in
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
   (** Check that the generalization is indeed well-typed *)
@@ -3256,7 +3230,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             | Var id -> id
             | _ ->
             let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in
+            id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
@@ -3342,6 +3316,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
   let before = ref true in
   let maindep = ref false in
   let seek_deps env decl rhyp =
+    let decl = map_named_decl EConstr.of_constr decl in
     let hyp = NamedDecl.get_id decl in
     if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false)
     then begin
@@ -3434,15 +3409,15 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  params: Context.Rel.t;      (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  params: rel_context;      (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;               (* number of parameters *)
-  predicates: Context.Rel.t;  (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  predicates: rel_context;  (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
   npredicates: int;           (* Number of predicates *)
-  branches: Context.Rel.t;    (* branchr,...,branch1 *)
+  branches: rel_context;    (* branchr,...,branch1 *)
   nbranches: int;             (* Number of branches *)
-  args: Context.Rel.t;        (* (xni, Ti_ni) ... (x1, Ti_1) *)
+  args: rel_context;        (* (xni, Ti_ni) ... (x1, Ti_1) *)
   nargs: int;                 (* number of arguments *)
-  indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni)
+  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
                                                if HI is in premisses, None otherwise *)
   concl: types;               (* Qi x1...xni HI (f...), HI and (f...)
 			         are optional and mutually exclusive *)
@@ -3586,10 +3561,10 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   in
     (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
-  let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> local_assum (Anonymous, x)) eqs) in
+  let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> LocalAssum (Anonymous, x)) eqs) in
   let decl = match body with
-    | None -> local_assum (Name id, c)
-    | Some body -> local_def (Name id, body, c)
+    | None -> LocalAssum (Name id, c)
+    | Some body -> LocalDef (Name id, body, c)
   in
     (* Abstract by the "generalized" hypothesis. *)
   let genarg = mkProd_or_LetIn decl abseqs in
@@ -3668,7 +3643,6 @@ let abstract_args gl generalize_vars dep id defined f args =
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_type decl, c
     in
-    let ty = EConstr.of_constr ty in
     let argty = Tacmach.pf_unsafe_type_of gl arg in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
     let () = sigma := sigma' in
@@ -3681,7 +3655,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       	  Id.Set.add id nongenvars, Id.Set.remove id vars, env)
       | _ ->
 	  let name = get_id name in
-	  let decl = local_assum (Name name, ty) in
+	  let decl = LocalAssum (Name name, ty) in
 	  let ctx = decl :: ctx in
 	  let c' = mkApp (lift 1 c, [|mkRel 1|]) in
 	  let args = arg :: args in
@@ -3739,10 +3713,9 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   let (f, args, def, id, oldid) =
     let oldid = Tacmach.New.pf_get_new_id id gl in
       match Tacmach.New.pf_get_hyp id gl with
-      | LocalAssum (_,t) -> let f, args = decompose_app sigma (EConstr.of_constr t) in
+      | LocalAssum (_,t) -> let f, args = decompose_app sigma t in
 	        (f, args, false, id, oldid)
       | LocalDef (_,t,_) ->
-          let t = EConstr.of_constr t in
 	  let f, args = decompose_app sigma t in
 	  (f, args, true, id, oldid)
   in
@@ -3809,13 +3782,13 @@ let specialize_eqs id gl =
 	    if in_eqs then acc, in_eqs, ctx, ty
 	    else
 	      let e = e_new_evar (push_rel_context ctx env) evars t in
-		aux false (local_def (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+		aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
     | t -> acc, in_eqs, ctx, ty
   in
   let acc, worked, ctx, ty = aux false [] (mkVar id) ty in
   let ctx' = nf_rel_context_evar !evars ctx in
   let ctx'' = List.map (function
-    | LocalDef (n,k,t) when isEvar !evars (EConstr.of_constr k) -> LocalAssum (n,t)
+    | LocalDef (n,k,t) when isEvar !evars k -> LocalAssum (n,t)
     | decl -> decl) ctx'
   in
   let ty' = it_mkProd_or_LetIn ty ctx'' in
@@ -3855,13 +3828,13 @@ let decompose_paramspred_branch_args sigma elimt =
       | Prod(nme,tpe,elimt') ->
 	  let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in
 	  if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe
-	  then cut_noccur elimt' (local_assum (nme,tpe)::acc2)
+	  then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2)
 	  else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl
       | App(_, _) | Rel _ -> acc2 , [] , elimt
       | _ -> error_ind_scheme "" in
   let rec cut_occur elimt acc1 =
     match EConstr.kind sigma elimt with
-      | Prod(nme,tpe,c) when occur_rel sigma 1 c -> cut_occur c (local_assum (nme,tpe)::acc1)
+      | Prod(nme,tpe,c) when occur_rel sigma 1 c -> cut_occur c (LocalAssum (nme,tpe)::acc1)
       | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
       | App(_, _) | Rel _ -> acc1,[],[],elimt
       | _ -> error_ind_scheme "" in
@@ -3939,7 +3912,6 @@ let compute_elim_sig sigma ?elimc elimt =
       match List.hd args_indargs with
 	| LocalDef (hiname,_,hi) -> error_ind_scheme ""
 	| LocalAssum (hiname,hi) ->
-            let hi = EConstr.of_constr hi in
 	    let hi_ind, hi_args = decompose_app sigma hi in
 	    let hi_is_ind = (* hi est d'un type globalisable *)
 	      match EConstr.kind sigma hi_ind with
@@ -3965,7 +3937,6 @@ let compute_elim_sig sigma ?elimc elimt =
       | None -> !res (* No indref *)
       | Some (LocalDef _) -> error_ind_scheme ""
       | Some (LocalAssum (_,ind)) ->
-          let ind = EConstr.of_constr ind in
 	  let indhd,indargs = decompose_app sigma ind in
 	  try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) }
 	  with e when CErrors.noncritical e ->
@@ -3983,7 +3954,6 @@ let compute_scheme_signature evd scheme names_info ind_type_guess =
 	  let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl
 	  in (cond, fun _ _ -> ())
       | Some (LocalAssum (_,ind)) -> (* Standard scheme from an inductive type *)
-          let ind = EConstr.of_constr ind in
 	  let indhd,indargs = decompose_app evd ind in
 	  let cond hd = EConstr.eq_constr evd hd indhd in
 	  let check_concl is_pred p =
@@ -4016,7 +3986,6 @@ let compute_scheme_signature evd scheme names_info ind_type_guess =
   let rec find_branches p lbrch =
     match lbrch with
       | LocalAssum (_,t) :: brs ->
-        let t = EConstr.of_constr t in
 	(try
 	   let lchck_brch = check_branch p t in
 	   let n = List.fold_left
@@ -4123,7 +4092,7 @@ let get_eliminator elim dep s gl =
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
       let _, (l, s) = compute_elim_signature elims id in
-      let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (EConstr.of_constr (RelDecl.get_type d))))
+      let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
                                     (List.rev s.branches)
       in
       evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
@@ -4465,7 +4434,6 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
-      let t = EConstr.Unsafe.to_constr t in
       let x = id_of_name_using_hdchar (Global.env()) t Anonymous in
       new_fresh_id [] x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
@@ -4503,7 +4471,7 @@ let induction_gen_l isrec with_evars elim names lc =
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let sigma = Tacmach.New.project gl in
                 let x =
-		  id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in
+		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
                 let id = new_fresh_id [] x gl in
 		let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
@@ -4863,6 +4831,9 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
 (** d1 is the section variable in the global context, d2 in the goal context *)
 let interpretable_as_section_decl evd d1 d2 =
   let open Context.Named.Declaration in
+  let e_eq_constr_univs sigma c1 c2 =
+    e_eq_constr_univs sigma (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2)
+  in
   match d2, d1 with
   | LocalDef _, LocalAssum _ -> false
   | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b0d9dcb1c..0087d607d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -35,9 +35,9 @@ val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool
 
 val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp     : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic
+val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
+val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t option -> int -> unit Proofview.tactic
@@ -51,7 +51,7 @@ val convert_leq     : constr -> constr -> unit Proofview.tactic
 
 val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
 val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
-val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list
+val find_intro_names : rel_context -> goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
@@ -185,7 +185,7 @@ val revert        : Id.t list -> unit Proofview.tactic
 (** {6 Resolution tactics. } *)
 
 val apply_type : constr -> constr list -> unit Proofview.tactic
-val bring_hyps : Context.Named.t -> unit Proofview.tactic
+val bring_hyps : named_context -> unit Proofview.tactic
 
 val apply                 : constr -> unit Proofview.tactic
 val eapply                : constr -> unit Proofview.tactic
@@ -244,15 +244,15 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  params: Context.Rel.t;      (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  params: rel_context;      (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;               (** number of parameters *)
-  predicates: Context.Rel.t;  (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  predicates: rel_context;  (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
   npredicates: int;           (** Number of predicates *)
-  branches: Context.Rel.t;    (** branchr,...,branch1 *)
+  branches: rel_context;    (** branchr,...,branch1 *)
   nbranches: int;             (** Number of branches *)
-  args: Context.Rel.t;        (** (xni, Ti_ni) ... (x1, Ti_1) *)
+  args: rel_context;        (** (xni, Ti_ni) ... (x1, Ti_1) *)
   nargs: int;                 (** number of arguments *)
-  indarg: Context.Rel.Declaration.t option;  (** Some (H,I prm1..prmp x1...xni)
+  indarg: rel_declaration option;  (** Some (H,I prm1..prmp x1...xni)
 	  		 	                 if HI is in premisses, None otherwise *)
   concl: types;               (** Qi x1...xni HI (f...), HI and (f...)
 			          are optional and mutually exclusive *)
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 219abb7fd..2c863c42a 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -344,7 +344,7 @@ struct
     ) (pr_dconstr pr_term_pattern) p*)
 
   let search_pat cpat dpat dn =
-    let whole_c = cpat in
+    let whole_c = EConstr.of_constr cpat in
     (* if we are at the root, add an empty context *)
     let dpat = under_prod (empty_ctx dpat) in
     TDnet.Idset.fold
@@ -352,9 +352,8 @@ struct
 	 let c_id = Opt.reduce (Ident.constr_of id) in
 	 let c_id = EConstr.of_constr c_id in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) c_id (** FIXME *)
+	   try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *)
 	   with Invalid_argument _ -> [],c_id in
-          let wc = EConstr.Unsafe.to_constr wc in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
           let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in