Merge PR#379: Introducing evar-insensitive constrs

20 files changed, 452 insertions, 371 deletions

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index c5b26e6d5..5d3f6df03 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -7,6 +7,9 @@
 (************************************************************************)
 
 open Util
+open Names
+open Term
+open EConstr
 open CErrors
 open Evar_refiner
 open Tacmach
@@ -35,25 +38,32 @@ let instantiate_evar evk (ist,rawc) sigma =
   let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in
   tclEVARS sigma'
 
+let evar_list sigma c =
+  let rec evrec acc c =
+    match EConstr.kind sigma c with
+    | Evar (evk, _ as ev) -> ev :: acc
+    | _ -> EConstr.fold sigma evrec acc c in
+  evrec [] c
+
 let instantiate_tac n c ido =
   Proofview.V82.tactic begin fun gl ->
   let sigma = gl.sigma in
   let evl =
     match ido with
-	ConclLocation () -> evar_list (pf_concl gl)
+	ConclLocation () -> evar_list sigma (pf_concl gl)
       | HypLocation (id,hloc) ->
 	  let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in
 	    match hloc with
 		InHyp ->
 		  (match decl with
-                    | LocalAssum (_,typ) -> evar_list typ
+                    | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
 		    | _ -> error
 			"Please be more specific: in type or value?")
 	      | InHypTypeOnly ->
-		  evar_list (NamedDecl.get_type decl)
+		  evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
 	      | InHypValueOnly ->
 		  (match decl with
-		    | LocalDef (_,body,_) -> evar_list body
+		    | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
 		    | _ -> error "Not a defined hypothesis.") in
   if List.length evl < n then
     error "Not enough uninstantiated existential variables.";
@@ -78,16 +88,32 @@ let let_evar name typ =
     let env = Proofview.Goal.env gl in
     let sigma = ref sigma in
     let _ = Typing.e_sort_of env sigma typ in
-    let sigma = Sigma.Unsafe.of_evar_map !sigma in
+    let sigma = !sigma in
     let id = match name with
     | Names.Anonymous -> 
-      let id = Namegen.id_of_name_using_hdchar env typ name in
+      let id = Namegen.id_of_name_using_hdchar env sigma typ name in
       Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
     | Names.Name id -> id
     in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
     let tac =
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
     in
     Sigma (tac, sigma, p)
   end }
+
+let hget_evar n =
+  let open EConstr in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let sigma = Tacmach.New.project gl in
+  let concl = Proofview.Goal.concl gl in
+  let evl = evar_list sigma concl in
+  if List.length evl < n then
+    error "Not enough uninstantiated existential variables.";
+  if n <= 0 then error "Incorrect existential variable index.";
+  let ev = List.nth evl (n-1) in
+  let ev_type = EConstr.existential_type sigma ev in
+  Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
+  end }
+
diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli
index e67540c05..cfe747665 100644
--- a/plugins/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
@@ -16,4 +16,6 @@ val instantiate_tac : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
 val instantiate_tac_by_name : Id.t ->
   Tacinterp.interp_sign * Glob_term.glob_constr -> unit Proofview.tactic
 
-val let_evar : Name.t -> Term.types -> unit Proofview.tactic
+val let_evar : Name.t -> EConstr.types -> unit Proofview.tactic
+
+val hget_evar : int -> unit Proofview.tactic
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b12187e18..7d4bccfad 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -38,12 +38,12 @@ val wit_lglob :
 val wit_lconstr :
   (constr_expr,
   Tacexpr.glob_constr_and_expr,
-  Constr.t) Genarg.genarg_type
+  EConstr.t) Genarg.genarg_type
 
 val wit_casted_constr :
   (constr_expr,
   Tacexpr.glob_constr_and_expr,
-  Constr.t) Genarg.genarg_type
+  EConstr.t) Genarg.genarg_type
 
 val glob : constr_expr Pcoq.Gram.entry
 val lglob : constr_expr Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 7a9fc6657..38fdfb759 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -118,7 +118,7 @@ END
 
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
+  discr_main { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
 
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None) with_evars c
@@ -150,7 +150,7 @@ END
 
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  injection_main false { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
+  injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -290,6 +290,7 @@ END
 (* Hint Resolve                                                       *)
 
 open Term
+open EConstr
 open Vars
 open Coqlib
 
@@ -298,22 +299,25 @@ let project_hint pri l2r r =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, c = Evd.fresh_global env sigma gr in
+  let c = EConstr.of_constr c in
   let t = Retyping.get_type_of env sigma c in
   let t =
     Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
-  let sign,ccl = decompose_prod_assum t in
-  let (a,b) = match snd (decompose_app ccl) with
+  let sign,ccl = decompose_prod_assum sigma t in
+  let (a,b) = match snd (decompose_app sigma ccl) with
     | [a;b] -> (a,b)
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let c = Reductionops.whd_beta Evd.empty (mkApp (c, Context.Rel.to_extended_vect 0 sign)) in
+  let p = EConstr.of_constr p in
+  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
   let ctx = Evd.universe_context_set sigma in
+  let c = EConstr.to_constr sigma c in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
   let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
@@ -341,6 +345,9 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
+open EConstr
+open Vars
+
 let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
@@ -349,14 +356,17 @@ let constr_flags () = {
   Pretyping.expand_evars = true }
 
 let refine_tac ist simple with_classes c =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags =
       { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
-    let update = { run = fun sigma -> c.delayed env sigma } in
+    let update = { run = fun sigma ->
+      let Sigma (c, sigma, p) = c.delayed env sigma in
+      Sigma (c, sigma, p)
+    } in
     let refine = Refine.refine ~unsafe:true update in
     if simple then refine
     else refine <*>
@@ -412,8 +422,6 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ]
 END
 
-open Term
-
 VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
   => [ seff na ]
@@ -492,6 +500,7 @@ let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l"
 let step left x tac =
   let l =
     List.map (fun lem ->
+      let lem = EConstr.of_constr lem in
       Tacticals.New.tclTHENLAST
         (apply_with_bindings (lem, ImplicitBindings [x]))
         tac)
@@ -509,7 +518,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
 
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
-let inTransitivity : bool * constr -> obj =
+let inTransitivity : bool * Constr.constr -> obj =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
@@ -656,7 +665,7 @@ let subst_hole_with_term occ tc t =
 open Tacmach
 
 let hResolve id c occ t =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
@@ -674,6 +683,7 @@ let hResolve id c occ t =
           resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
   in
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
+  let t_constr = EConstr.of_constr t_constr in
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
   let tac =
@@ -701,21 +711,8 @@ END
    hget_evar
 *)
 
-let hget_evar n =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let sigma = Tacmach.New.project gl in
-  let concl = Proofview.Goal.concl gl in
-  let evl = evar_list concl in
-  if List.length evl < n then
-    error "Not enough uninstantiated existential variables.";
-  if n <= 0 then error "Incorrect existential variable index.";
-  let ev = List.nth evl (n-1) in
-  let ev_type = existential_type sigma ev in
-  change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
-  end }
-
 TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> [ hget_evar n ]
+| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ]
 END
 
 (**********************************************************************)
@@ -731,7 +728,7 @@ END
 exception Found of unit Proofview.tactic
 
 let rewrite_except h =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
   Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else 
       Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
@@ -750,11 +747,11 @@ let refl_equal =
   should be replaced by a call to the tactic but I don't know how to
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
        Tacticals.New.tclTHENLIST
-         [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
-          Proofview.Goal.nf_enter { enter = begin fun gl ->
+         [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
+          Proofview.Goal.enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
@@ -766,16 +763,16 @@ let  mkCaseEq a  : unit Proofview.tactic =
 
 
 let case_eq_intros_rewrite x =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let n = nb_prod (Proofview.Goal.concl gl) in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let hyps = Tacmach.New.pf_ids_of_hyps gl in
-      let n' = nb_prod concl in
-      let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in
+      let n' = nb_prod (Tacmach.New.project gl) concl in
+      let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl)  in
       Tacticals.New.tclTHENLIST [
                     Tacticals.New.tclDO (n'-n-1) intro;
 		    introduction h;
@@ -784,36 +781,37 @@ let case_eq_intros_rewrite x =
   ]
   end }
 
-let rec find_a_destructable_match t =
+let rec find_a_destructable_match sigma t =
   let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in
   let cl = [cl, (None, None), None], None in
   let dest = TacAtom (Loc.ghost, TacInductionDestruct(false, false, cl)) in
-  match kind_of_term t with
-    | Case (_,_,x,_) when closed0 x ->
-	if isVar x then
+  match EConstr.kind sigma t with
+    | Case (_,_,x,_) when closed0 sigma x ->
+	if isVar sigma x then
 	  (* TODO check there is no rel n. *)
 	  raise (Found (Tacinterp.eval_tactic dest))
 	else
 	  (* let _ = Pp.msgnl (Printer.pr_lconstr x)  in *)
 	  raise (Found (case_eq_intros_rewrite x))
-    | _ -> iter_constr find_a_destructable_match t
+    | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t
 	
 
 let destauto t =
-  try find_a_destructable_match t;
+  Proofview.tclEVARMAP >>= fun sigma ->
+  try find_a_destructable_match sigma t;
     Tacticals.New.tclZEROMSG (str "No destructable match found")
   with Found tac -> tac
 
 let destauto_in id = 
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
   end }
 
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
+| [ "destauto" ] -> [ Proofview.Goal.enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
@@ -823,8 +821,9 @@ END
 let eq_constr x y = 
   Proofview.Goal.enter { enter = begin fun gl ->
     let evd = Tacmach.New.project gl in
-      if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () 
-      else Tacticals.New.tclFAIL 0 (str "Not equal")
+      match EConstr.eq_constr_universes evd x y with
+      | Some _ -> Proofview.tclUNIT () 
+      | None -> Tacticals.New.tclFAIL 0 (str "Not equal")
   end }
 
 TACTIC EXTEND constr_eq
@@ -833,21 +832,22 @@ END
 
 TACTIC EXTEND constr_eq_nounivs
 | [ "constr_eq_nounivs" constr(x) constr(y) ] -> [
-    if eq_constr_nounivs x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ]
+    Proofview.tclEVARMAP >>= fun sigma ->
+    if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ]
 END
 
 TACTIC EXTEND is_evar
-| [ "is_evar" constr(x) ] ->
-    [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
-      match Evarutil.kind_of_term_upto sigma x with
-        | Evar _ -> Proofview.tclUNIT ()
-        | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
-      end
+| [ "is_evar" constr(x) ] -> [
+    Proofview.tclEVARMAP >>= fun sigma ->
+    match EConstr.kind sigma x with
+      | Evar _ -> Proofview.tclUNIT ()
+      | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
     ]
 END
 
+let has_evar sigma c =
 let rec has_evar x =
-  match kind_of_term x with
+  match EConstr.kind sigma x with
     | Evar _ -> true
     | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ ->
       false
@@ -866,57 +866,68 @@ and has_evar_array x =
   Array.exists has_evar x
 and has_evar_prec (_, ts1, ts2) =
   Array.exists has_evar ts1 || Array.exists has_evar ts2
+in
+has_evar c
 
 TACTIC EXTEND has_evar
-| [ "has_evar" constr(x) ] ->
-    [ if has_evar x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") ]
+| [ "has_evar" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars")
+]
 END
 
 TACTIC EXTEND is_hyp
-| [ "is_var" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_var" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | Var _ ->  Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ]
 END
 
 TACTIC EXTEND is_fix
-| [ "is_fix" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_fix" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | Fix _ -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ]
 END;;
 
 TACTIC EXTEND is_cofix
-| [ "is_cofix" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_cofix" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | CoFix _ -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ]
 END;;
 
 TACTIC EXTEND is_ind
-| [ "is_ind" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_ind" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | Ind _ -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ]
 END;;
 
 TACTIC EXTEND is_constructor
-| [ "is_constructor" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_constructor" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | Construct _ -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ]
 END;;
 
 TACTIC EXTEND is_proj
-| [ "is_proj" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_proj" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | Proj _ -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ]
 END;;
 
 TACTIC EXTEND is_const
-| [ "is_const" constr(x) ] ->
-  [ match kind_of_term x with
+| [ "is_const" constr(x) ] -> [
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.kind sigma x with
     | Const _ -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ]
 END;;
@@ -1060,8 +1071,9 @@ END
 
 let decompose l c =
   Proofview.Goal.enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     let to_ind c =
-      if isInd c then Univ.out_punivs (destInd c)
+      if isInd sigma c then fst (destInd sigma c)
       else error "not an inductive type"
     in
     let l = List.map to_ind l in
@@ -1075,10 +1087,14 @@ END
 (** library/keys *)
 
 VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
-| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ 
-  let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in 
-  let k1 = Keys.constr_key (it c) in
-  let k2 = Keys.constr_key (it c') in
+| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
+  let get_key c =
+    let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+    let kind c = EConstr.kind evd c in
+    Keys.constr_key kind c
+  in
+  let k1 = get_key c in
+  let k2 = get_key c' in
     match k1, k2 with
     | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
     | _ -> () ]
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index f75ea7087..dfa8331ff 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,6 +16,7 @@ open Pcoq.Constr
 open Pltac
 open Hints
 open Tacexpr
+open Proofview.Notations
 open Names
 
 DECLARE PLUGIN "g_auto"
@@ -49,7 +50,11 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true
   } in
-  List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
+  let map c = { delayed = fun env sigma ->
+    let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in
+    Sigma.Sigma (c, sigma, p)
+  } in
+  List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
 
 let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
 let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index ca9537c82..40f30c794 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -89,7 +89,7 @@ TACTIC EXTEND is_ground
 END
 
 TACTIC EXTEND autoapply
-  [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ]
+  [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ]
 END
 
 (** TODO: DEPRECATE *)
@@ -98,18 +98,20 @@ open Term
 open Proofview.Goal
 open Proofview.Notations
 
-let rec eq_constr_mod_evars x y =
-  match kind_of_term x, kind_of_term y with
+let rec eq_constr_mod_evars sigma x y =
+  let open EConstr in
+  match EConstr.kind sigma x, EConstr.kind sigma y with
   | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true
-  | _, _ -> compare_constr eq_constr_mod_evars x y
+  | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y
 
 let progress_evars t =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let check =
-      Proofview.Goal.nf_enter { enter = begin fun gl' ->
+      Proofview.Goal.enter { enter = begin fun gl' ->
+        let sigma = Tacmach.New.project gl' in
         let newconcl = Proofview.Goal.concl gl' in
-        if eq_constr_mod_evars concl newconcl
+        if eq_constr_mod_evars sigma concl newconcl
         then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
         else Proofview.tclUNIT ()
       end }
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index dc418d530..39ae1f41d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -79,8 +79,8 @@ type 'a glob_extra_genarg_printer =
     'a -> std_ppcmds
 
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) ->
-    (Term.constr -> std_ppcmds) ->
+    (EConstr.constr -> std_ppcmds) ->
+    (EConstr.constr -> std_ppcmds) ->
     (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
@@ -1153,23 +1153,24 @@ type 'a extra_genarg_printer =
   let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
   let strip_prod_binders_constr n ty =
+    let ty = EConstr.Unsafe.to_constr ty in
     let rec strip_ty acc n ty =
-      if n=0 then (List.rev acc, ty) else
+      if n=0 then (List.rev acc, EConstr.of_constr ty) else
         match Term.kind_of_term ty with
             Term.Prod(na,a,b) ->
-              strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
+              strip_ty (([Loc.ghost,na],EConstr.of_constr a)::acc) (n-1) b
           | _ -> error "Cannot translate fix tactic: not enough products" in
     strip_ty [] n ty
 
-  let pr_atomic_tactic_level env n t =
+  let pr_atomic_tactic_level env sigma n t =
     let prtac n (t:atomic_tactic_expr) =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
-        pr_constr = pr_constr_env env Evd.empty;
+        pr_constr = (fun c -> pr_econstr_env env sigma c);
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_lconstr = pr_lconstr_env env Evd.empty;
-        pr_pattern = pr_constr_pattern_env env Evd.empty;
-        pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
+        pr_lconstr = (fun c -> pr_leconstr_env env sigma c);
+        pr_pattern = pr_constr_pattern_env env sigma;
+        pr_lpattern = pr_lconstr_pattern_env env sigma;
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
@@ -1200,7 +1201,7 @@ type 'a extra_genarg_printer =
   let pr_extend pr lev ml args =
     pr_extend_gen pr lev ml args
 
-  let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
+  let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c
 
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
@@ -1217,7 +1218,7 @@ let declare_extra_genarg_pprule wit
   in
   let h x =
     let env = Global.env () in
-    h (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+    h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
   in
   Genprint.register_print0 wit f g h
 
@@ -1247,7 +1248,7 @@ let () =
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
+    (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c))));
   Genprint.register_print0
     wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
@@ -1258,7 +1259,7 @@ let () =
     wit_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_constr
+    Printer.pr_econstr
   ;
   Genprint.register_print0
     wit_uconstr
@@ -1270,25 +1271,25 @@ let () =
     wit_open_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_constr
+    Printer.pr_econstr
   ;
   Genprint.register_print0 wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
     (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
-    (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+    (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
   Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
   Genprint.register_print0 wit_bindings
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+    (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
+    (fun it -> pr_with_bindings pr_econstr pr_leconstr (fst (run_delayed it)));
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it));
+    (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it));
   Genprint.register_print0 Stdarg.wit_int int int int;
   Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
   Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 43e22dba3..729338fb9 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -36,8 +36,8 @@ type 'a glob_extra_genarg_printer =
     'a -> std_ppcmds
 
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) ->
-    (Term.constr -> std_ppcmds) ->
+    (EConstr.t -> std_ppcmds) ->
+    (EConstr.t -> std_ppcmds) ->
     (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
@@ -100,7 +100,7 @@ val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
 
 val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
-val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
+val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds
 
 val pr_hintbases : string list option -> std_ppcmds
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3c5a109c0..b84be4600 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -13,6 +13,7 @@ open Util
 open Nameops
 open Namegen
 open Term
+open EConstr
 open Vars
 open Reduction
 open Tacticals.New
@@ -31,6 +32,7 @@ open Decl_kinds
 open Elimschemes
 open Environ
 open Termops
+open EConstr
 open Libnames
 open Sigma.Notations
 open Proofview.Notations
@@ -97,7 +99,7 @@ let new_cstr_evar (evd,cstrs) env t =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in
   let evd' = Sigma.to_evar_map evd' in
-  let ev, _ = destEvar t in
+  let ev, _ = destEvar evd' t in
     (evd', Evar.Set.add ev cstrs), t
 
 (** Building or looking up instances. *)
@@ -214,7 +216,7 @@ end) = struct
       match obj with
       | None | Some (_, None) ->
 	let evars, relty = mk_relation env evars ty in
-	  if closed0 ty then 
+	  if closed0 (goalevars evars) ty then 
 	    let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
 	      new_cstr_evar evars env' relty
 	  else new_cstr_evar evars newenv relty
@@ -222,10 +224,10 @@ end) = struct
     in
     let rec aux env evars ty l =
       let t = Reductionops.whd_all env (goalevars evars) ty in
-	match kind_of_term t, l with
+	match EConstr.kind (goalevars evars) t, l with
 	| Prod (na, ty, b), obj :: cstrs ->
           let b = Reductionops.nf_betaiota (goalevars evars) b in
-	  if noccurn 1 b (* non-dependent product *) then
+	  if noccurn (goalevars evars) 1 b (* non-dependent product *) then
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
@@ -233,7 +235,7 @@ end) = struct
 	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
 	  else
 	    let (evars, b, arg, cstrs) =
-	      aux (Environ.push_rel (LocalAssum (na, ty)) env) evars b cstrs
+	      aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
 	    in
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let pred = mkLambda (na, ty, b) in
@@ -253,30 +255,30 @@ end) = struct
 
   (** Folding/unfolding of the tactic constants. *)
 
-  let unfold_impl t =
-    match kind_of_term t with
+  let unfold_impl sigma t =
+    match EConstr.kind sigma t with
     | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
       mkProd (Anonymous, a, lift 1 b)
     | _ -> assert false
 
-  let unfold_all t =
-    match kind_of_term t with
+  let unfold_all sigma t =
+    match EConstr.kind sigma t with
     | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
-      (match kind_of_term b with
+      (match EConstr.kind sigma b with
       | Lambda (n, ty, b) -> mkProd (n, ty, b)
       | _ -> assert false)
     | _ -> assert false
 
-  let unfold_forall t =
-    match kind_of_term t with
+  let unfold_forall sigma t =
+    match EConstr.kind sigma t with
     | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
-      (match kind_of_term b with
+      (match EConstr.kind sigma b with
       | Lambda (n, ty, b) -> mkProd (n, ty, b)
       | _ -> assert false)
     | _ -> assert false
 
   let arrow_morphism env evd ta tb a b =
-    let ap = is_Prop ta and bp = is_Prop tb in
+    let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in
       if ap && bp then app_poly env evd impl [| a; b |], unfold_impl
       else if ap then (* Domain in Prop, CoDomain in Type *)
 	(app_poly env evd arrow [| a; b |]), unfold_impl
@@ -286,28 +288,28 @@ end) = struct
       else (* None in Prop, use arrow *)
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 
-  let rec decomp_pointwise n c =
+  let rec decomp_pointwise sigma n c =
     if Int.equal n 0 then c
     else
-      match kind_of_term c with
-      | App (f, [| a; b; relb |]) when Globnames.is_global (pointwise_relation_ref ()) f ->
-	decomp_pointwise (pred n) relb
-      | App (f, [| a; b; arelb |]) when Globnames.is_global (forall_relation_ref ()) f ->
-	decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1]))
+      match EConstr.kind sigma c with
+      | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
+	decomp_pointwise sigma (pred n) relb
+      | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
+	decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
       | _ -> invalid_arg "decomp_pointwise"
 
-  let rec apply_pointwise rel = function
+  let rec apply_pointwise sigma rel = function
     | arg :: args ->
-      (match kind_of_term rel with
-      | App (f, [| a; b; relb |]) when Globnames.is_global (pointwise_relation_ref ()) f ->
-	apply_pointwise relb args
-      | App (f, [| a; b; arelb |]) when Globnames.is_global (forall_relation_ref ()) f ->
-	apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args
+      (match EConstr.kind sigma rel with
+      | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
+	apply_pointwise sigma relb args
+      | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
+	apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args
       | _ -> invalid_arg "apply_pointwise")
     | [] -> rel
 
   let pointwise_or_dep_relation env evd n t car rel =
-    if noccurn 1 car && noccurn 1 rel then
+    if noccurn (goalevars evd) 1 car && noccurn (goalevars evd) 1 rel then
       app_poly env evd pointwise_relation [| t; lift (-1) car; lift (-1) rel |]
     else
       app_poly env evd forall_relation
@@ -324,14 +326,15 @@ end) = struct
     let rec aux evars env prod n = 
       if Int.equal n 0 then start evars env prod
       else
-	match kind_of_term (Reduction.whd_all env prod) with
+        let sigma = goalevars evars in
+	match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
 	| Prod (na, ty, b) ->
-	  if noccurn 1 b then
+	  if noccurn sigma 1 b then
 	    let b' = lift (-1) b in
 	    let evars, rb = aux evars env b' (pred n) in
 	      app_poly env evars pointwise_relation [| ty; b'; rb |]
 	  else
-	    let evars, rb = aux evars (Environ.push_rel (LocalAssum (na, ty)) env) b (pred n) in
+	    let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in
 	      app_poly env evars forall_relation
 		[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
 	| _ -> raise Not_found
@@ -342,24 +345,25 @@ end) = struct
 	try let evars, found = aux evars env ty (succ (List.length args)) in
 	      Some (evars, found, c, ty, arg :: args)
 	with Not_found ->
-	  let ty = whd_all env ty in
-	  find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args
+          let sigma = goalevars evars in
+	  let ty = Reductionops.whd_all env sigma ty in
+	  find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args
     in find env c ty args
 
   let unlift_cstr env sigma = function
     | None -> None
-    | Some codom -> Some (decomp_pointwise 1 codom)
+    | Some codom -> Some (decomp_pointwise (goalevars sigma) 1 codom)
 
   (** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
   let is_applied_rewrite_relation env sigma rels t =
-    match kind_of_term t with
+    match EConstr.kind sigma t with
     | App (c, args) when Array.length args >= 2 ->
-      let head = if isApp c then fst (destApp c) else c in
-	if Globnames.is_global (coq_eq_ref ()) head then None
+      let head = if isApp sigma c then fst (destApp sigma c) else c in
+	if Termops.is_global sigma (coq_eq_ref ()) head then None
 	else
 	  (try
 	   let params, args = Array.chop (Array.length args - 2) args in
-	   let env' = Environ.push_rel_context rels env in
+	   let env' = push_rel_context rels env in
 	   let sigma = Sigma.Unsafe.of_evar_map sigma in
 	   let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
 	   let evars = Sigma.to_evar_map evars in
@@ -430,7 +434,7 @@ module TypeGlobal = struct
 end
 
 let sort_of_rel env evm rel =
-  Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)
+  ESorts.kind evm (Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel))
 
 let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation
 
@@ -480,7 +484,7 @@ let error_no_relation () = error "Cannot find a relation to rewrite."
 let rec decompose_app_rel env evd t = 
   (** Head normalize for compatibility with the old meta mechanism *)
   let t = Reductionops.whd_betaiota evd t in
-  match kind_of_term t with
+  match EConstr.kind evd t with
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
     let (f', argl, argr) = decompose_app_rel env evd arg in
@@ -499,7 +503,7 @@ let rec decompose_app_rel env evd t =
 let decompose_app_rel env evd t =
   let (rel, t1, t2) = decompose_app_rel env evd t in
   let ty = Retyping.get_type_of env evd rel in
-  let () = if not (Reduction.is_arity env ty) then error_no_relation () in
+  let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in
   (rel, t1, t2)
 
 let decompose_applied_relation env sigma (c,l) =
@@ -617,9 +621,10 @@ let solve_remaining_by env sigma holes by =
   | Some tac ->
     let map h =
       if h.Clenv.hole_deps then None
-      else
-        let (evk, _) = destEvar (h.Clenv.hole_evar) in
+      else match EConstr.kind sigma h.Clenv.hole_evar with
+      | Evar (evk, _) ->
         Some evk
+      | _ -> None
     in
     (** Only solve independent holes *)
     let indep = List.map_filter map holes in
@@ -639,7 +644,7 @@ let solve_remaining_by env sigma holes by =
         (** Evar should not be defined, but just in case *)
       | Some evi ->
         let env = Environ.reset_with_named_context evi.evar_hyps env in
-        let ty = evi.evar_concl in
+        let ty = EConstr.of_constr evi.evar_concl in
         let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
         Evd.define evk c sigma
     in
@@ -714,7 +719,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
     let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
       ~fail:true env sigma in
     let evd = solve_remaining_by env sigma holes by in
-    let nf c = Evarutil.nf_evar evd (Reductionops.nf_meta evd c) in
+    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
     let c1 = nf c1 and c2 = nf c2
     and rew_car = nf car and rel = nf rel
     and prf = nf prf in
@@ -754,9 +759,9 @@ let default_flags = { under_lambdas = true; on_morphisms = true; }
 let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
 
 let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
 let make_eq_refl () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
 
 let get_rew_prf r = match r.rew_prf with
   | RewPrf (rel, prf) -> rel, prf 
@@ -769,7 +774,7 @@ let poly_subrelation sort =
   if sort then PropGlobal.subrelation else TypeGlobal.subrelation
 
 let resolve_subrelation env avoid car rel sort prf rel' res =
-  if eq_constr rel rel' then res
+  if Termops.eq_constr (fst res.rew_evars) rel rel' then res
   else
     let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
     let evars, subrel = new_cstr_evar evars env app in
@@ -805,7 +810,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	if b then PropGlobal.do_subrelation, PropGlobal.apply_subrelation 
 	else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
       in
-	Environ.push_named
+	EConstr.push_named
 	  (LocalDef (Id.of_string "do_subrelation",
 	             snd (app_poly_sort b env evars dosub [||]),
 	             snd (app_poly_nocheck env evars appsub [||])))
@@ -837,8 +842,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
       ([], [], evars, sigargs, []) args args'
   in
-  let proof = applistc proj (List.rev projargs) in
-  let newt = applistc m' (List.rev typeargs) in
+  let proof = applist (proj, List.rev projargs) in
+  let newt = applist (m', List.rev typeargs) in
     match respars with
 	[ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
       | _ -> assert(false)
@@ -861,13 +866,13 @@ let apply_rule unify loccs : int pure_strategy =
   in
   { strategy = fun { state = occ ; env ; unfresh ;
 		     term1 = t ; ty1 = ty ; cstr ; evars } ->
-      let unif = if isEvar t then None else unify env evars t in
+      let unif = if isEvar (goalevars evars) t then None else unify env evars t in
 	match unif with
 	| None -> (occ, Fail)
         | Some rew ->
 	  let occ = succ occ in
 	    if not (is_occ occ) then (occ, Fail)
-	    else if eq_constr t rew.rew_to then (occ, Identity)
+	    else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
 	    else
 	      let res = { rew with rew_car = ty } in
               let rel, prf = get_rew_prf res in
@@ -921,17 +926,17 @@ let reset_env env =
     Environ.push_rel_context (Environ.rel_context env) env'
       
 let fold_match ?(force=false) env sigma c =
-  let (ci, p, c, brs) = destCase c in
+  let (ci, p, c, brs) = destCase sigma c in
   let cty = Retyping.get_type_of env sigma c in
   let dep, pred, exists, (sk,eff) = 
     let env', ctx, body =
-      let ctx, pred = decompose_lam_assum p in
-      let env' = Environ.push_rel_context ctx env in
+      let ctx, pred = decompose_lam_assum sigma p in
+      let env' = push_rel_context ctx env in
 	env', ctx, pred
     in
     let sortp = Retyping.get_sort_family_of env' sigma body in
     let sortc = Retyping.get_sort_family_of env sigma cty in
-    let dep = not (noccurn 1 body) in
+    let dep = not (noccurn sigma 1 body) in
     let pred = if dep then p else
 	it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
     in
@@ -955,7 +960,7 @@ let fold_match ?(force=false) env sigma c =
       else raise Not_found
   in
   let app =
-    let ind, args = Inductive.find_rectype env cty in
+    let ind, args = Inductiveops.find_mrectype env sigma cty in
     let pars, args = List.chop ci.ci_npar args in
     let meths = List.map (fun br -> br) (Array.to_list brs) in
       applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
@@ -963,9 +968,10 @@ let fold_match ?(force=false) env sigma c =
     sk, (if exists then env else reset_env env), app, eff
 
 let unfold_match env sigma sk app =
-  match kind_of_term app with
-  | App (f', args) when eq_constant (fst (destConst f')) sk ->
+  match EConstr.kind sigma app with
+  | App (f', args) when eq_constant (fst (destConst sigma f')) sk ->
       let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
+      let v = EConstr.of_constr v in
 	Reductionops.whd_beta sigma (mkApp (v, args))
   | _ -> app
 
@@ -975,7 +981,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
   let rec aux { state ; env ; unfresh ;
 		term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
     let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
-      match kind_of_term t with
+      match EConstr.kind (goalevars evars) t with
       | App (m, args) ->
 	  let rewrite_args state success =
 	    let state, (args', evars', progress) =
@@ -1055,7 +1061,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 			let app = if prop then PropGlobal.apply_pointwise 
 			  else TypeGlobal.apply_pointwise 
 			in
-			  RewPrf (app rel argsl, mkApp (prf, args))
+			  RewPrf (app (goalevars evars) rel argsl, mkApp (prf, args))
 		      | x -> x
 		    in
 		    let res =
@@ -1072,9 +1078,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		    in state, res
 	    else rewrite_args state None
 	      
-      | Prod (n, x, b) when noccurn 1 b ->
+      | Prod (n, x, b) when noccurn (goalevars evars) 1 b ->
 	  let b = subst1 mkProp b in
-	  let tx = Retyping.get_type_of env (goalevars evars) x 
+	  let tx = Retyping.get_type_of env (goalevars evars) x
 	  and tb = Retyping.get_type_of env (goalevars evars) b in
 	  let arr = if prop then PropGlobal.arrow_morphism 
 	    else TypeGlobal.arrow_morphism 
@@ -1085,7 +1091,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 				 cstr = (prop,cstr) ; evars = evars' } in
 	  let res = 
 	    match res with
-	    | Success r -> Success { r with rew_to = unfold r.rew_to }
+	    | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
 	    | Fail | Identity -> res
 	  in state, res
 
@@ -1106,7 +1112,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       | Prod (n, dom, codom) ->
 	  let lam = mkLambda (n, dom, codom) in
 	  let (evars', app), unfold = 
-	    if eq_constr ty mkProp then
+	    if eq_constr (fst evars) ty mkProp then
 	      (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
 	    else 
 	      let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
@@ -1117,7 +1123,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 				 cstr = (prop,cstr) ; evars = evars' } in
 	  let res = 
 	    match res with
-	    | Success r -> Success { r with rew_to = unfold r.rew_to }
+	    | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
 	    | Fail | Identity -> res
 	  in state, res
 
@@ -1152,7 +1158,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       | Lambda (n, t, b) when flags.under_lambdas ->
         let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
         let open Context.Rel.Declaration in
-	let env' = Environ.push_rel (LocalAssum (n', t)) env in
+	let env' = EConstr.push_rel (LocalAssum (n', t)) env in
 	let bty = Retyping.get_type_of env' (goalevars evars) b in
 	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
 	let state, b' = s.strategy { state ; env = env' ; unfresh ;
@@ -1381,7 +1387,7 @@ module Strategies =
     let inj_open hint = (); fun sigma ->
       let ctx = Evd.evar_universe_context_of hint.Autorewrite.rew_ctx in
       let sigma = Evd.merge_universe_context sigma ctx in
-      (sigma, (hint.Autorewrite.rew_lemma, NoBindings))
+      (sigma, (EConstr.of_constr hint.Autorewrite.rew_lemma, NoBindings))
 
     let old_hints (db : string) : 'a pure_strategy =
       let rules = Autorewrite.find_rewrites db in
@@ -1391,6 +1397,7 @@ module Strategies =
 
     let hints (db : string) : 'a pure_strategy = { strategy =
       fun ({ term1 = t } as input) ->
+      let t = EConstr.Unsafe.to_constr t in
       let rules = Autorewrite.find_matches db t in
       let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
 			hint.Autorewrite.rew_tac) in
@@ -1404,7 +1411,7 @@ module Strategies =
           let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in
 	  let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in
 	  let evars' = Sigma.to_evar_map sigma in
-	    if eq_constr t' t then
+	    if Termops.eq_constr evars' t' t then
 	      state, Identity
 	    else
 	      state, Success { rew_car = ty; rew_from = t; rew_to = t';
@@ -1423,7 +1430,7 @@ module Strategies =
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
-	    let c' = Evarutil.nf_evar sigma c in
+	    let c' = Reductionops.nf_evar sigma c in
 	      state, Success { rew_car = ty; rew_from = t; rew_to = c';
 				  rew_prf = RewCast DEFAULTcast;
 				  rew_evars = (sigma, snd evars) }
@@ -1496,7 +1503,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
     | Success res ->
       let (_, cstrs) = res.rew_evars in
       let evars' = solve_constraints env res.rew_evars in
-      let newt = Evarutil.nf_evar evars' res.rew_to in
+      let newt = Reductionops.nf_evar evars' res.rew_to in
       let evars = (* Keep only original evars (potentially instantiated) and goal evars,
 		     the rest has been defined and substituted already. *)
 	Evar.Set.fold 
@@ -1504,20 +1511,20 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	   if not (Evd.is_defined acc ev) then 
 	     user_err ~hdr:"rewrite"
 			  (str "Unsolved constraint remaining: " ++ spc () ++
-			   Evd.pr_evar_info (Evd.find acc ev))
+			   Termops.pr_evar_info (Evd.find acc ev))
 	   else Evd.remove acc ev) 
 	  cstrs evars'
       in
       let res = match res.rew_prf with
 	| RewCast c -> None
 	| RewPrf (rel, p) ->
-	  let p = nf_zeta env evars' (Evarutil.nf_evar evars' p) in
+	  let p = nf_zeta env evars' (Reductionops.nf_evar evars' p) in
 	  let term =
 	    match abs with
 	    | None -> p
 	    | Some (t, ty) ->
-              let t = Evarutil.nf_evar evars' t in
-              let ty = Evarutil.nf_evar evars' ty in
+              let t = Reductionops.nf_evar evars' t in
+              let ty = Reductionops.nf_evar evars' ty in
 		mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
 	  in
 	  let proof = match is_hyp with
@@ -1527,23 +1534,24 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
       in Some (Some (evars, res, newt))
 
 (** Insert a declaration after the last declaration it depends on *)
-let rec insert_dependent env decl accu hyps = match hyps with
+let rec insert_dependent env sigma decl accu hyps = match hyps with
 | [] -> List.rev_append accu [decl]
 | ndecl :: rem ->
-  if occur_var_in_decl env (NamedDecl.get_id ndecl) decl then
+  if occur_var_in_decl env sigma (NamedDecl.get_id ndecl) decl then
     List.rev_append accu (decl :: hyps)
   else
-    insert_dependent env decl (ndecl :: accu) rem
+    insert_dependent env sigma decl (ndecl :: accu) rem
 
 let assert_replacing id newt tac = 
-  let prf = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let prf = Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let ctx = Environ.named_context env in
+    let sigma = Tacmach.New.project gl in
+    let ctx = named_context env in
     let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in
     let nc = match before with
     | [] -> assert false
-    | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
+    | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Refine.refine ~unsafe:false { run = begin fun sigma ->
@@ -1553,7 +1561,7 @@ let assert_replacing id newt tac =
         let n = NamedDecl.get_id d in
         if Id.equal n id then ev' else mkVar n
       in
-      let (e, _) = destEvar ev in
+      let (e, _) = destEvar (Sigma.to_evar_map sigma) ev in
       Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
     end }
   end } in
@@ -1603,22 +1611,22 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = match clause with
     | None -> concl
-    | Some id -> Environ.named_type id env
+    | Some id -> EConstr.of_constr (Environ.named_type id env)
     in
     let env = match clause with
     | None -> env
     | Some id ->
       (** Only consider variables not depending on [id] *)
-      let ctx = Environ.named_context env in
-      let filter decl = not (occur_var_in_decl env id decl) in
+      let ctx = named_context env in
+      let filter decl = not (occur_var_in_decl env sigma id decl) in
       let nctx = List.filter filter ctx in
-      Environ.reset_with_named_context (Environ.val_of_named_context nctx) env
+      Environ.reset_with_named_context (val_of_named_context nctx) env
     in
     try
       let res =
@@ -1853,9 +1861,10 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 
 let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None)
 
-let proper_projection r ty =
-  let ctx, inst = decompose_prod_assum ty in
-  let mor, args = destApp inst in
+let proper_projection sigma r ty =
+  let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
+  let ctx, inst = decompose_prod_assum sigma ty in
+  let mor, args = destApp sigma inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
   let app = mkApp (Lazy.force PropGlobal.proper_proj,
 		  Array.append args [| instarg |]) in
@@ -1866,31 +1875,34 @@ let declare_projection n instance_id r =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma,c = Evd.fresh_global env sigma r in
+  let c = EConstr.of_constr c in
   let ty = Retyping.get_type_of env sigma c in
-  let term = proper_projection c ty in
+  let term = proper_projection sigma c ty in
   let sigma, typ = Typing.type_of env sigma term in
-  let ctx, typ = decompose_prod_assum typ in
+  let ctx, typ = decompose_prod_assum sigma typ in
   let typ =
     let n =
       let rec aux t =
-	match kind_of_term t with
+	match EConstr.kind sigma t with
 	| App (f, [| a ; a' ; rel; rel' |]) 
-	    when Globnames.is_global (PropGlobal.respectful_ref ()) f ->
+	    when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
 	  succ (aux rel')
 	| _ -> 0
       in
       let init =
-	match kind_of_term typ with
-	    App (f, args) when Globnames.is_global (PropGlobal.respectful_ref ()) f  ->
+	match EConstr.kind sigma typ with
+	    App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f  ->
 	      mkApp (f, fst (Array.chop (Array.length args - 2) args))
 	  | _ -> typ
       in aux init
     in
-    let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ
+    let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
   let pl, ctx = Evd.universe_context sigma in
+  let typ = EConstr.to_constr sigma typ in
+  let term = EConstr.to_constr sigma term in
   let cst = 
     Declare.definition_entry ~types:typ ~poly ~univs:ctx term
   in
@@ -1899,11 +1911,12 @@ let declare_projection n instance_id r =
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
+  let m = EConstr.of_constr m in
   let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
   let cstrs =
     let rec aux t =
-      match kind_of_term t with
+      match EConstr.kind sigma t with
 	| Prod (na, a, b) ->
 	    None :: aux b
 	| _ -> []
@@ -1923,8 +1936,8 @@ let build_morphism_signature env sigma m =
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
   let evd = Evd.nf_constraints evd in
-  let m = Evarutil.nf_evars_universes evd morph in
-  Pretyping.check_evars env Evd.empty evd m;
+  let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
+  Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
@@ -1936,7 +1949,7 @@ let default_morphism sign m =
   in
   let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
   let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
-    mor, proper_projection mor morph
+    mor, proper_projection sigma mor morph
 
 let add_setoid global binders a aeq t n =
   init_setoid ();
@@ -1991,7 +2004,7 @@ let add_morphism_infer glob m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook;
+	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
@@ -2052,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
         ~flags:rewrite_conv_unif_flags
         env sigma ((if l2r then c1 else c2),but)
   in
-  let nf c = Evarutil.nf_evar sigma c in
+  let nf c = Reductionops.nf_evar sigma c in
   let c1 = if l2r then nf c' else nf c1
   and c2 = if l2r then nf c2 else nf c'
   and car = nf car and rel = nf rel in
@@ -2071,7 +2084,7 @@ let get_hyp gl (c,l) clause l2r =
   let sigma, hi = decompose_applied_relation env evars (c,l) in
   let but = match clause with
     | Some id -> Tacmach.New.pf_get_hyp_typ id gl
-    | None -> Evarutil.nf_evar evars (Tacmach.New.pf_concl gl)
+    | None -> Reductionops.nf_evar evars (Tacmach.New.pf_concl gl)
   in
   unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env
 
@@ -2082,7 +2095,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
   let unify env evars t = unify_abs res l2r sort env evars t in
   let app = apply_rule unify occs in
@@ -2110,13 +2123,13 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
-let not_declared env ty rel =
+let not_declared env sigma ty rel =
   tclFAIL 0
-    (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
+    (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++
      str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
 let setoid_proof ty fn fallback =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
@@ -2125,7 +2138,7 @@ let setoid_proof ty fn fallback =
         try
           let rel, _, _ = decompose_app_rel env sigma concl in
           let (sigma, t) = Typing.type_of env sigma rel in
-          let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in
+          let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
 	    (try init_relation_classes () with _ -> raise Not_found);
             fn env sigma car rel
         with e -> Proofview.tclZERO e
@@ -2139,7 +2152,7 @@ let setoid_proof ty fn fallback =
 	            begin match e with
 	            | (Not_found, _) ->
 	                let rel, _, _ = decompose_app_rel env sigma concl in
-		        not_declared env ty rel
+		        not_declared env sigma ty rel
 	            | (e, info) -> Proofview.tclZERO ~info e
                     end
                 | e' -> Proofview.tclZERO ~info e'
@@ -2185,9 +2198,10 @@ let setoid_transitivity c =
     
 let setoid_symmetry_in id =
   Proofview.V82.tactic (fun gl ->
+  let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
-  let binders,concl = decompose_prod_assum ctype in
-  let (equiv, args) = decompose_app concl in
+  let binders,concl = decompose_prod_assum sigma ctype in
+  let (equiv, args) = decompose_app sigma concl in
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
     | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 4fdce0c84..7a20838a2 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -9,6 +9,7 @@
 open Names
 open Constr
 open Environ
+open EConstr
 open Constrexpr
 open Tacexpr
 open Misctypes
@@ -74,7 +75,7 @@ val cl_rewrite_clause :
   bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
 
 val is_applied_rewrite_relation :
-  env -> evar_map -> Context.Rel.t -> constr -> types option
+  env -> evar_map -> rel_context -> constr -> types option
 
 val declare_relation :
   ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
@@ -112,6 +113,6 @@ val apply_strategy :
   strategy ->
   Environ.env ->
   Names.Id.t list ->
-  Term.constr ->
-  bool * Term.constr ->
+  constr ->
+  bool * constr ->
   evars -> rewrite_result
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index df38a42cb..b76009c99 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open EConstr
 open Pattern
 open Misctypes
 open Genarg
@@ -17,7 +18,7 @@ open Geninterp
 
 exception CannotCoerceTo of string
 
-let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
+let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_context" in
   let () = register_val0 wit None in
   wit
@@ -96,7 +97,7 @@ let is_variable env id =
 
 (* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
-  Term.mkVar (let _ = Environ.lookup_named id env in id)
+  EConstr.mkVar (let _ = Environ.lookup_named id env in id)
 
 (* Gives the constr corresponding to a Constr_context tactic_arg *)
 let coerce_to_constr_context v =
@@ -106,7 +107,7 @@ let coerce_to_constr_context v =
   else raise (CannotCoerceTo "a term context")
 
 (* Interprets an identifier which must be fresh *)
-let coerce_var_to_ident fresh env v =
+let coerce_var_to_ident fresh env sigma v =
   let v = Value.normalize v in
   let fail () = raise (CannotCoerceTo "a fresh identifier") in
   if has_type v (topwit wit_intro_pattern) then
@@ -119,15 +120,16 @@ let coerce_var_to_ident fresh env v =
   | None -> fail ()
   | Some c ->
     (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
-    if isVar c && not (fresh && is_variable env (destVar c)) then
-      destVar c
+    if isVar sigma c && not (fresh && is_variable env (destVar sigma c)) then
+      destVar sigma c
     else fail ()
 
 
 (* Interprets, if possible, a constr to an identifier which may not
    be fresh but suitable to be given to the fresh tactic. Works for
    vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh g env v =
+let coerce_to_ident_not_fresh env sigma v =
+let g = sigma in
 let id_of_name = function
   | Names.Anonymous -> Id.of_string "x"
   | Names.Name x -> x in
@@ -143,7 +145,7 @@ let id_of_name = function
     match Value.to_constr v with
     | None -> fail ()
     | Some c ->
-       match Constr.kind c with
+       match EConstr.kind sigma c with
        | Var id -> id 
        | Meta m -> id_of_name (Evd.meta_name g m)
        | Evar (kn,_) ->
@@ -162,14 +164,14 @@ let id_of_name = function
 	  basename
        | Sort s ->
 	  begin
-	    match s with
+	    match ESorts.kind sigma s with
 	    | Prop _ -> Label.to_id (Label.make "Prop")
 	    | Type _ -> Label.to_id (Label.make "Type")
 	  end
        | _ -> fail()
 
 
-let coerce_to_intro_pattern env v =
+let coerce_to_intro_pattern env sigma v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     snd (out_gen (topwit wit_intro_pattern) v)
@@ -177,14 +179,14 @@ let coerce_to_intro_pattern env v =
     let id = out_gen (topwit wit_var) v in
     IntroNaming (IntroIdentifier id)
   else match Value.to_constr v with
-  | Some c when isVar c ->
+  | Some c when isVar sigma c ->
       (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
       (* but also in "destruct H as (H,H')" *)
-      IntroNaming (IntroIdentifier (destVar c))
+      IntroNaming (IntroIdentifier (destVar sigma c))
   | _ -> raise (CannotCoerceTo "an introduction pattern")
 
-let coerce_to_intro_pattern_naming env v =
-  match coerce_to_intro_pattern env v with
+let coerce_to_intro_pattern_naming env sigma v =
+  match coerce_to_intro_pattern env sigma v with
   | IntroNaming pat -> pat
   | _ -> raise (CannotCoerceTo "a naming introduction pattern")
 
@@ -232,7 +234,7 @@ let coerce_to_closed_constr env v =
   let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
   c
 
-let coerce_to_evaluable_ref env v =
+let coerce_to_evaluable_ref env sigma v =
   let fail () = raise (CannotCoerceTo "an evaluable reference") in
   let v = Value.normalize v in
   let ev =
@@ -253,8 +255,8 @@ let coerce_to_evaluable_ref env v =
     | IndRef _ | ConstructRef _ -> fail ()
   else
     match Value.to_constr v with
-    | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
-    | Some c when isVar c -> EvalVarRef (destVar c)
+    | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
+    | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
     | _ -> fail ()
   in if Tacred.is_evaluable env ev then ev else fail ()
 
@@ -266,14 +268,14 @@ let coerce_to_constr_list env v =
     List.map map l
   | None -> raise (CannotCoerceTo "a term list")
 
-let coerce_to_intro_pattern_list loc env v =
+let coerce_to_intro_pattern_list loc env sigma v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
-    let map v = (loc, coerce_to_intro_pattern env v) in
+    let map v = (loc, coerce_to_intro_pattern env sigma v) in
     List.map map l
 
-let coerce_to_hyp env v =
+let coerce_to_hyp env sigma v =
   let fail () = raise (CannotCoerceTo "a variable") in
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
@@ -284,31 +286,31 @@ let coerce_to_hyp env v =
     let id = out_gen (topwit wit_var) v in
     if is_variable env id then id else fail ()
   else match Value.to_constr v with
-  | Some c when isVar c -> destVar c
+  | Some c when isVar sigma c -> destVar sigma c
   | _ -> fail ()
 
-let coerce_to_hyp_list env v =
+let coerce_to_hyp_list env sigma v =
   let v = Value.to_list v in
   match v with
   | Some l ->
-    let map n = coerce_to_hyp env n in
+    let map n = coerce_to_hyp env sigma n in
     List.map map l
   | None -> raise (CannotCoerceTo "a variable list")
 
 (* Interprets a qualified name *)
-let coerce_to_reference env v =
+let coerce_to_reference env sigma v =
   let v = Value.normalize v in
   match Value.to_constr v with
   | Some c ->
     begin
-      try Globnames.global_of_constr c
+      try fst (Termops.global_of_constr sigma c)
       with Not_found -> raise (CannotCoerceTo "a reference")
     end
   | None -> raise (CannotCoerceTo "a reference")
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
-let coerce_to_quantified_hypothesis v =
+let coerce_to_quantified_hypothesis sigma v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     let v = out_gen (topwit wit_intro_pattern) v in
@@ -321,17 +323,17 @@ let coerce_to_quantified_hypothesis v =
   else if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else match Value.to_constr v with
-  | Some c when isVar c -> NamedHyp (destVar c)
+  | Some c when isVar sigma c -> NamedHyp (destVar sigma c)
   | _ -> raise (CannotCoerceTo "a quantified hypothesis")
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env v =
+let coerce_to_decl_or_quant_hyp env sigma v =
   let v = Value.normalize v in
   if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else
-    try coerce_to_quantified_hypothesis v
+    try coerce_to_quantified_hypothesis sigma v
     with CannotCoerceTo _ ->
       raise (CannotCoerceTo "a declared or quantified hypothesis")
 
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 0b67f8726..9c4ac5265 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open EConstr
 open Misctypes
 open Pattern
 open Genarg
@@ -50,14 +51,14 @@ end
 
 val coerce_to_constr_context : Value.t -> constr
 
-val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
+val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
+val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
-  Environ.env -> Value.t -> intro_pattern_naming_expr
+  Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr
 
 val coerce_to_hint_base : Value.t -> string
 
@@ -70,27 +71,27 @@ val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
 val coerce_to_evaluable_ref :
-  Environ.env -> Value.t -> evaluable_global_reference
+  Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference
 
 val coerce_to_constr_list : Environ.env -> Value.t -> constr list
 
 val coerce_to_intro_pattern_list :
-  Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
+  Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
 
-val coerce_to_hyp : Environ.env -> Value.t -> Id.t
+val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
+val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
 
-val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
+val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference
 
-val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
+val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis
 
-val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
+val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
 
 val coerce_to_int_or_var_list : Value.t -> int or_var list
 
 (** {5 Missing generic arguments} *)
 
-val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
+val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
 
 val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index e23992a80..8aefe7605 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -120,9 +120,9 @@ type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr *
 type 'a delayed_open = 'a Tactypes.delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
-type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
 
-type delayed_open_constr = Term.constr delayed_open
+type delayed_open_constr = EConstr.constr delayed_open
 
 type intro_pattern = delayed_open_constr intro_pattern_expr located
 type intro_patterns = delayed_open_constr intro_pattern_expr located list
@@ -354,7 +354,7 @@ type raw_tactic_arg =
 
 (** Interpreted tactics *)
 
-type t_trm = Term.constr
+type t_trm = EConstr.constr
 type t_pat = constr_pattern
 type t_cst = evaluable_global_reference
 type t_ref = ltac_constant located
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fe10f0c31..50f43931e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -239,12 +239,12 @@ let pr_value env v =
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
     match env with
-    | Some (env,sigma) -> pr_lconstr_env env sigma c
+    | Some (env,sigma) -> pr_leconstr_env env sigma c
     | _ -> str "a term"
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
     match env with
-    | Some (env,sigma) -> pr_lconstr_env env sigma c
+    | Some (env,sigma) -> pr_leconstr_env env sigma c
     | _ -> str "a term"
   else if has_type v (topwit wit_constr_under_binders) then
     let c = out_gen (topwit wit_constr_under_binders) v in
@@ -282,7 +282,7 @@ let pr_inspect env expr result =
 
 (* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
-  Term.mkVar (let _ = Environ.lookup_named id env in id)
+  EConstr.mkVar (let _ = Environ.lookup_named id env in id)
 
 (** Generic arguments : table of interpretation functions *)
 
@@ -385,7 +385,7 @@ let interp_ltac_var coerce ist env locid =
   with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
 
 let interp_ident ist env sigma id =
-  try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id)
+  try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (dloc,id)
   with Not_found -> id
 
 (* Interprets an optional identifier, bound or fresh *)
@@ -394,11 +394,11 @@ let interp_name ist env sigma = function
   | Name id -> Name (interp_ident ist env sigma id)
 
 let interp_intro_pattern_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id)
+  try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id)
   with Not_found -> IntroNaming (IntroIdentifier id)
 
 let interp_intro_pattern_naming_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id)
+  try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id)
   with Not_found -> IntroIdentifier id
 
 let interp_int ist locid =
@@ -423,14 +423,14 @@ let interp_int_or_var_list ist l =
 (* Interprets a bound variable (especially an existing hypothesis) *)
 let interp_hyp ist env sigma (loc,id as locid) =
   (* Look first in lfun for a value coercible to a variable *)
-  try try_interp_ltac_var (coerce_to_hyp env) ist (Some (env,sigma)) locid
+  try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
   else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env sigma (loc,id as x) =
-  try coerce_to_hyp_list env (Id.Map.find id ist.lfun)
+  try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
   with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x]
 
 let interp_hyp_list ist env sigma l =
@@ -445,7 +445,7 @@ let interp_move_location ist env sigma = function
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar (loc, id) ->
-    try try_interp_ltac_var (coerce_to_reference env) ist (Some (env,sigma)) (loc, id)
+    try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id)
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
@@ -469,7 +469,7 @@ let interp_evaluable ist env sigma = function
     end
   | ArgArg (r,None) -> r
   | ArgVar (loc, id) ->
-    try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id)
+    try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
       with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
@@ -540,7 +540,7 @@ let default_fresh_id = Id.of_string "H"
 
 let interp_fresh_id ist env sigma l =
   let extract_ident ist env sigma id =
-    try try_interp_ltac_var (coerce_to_ident_not_fresh sigma env)
+    try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
 			    ist (Some (env,sigma)) (dloc,id)
     with Not_found -> id in
   let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
@@ -561,24 +561,24 @@ let interp_fresh_id ist env sigma l =
   Tactics.fresh_id_in_env avoid id env
 
 (* Extract the uconstr list from lfun *)
-let extract_ltac_constr_context ist env =
+let extract_ltac_constr_context ist env sigma =
   let open Glob_term in
-  let add_uconstr id env v map =
+  let add_uconstr id v map =
     try Id.Map.add id (coerce_to_uconstr env v) map
     with CannotCoerceTo _ -> map
   in
-  let add_constr id env v map =
+  let add_constr id v map =
     try Id.Map.add id (coerce_to_constr env v) map
     with CannotCoerceTo _ -> map
   in
-  let add_ident id env v map =
-    try Id.Map.add id (coerce_var_to_ident false env v) map
+  let add_ident id v map =
+    try Id.Map.add id (coerce_var_to_ident false env sigma v) map
     with CannotCoerceTo _ -> map
   in
   let fold id v {idents;typed;untyped} =
-    let idents = add_ident id env v idents in
-    let typed = add_constr id env v typed in
-    let untyped = add_uconstr id env v untyped in
+    let idents = add_ident id v idents in
+    let typed = add_constr id v typed in
+    let untyped = add_uconstr id v untyped in
     { idents ; typed ; untyped }
   in
   let empty =  { idents = Id.Map.empty ;typed = Id.Map.empty ; untyped = Id.Map.empty } in
@@ -586,11 +586,11 @@ let extract_ltac_constr_context ist env =
 
 (** Significantly simpler than [interp_constr], to interpret an
     untyped constr, it suffices to adjoin a closure environment. *)
-let interp_uconstr ist env = function
+let interp_uconstr ist env sigma = function
   | (term,None) ->
-      { closure = extract_ltac_constr_context ist env ; term }
+      { closure = extract_ltac_constr_context ist env sigma; term }
   | (_,Some ce) ->
-      let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env in
+      let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env sigma in
       let ltacvars = {
         Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
@@ -598,7 +598,7 @@ let interp_uconstr ist env = function
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
-  let constrvars = extract_ltac_constr_context ist env in
+  let constrvars = extract_ltac_constr_context ist env sigma in
   let vars = {
     Pretyping.ltac_constrs = constrvars.typed;
     Pretyping.ltac_uconstrs = constrvars.untyped;
@@ -639,7 +639,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   (* spiwack: to avoid unnecessary modifications of tacinterp, as this
      function already use effect, I call [run] hoping it doesn't mess
      up with any assumption. *)
-  Proofview.NonLogical.run (db_constr (curr_debug ist) env c);
+  Proofview.NonLogical.run (db_constr (curr_debug ist) env evd c);
   (evd,c)
 
 let constr_flags () = {
@@ -691,7 +691,9 @@ let interp_pure_open_constr ist =
 let interp_typed_pattern ist env sigma (_,c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
-  pattern_of_constr env sigma c
+  (** FIXME: it is necessary to be unsafe here because of the way we handle
+      evars in the pretyper. Sometimes they get solved eagerly. *)
+  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 
 (* Interprets a constr expression *)
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
@@ -733,10 +735,10 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
          prioritary to an evaluable reference and otherwise to a constr
          (it is an encoding to satisfy the "union" type given to Simpl) *)
     let coerce_eval_ref_or_constr x =
-      try Inl (coerce_to_evaluable_ref env x)
+      try Inl (coerce_to_evaluable_ref env sigma x)
       with CannotCoerceTo _ ->
         let c = coerce_to_closed_constr env x in
-        Inr (pattern_of_constr env sigma c) in
+        Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
      with Not_found ->
        error_global_not_found ~loc (qualid_of_ident id))
@@ -789,9 +791,11 @@ let interp_may_eval f ist env sigma = function
       (try
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+	let ctxt = EConstr.Unsafe.to_constr ctxt in
 	let evdref = ref sigma in
+	let ic = EConstr.Unsafe.to_constr ic in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.e_solve_evars env evdref c in
+	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
 	!evdref , c
       with
 	| Not_found ->
@@ -799,7 +803,8 @@ let interp_may_eval f ist env sigma = function
 	    (str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
-      Typing.type_of ~refresh:true env sigma c_interp
+      let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in
+      (sigma, t)
   | ConstrTerm c ->
      try
 	f ist env sigma c
@@ -829,7 +834,7 @@ let interp_constr_may_eval ist env sigma c =
     (* spiwack: to avoid unnecessary modifications of tacinterp, as this
        function already use effect, I call [run] hoping it doesn't mess
        up with any assumption. *)
-    Proofview.NonLogical.run (db_constr (curr_debug ist) env csr);
+    Proofview.NonLogical.run (db_constr (curr_debug ist) env sigma csr);
     sigma , csr
   end
 
@@ -841,10 +846,10 @@ let rec message_of_value v =
     Ftactic.return (str "<tactic>")
   else if has_type v (topwit wit_constr) then
     let v = out_gen (topwit wit_constr) v in
-    Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) v) end }
+    Ftactic.enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
   else if has_type v (topwit wit_constr_under_binders) then
     let c = out_gen (topwit wit_constr_under_binders) v in
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
     end }
   else if has_type v (topwit wit_unit) then
@@ -853,22 +858,25 @@ let rec message_of_value v =
     Ftactic.return (int (out_gen (topwit wit_int) v))
   else if has_type v (topwit wit_intro_pattern) then
     let p = out_gen (topwit wit_intro_pattern) v in
-    let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in
-    Ftactic.nf_enter { enter = begin fun gl ->
+    let print env sigma c =
+      let (c, sigma) = Tactics.run_delayed env sigma c in
+      pr_econstr_env env sigma c
+    in
+    Ftactic.enter { enter = begin fun gl ->
       Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
     end }
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) c) end }
+    Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
   else if has_type v (topwit wit_uconstr) then
     let c = out_gen (topwit wit_uconstr) v in
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       Ftactic.return (pr_closed_glob_env (pf_env gl)
                         (project gl) c)
     end }
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
-    Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
+    Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
   else match Value.to_list v with
   | Some l ->
     Ftactic.List.map message_of_value l >>= fun l ->
@@ -933,7 +941,7 @@ and interp_or_and_intro_pattern ist env sigma = function
 
 and interp_intro_pattern_list_as_list ist env sigma = function
   | [loc,IntroNaming (IntroIdentifier id)] as l ->
-      (try sigma, coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun)
+      (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ ->
          List.fold_map (interp_intro_pattern ist env) sigma l)
   | l -> List.fold_map (interp_intro_pattern ist env) sigma l
@@ -945,7 +953,7 @@ let interp_intro_pattern_naming_option ist env sigma = function
 let interp_or_and_intro_pattern_option ist env sigma = function
   | None -> sigma, None
   | Some (ArgVar (loc,id)) ->
-      (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
+      (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with
       | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
       | _ ->
         user_err ~loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
@@ -963,31 +971,25 @@ let interp_in_hyp_as ist env sigma (id,ipat) =
   let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
   sigma,(interp_hyp ist env sigma id,ipat)
 
-let interp_quantified_hypothesis ist = function
-  | AnonHyp n -> AnonHyp n
-  | NamedHyp id ->
-      try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
-      with Not_found -> NamedHyp id
-
-let interp_binding_name ist = function
+let interp_binding_name ist sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       (* If a name is bound, it has to be a quantified hypothesis *)
       (* user has to use other names for variables if these ones clash with *)
       (* a name intented to be used as a (non-variable) identifier *)
-      try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
+      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(dloc,id)
       with Not_found -> NamedHyp id
 
 let interp_declared_or_quantified_hypothesis ist env sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var
-	    (coerce_to_decl_or_quant_hyp env) ist (Some (env,sigma)) (dloc,id)
+	    (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id)
       with Not_found -> NamedHyp id
 
 let interp_binding ist env sigma (loc,b,c) =
   let sigma, c = interp_open_constr ist env sigma c in
-  sigma, (loc,interp_binding_name ist b,c)
+  sigma, (loc,interp_binding_name ist sigma b,c)
 
 let interp_bindings ist env sigma = function
 | NoBindings ->
@@ -1213,7 +1215,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
          end
   | TacAbstract (tac,ido) ->
-      Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT
+      Proofview.Goal.enter { enter = begin fun gl -> Tactics.tclABSTRACT
         (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
       end }
   | TacThen (t1,t) ->
@@ -1355,7 +1357,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
       Ftactic.s_enter { s_enter = begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        let c = interp_uconstr ist env c in
+        let c = interp_uconstr ist env (Sigma.to_evar_map sigma) c in
         let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in
         Sigma (Ftactic.return (Value.of_constr c), sigma, p)
       end }
@@ -1528,7 +1530,7 @@ and interp_match ist lz constr lmr =
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       let sigma = project gl in
       let env = Proofview.Goal.env gl in
       let hyps = Proofview.Goal.hyps gl in
@@ -1593,7 +1595,7 @@ and interp_genarg_var_list ist x =
   end }
 
 (* Interprets tactic expressions : returns a "constr" *)
-and interp_ltac_constr ist e : constr Ftactic.t =
+and interp_ltac_constr ist e : EConstr.t Ftactic.t =
   let (>>=) = Ftactic.bind in
   begin Proofview.tclORELSE
       (val_interp ist e)
@@ -1621,7 +1623,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
       debugging_step ist (fun () ->
         Pptactic.pr_glob_tactic env e ++ fnl() ++
           str " has value " ++ fnl() ++
-          pr_constr_env env sigma cresult)
+          pr_econstr_env env sigma cresult)
     end <*>
     Ftactic.return cresult
   with CannotCoerceTo _ ->
@@ -1641,7 +1643,8 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic =
   | Some e -> Proofview.tclUNIT e
   | None -> Proofview.tclENV
   end >>= fun env ->
-  let name () = Pptactic.pr_atomic_tactic env tacexpr in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let name () = Pptactic.pr_atomic_tactic env sigma tacexpr in
   Proofview.Trace.name_tactic name tac
 
 (* Interprets a primitive tactic *)
@@ -1756,8 +1759,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (Tactics.generalize_gen cl)) sigma
       end }
   | TacLetTac (na,c,clp,b,eqpat) ->
-      Proofview.V82.nf_evar_goals <*>
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let clp = interp_clause ist env sigma clp in
@@ -1794,7 +1796,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
          prenormalised. *)
-      Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
@@ -1830,8 +1831,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacChange (None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-      Proofview.V82.nf_evar_goals <*>
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
         let is_onhyps = match cl.onhyps with
           | None | Some [] -> true
           | _ -> false
@@ -1860,7 +1860,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacChange (Some op,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-      Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
@@ -1905,7 +1904,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
                 by))
       end }
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let (sigma,c_interp) =
@@ -2053,7 +2052,7 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
   Sigma.Unsafe.of_pair (c, sigma)
   }
 
-let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl ->
+let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl ->
   Ftactic.return (interp_destruction_arg ist gl c)
 end }
 
@@ -2087,8 +2086,8 @@ let () =
   register_interp0 wit_ltac interp
 
 let () =
-  register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
-    Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
+  register_interp0 wit_uconstr (fun ist c -> Ftactic.enter { enter = begin fun gl ->
+    Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c)
   end })
 
 (***************************************************************************)
@@ -2112,7 +2111,8 @@ let _ =
     if Genarg.has_type arg (glbwit wit_tactic) then
       let tac = Genarg.out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
-      Pfedit.refine_by_tactic env sigma ty tac
+      let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
+      (EConstr.of_constr c, sigma)
     else
       failwith "not a tactic"
   in
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index adbd1d32b..1e5f6bd42 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -9,6 +9,7 @@
 open Names
 open Tactic_debug
 open Term
+open EConstr
 open Tacexpr
 open Genarg
 open Redexpr
@@ -79,7 +80,7 @@ val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
 
 val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
-  glob_constr_and_expr with_bindings -> Evd.evar_map * constr with_bindings
+  glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings
 
 (** Initial call for interpretation *)
 
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5cbddc7f6..b2601ad32 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -51,7 +51,7 @@ let db_pr_goal gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let penv = print_named_context env in
-  let pc = print_constr_env env concl in
+  let pc = print_constr_env env (Tacmach.New.project gl) concl in
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
@@ -223,11 +223,11 @@ let is_debug db =
       return (Int.equal skip 0)
 
 (* Prints a constr *)
-let db_constr debug env c =
+let db_constr debug env sigma c =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
+    msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c)
   else return ()
 
 (* Prints the pattern rule *)
@@ -247,20 +247,20 @@ let hyp_bound = function
   | Name id -> str " (bound to " ++ pr_id id ++ str ")"
 
 (* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,_,c) ido =
+let db_matched_hyp debug env sigma (id,_,c) ido =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
     msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
-                str " has been matched: " ++ print_constr_env env c)
+                str " has been matched: " ++ print_constr_env env sigma c)
   else return ()
 
 (* Prints the matched conclusion *)
-let db_matched_concl debug env c =
+let db_matched_concl debug env sigma c =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
+    msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c)
   else return ()
 
 (* Prints a success message when the goal has been matched *)
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 520fb41ef..7745d9b7b 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -11,6 +11,7 @@ open Pattern
 open Names
 open Tacexpr
 open Term
+open EConstr
 open Evd
 
 (** TODO: Move those definitions somewhere sensible *)
@@ -34,7 +35,7 @@ val debug_prompt :
 val db_initialize : unit Proofview.NonLogical.t
 
 (** Prints a constr *)
-val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t
+val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
@@ -42,10 +43,10 @@ val db_pattern_rule :
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
+  debug_info -> env -> evar_map -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
 
 (** Prints the matched conclusion *)
-val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t
+val db_matched_concl : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t
 
 (** Prints a success message when the goal has been matched *)
 val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index ef45ee47e..5b5cd06cc 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
   subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Id.Map.t;
-  terms : Term.constr Id.Map.t;
+  context : EConstr.constr Id.Map.t;
+  terms : EConstr.constr Id.Map.t;
   lhs : 'a;
 }
 
@@ -285,7 +285,7 @@ module PatternMatching (E:StaticEnvironment) = struct
     let id = NamedDecl.get_id decl in
     let refresh = is_local_def decl in
     pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
-    put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+    put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
     return id
 
   (** [hyp_match_type hypname bodypat typepat hyps] matches a single
@@ -297,7 +297,7 @@ module PatternMatching (E:StaticEnvironment) = struct
       | LocalDef (id,body,hyp) ->
           pattern_match_term false bodypat body () <*>
           pattern_match_term true typepat hyp () <*>
-          put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+          put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
           return id
       | LocalAssum (id,hyp) -> fail
 
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 090207bcc..300b546f1 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -18,8 +18,8 @@
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
   subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Names.Id.Map.t;
-  terms : Term.constr Names.Id.Map.t;
+  context : EConstr.constr Names.Id.Map.t;
+  terms : EConstr.constr Names.Id.Map.t;
   lhs : 'a;
 }
 
@@ -31,7 +31,7 @@ type 'a t = {
 val match_term :
   Environ.env ->
   Evd.evar_map ->
-  Term.constr ->
+  EConstr.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
 
@@ -43,7 +43,7 @@ val match_term :
 val match_goal:
   Environ.env ->
   Evd.evar_map ->
-  Context.Named.t ->
-  Term.constr ->
+  EConstr.named_context ->
+  EConstr.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index fb05fd7d0..dc7ee6a23 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Hipattern
 open Names
 open Pp
@@ -16,6 +17,7 @@ open Tacexpr
 open Tacinterp
 open Util
 open Tacticals.New
+open Proofview.Notations
 
 let tauto_plugin = "tauto"
 let () = Mltop.add_known_module tauto_plugin
@@ -111,19 +113,21 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings]
 (** Test *)
 
 let is_empty _ ist =
-  if is_empty_type (assoc_var "X1" ist) then idtac else fail
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail
 
 (* Strictly speaking, this exceeds the propositional fragment as it
    matches also equality types (and solves them if a reflexivity) *)
 let is_unit_or_eq _ ist =
+  Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
-  if test (assoc_var "X1" ist) then idtac else fail
+  if test sigma (assoc_var "X1" ist) then idtac else fail
 
-let bugged_is_binary t =
-  isApp t &&
-  let (hdapp,args) = decompose_app t in
-    match (kind_of_term hdapp) with
+let bugged_is_binary sigma t =
+  isApp sigma t &&
+  let (hdapp,args) = decompose_app sigma t in
+    match EConstr.kind sigma hdapp with
     | Ind (ind,u)  ->
         let (mib,mip) = Global.lookup_inductive ind in
          Int.equal mib.Declarations.mind_nparams 2
@@ -132,21 +136,23 @@ let bugged_is_binary t =
 (** Dealing with conjunction *)
 
 let is_conj _ ist =
+  Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let ind = assoc_var "X1" ist in
-    if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) &&
-       is_conjunction
+    if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) &&
+       is_conjunction sigma
          ~strict:flags.strict_in_hyp_and_ccl
          ~onlybinary:flags.binary_mode ind
     then idtac
     else fail
 
 let flatten_contravariant_conj _ ist =
+  Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_conjunction
+  match match_with_conjunction sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode typ
   with
@@ -154,27 +160,29 @@ let flatten_contravariant_conj _ ist =
     let newtyp = List.fold_right mkArrow args c in
     let intros = tclMAP (fun _ -> intro) args in
     let by = tclTHENLIST [intros; apply hyp; split; assumption] in
-    tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)]
+    tclTHENLIST [assert_ ~by newtyp; clear (destVar sigma hyp)]
   | _ -> fail
 
 (** Dealing with disjunction *)
 
 let is_disj _ ist =
+  Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let t = assoc_var "X1" ist in
-  if (not flags.binary_mode_bugged_detection || bugged_is_binary t) &&
-     is_disjunction
+  if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) &&
+     is_disjunction sigma
        ~strict:flags.strict_in_hyp_and_ccl
        ~onlybinary:flags.binary_mode t
   then idtac
   else fail
 
 let flatten_contravariant_disj _ ist =
+  Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_disjunction
+  match match_with_disjunction sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode
           typ with
@@ -186,7 +194,7 @@ let flatten_contravariant_disj _ ist =
         assert_ ~by typ
       in
       let tacs = List.mapi map args in
-      let tac0 = clear (destVar hyp) in
+      let tac0 = clear (destVar sigma hyp) in
       tclTHEN (tclTHENLIST tacs) tac0
   | _ -> fail
 
@@ -217,6 +225,7 @@ let apply_nnpp _ ist =
     (Proofview.tclUNIT ())
     begin fun () -> try
       let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
+      let nnpp = EConstr.of_constr nnpp in
       apply nnpp
     with Not_found -> tclFAIL 0 (Pp.mt ())
     end