Clenv API using EConstr.

9 files changed, 113 insertions, 58 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7462b8d85..2b654f563 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -84,11 +84,12 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       (** Refresh the instance of the hint *)
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
       let map c = Vars.subst_univs_level_constr subst c in
+      let emap c = EConstr.Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       (** Only metas are mentioning the old universes. *)
       let clenv = {
-        templval = Evd.map_fl map clenv.templval;
-        templtyp = Evd.map_fl map clenv.templtyp;
+        templval = Evd.map_fl emap clenv.templval;
+        templtyp = Evd.map_fl emap clenv.templtyp;
         evd = Evd.map_metas map evd;
         env = Proofview.Goal.env gl;
       } in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 80b9ec06e..b567344c9 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -257,12 +257,12 @@ type hypinfo = {
 
 let decompose_applied_relation metas env sigma c ctype left2right =
   let find_rel ty =
-    let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
+    let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr ty) in
     let eqclause =
       if metas then eqclause
       else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
     in
-    let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+    let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
     let rec split_last_two = function
       | [c1;c2] -> [],(c1, c2)
       | x::y::z ->
@@ -276,7 +276,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
 	in
 (* 	  if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
 (* 	  else *)
-	    Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
+	    Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
 		   hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
 		   hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
       with Not_found -> None
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a2699ba8d..a8768b6ed 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -227,6 +227,7 @@ let e_give_exact flags poly (c,clenv) gl =
     else c, gl
   in
   let t1 = pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t1 = EConstr.of_constr t1 in
   Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
@@ -247,6 +248,7 @@ let unify_resolve_refine poly flags =
   { enter = begin fun gls ((c, t, ctx),n,clenv) ->
     let env = Proofview.Goal.env gls in
     let concl = Proofview.Goal.concl gls in
+    let concl = EConstr.of_constr concl in
     Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
       let sigma = Sigma.to_evar_map sigma in
       let sigma, term, ty =
@@ -259,17 +261,20 @@ let unify_resolve_refine poly flags =
           let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
           sigma, c, t
       in
+      let open EConstr in
+      let ty = EConstr.of_constr ty in
+      let term = EConstr.of_constr term in
       let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
-      let term = applistc term (List.map (fun x -> x.hole_evar) cl.cl_holes) in
+      let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
         let evdref = ref sigma' in
         if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
-                                      evdref (EConstr.of_constr cl.cl_concl) (EConstr.of_constr concl)) then
-          Type_errors.error_actual_type env
+                                      evdref cl.cl_concl concl) then
+          Pretype_errors.error_actual_type_core env sigma'
             {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
             concl;
         !evdref
-      in Sigma.here (EConstr.of_constr term) (Sigma.Unsafe.of_evar_map sigma') }
+      in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
   end }
 
 (** Dealing with goals of the form A -> B and hints of the form
@@ -279,9 +284,11 @@ let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some (None, clenv)
   else
+    let c = EConstr.of_constr c in
     let sigma = Tacmach.New.project gl in
-    let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma (EConstr.of_constr c) in
-    let diff = nb_prod sigma (EConstr.of_constr ty) - nprods in
+    let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+    let ty = EConstr.of_constr ty in
+    let diff = nb_prod sigma ty - nprods in
     if Pervasives.(>=) diff 0 then
       (* Was Some clenv... *)
       Some (Some diff,
@@ -1515,7 +1522,7 @@ let autoapply c i gl =
   let flags = auto_unif_flags Evar.Set.empty
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
   let cty = pf_unsafe_type_of gl (EConstr.of_constr c) in
-  let ce = mk_clenv_from gl (c,cty) in
+  let ce = mk_clenv_from gl (EConstr.of_constr c,EConstr.of_constr cty) in
   let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
     ((c,cty,Univ.ContextSet.empty),0,ce) } in
   Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2fad4fcf7..7b07c9309 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -31,9 +31,10 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t1 = EConstr.of_constr t1 in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
-  if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
+  if occur_existential sigma t1 || occur_existential sigma (EConstr.of_constr t2) then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ad80d2d1f..fbf461f6f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -144,7 +144,7 @@ let freeze_initial_evars sigma flags clause =
   (* We take evars of the type: this may include old evars! For excluding *)
   (* all old evars, including the ones occurring in the rewriting lemma, *)
   (* we would have to take the clenv_value *)
-  let newevars = Evd.evars_of_term (clenv_type clause) in
+  let newevars = Evd.evars_of_term (EConstr.Unsafe.to_constr (clenv_type clause)) in
   let evars =
     fold_undefined (fun evk _ evars ->
       if Evar.Set.mem evk newevars then evars
@@ -165,8 +165,11 @@ let side_tac tac sidetac =
 
 let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let env = Proofview.Goal.env gl in
+  let c = EConstr.of_constr c in
+  let ty = EConstr.of_constr ty in
+  let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
-  let (equiv, args) = decompose_appvect (Clenv.clenv_type eqclause) in
+  let (equiv, args) = decompose_appvect (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
   let arglen = Array.length args in
   let () = if arglen < 2 then error "The term provided is not an applied relation." in
   let c1 = args.(arglen - 2) in
@@ -181,8 +184,11 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let sigma, ct = pf_type_of gl (EConstr.of_constr c) in
+  let c = EConstr.of_constr c in
+  let sigma, ct = pf_type_of gl c in
   let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
+  let t = EConstr.of_constr t in
+  let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -975,9 +981,11 @@ let eq_baseid = Id.of_string "e"
 
 let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
+  let f = EConstr.of_constr f in
+  let t = EConstr.of_constr t in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.evd (EConstr.of_constr f_clause.templval.Evd.rebus)) with
+    (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
@@ -992,7 +1000,6 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
-  let pf = EConstr.of_constr pf in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
@@ -1011,13 +1018,17 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let c = EConstr.of_constr c in
+  let lbindc = Miscops.map_bindings EConstr.of_constr lbindc in
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
-  let t = type_of (EConstr.of_constr c) in
+  let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
+  let t' = EConstr.of_constr t' in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
+  let eqn = EConstr.Unsafe.to_constr eqn in
   let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
@@ -1371,7 +1382,8 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
-      let ty = simplify_args env sigma (clenv_type inj_clause) in
+      let ty = simplify_args env sigma (EConstr.Unsafe.to_constr (clenv_type inj_clause)) in
+      let pf = EConstr.Unsafe.to_constr pf in
 	evdref := sigma;
 	Some (pf, ty)
     with Failure _ -> None
@@ -1405,7 +1417,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
      tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
-	(tac (clenv_value eq_clause))
+	(tac (EConstr.Unsafe.to_constr (clenv_value eq_clause)))
 
 let get_previous_hyp_position id gl =
   let rec aux dest = function
@@ -1464,10 +1476,10 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-        ntac (clenv_value clause) 0
+        ntac (EConstr.Unsafe.to_constr (clenv_value clause)) 0
     | Inr posns ->
 	inject_at_positions env sigma true u clause posns
-          (ntac (clenv_value clause))
+          (ntac (EConstr.Unsafe.to_constr (clenv_value clause)))
   end }
 
 let dEqThen with_evars ntac = function
@@ -1478,9 +1490,11 @@ let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
-let intro_decomp_eq tac data cl =
+let intro_decomp_eq tac data (c, t) =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let cl = pf_apply make_clenv_binding gl cl NoBindings in
+    let c = EConstr.of_constr c in
+    let t = EConstr.of_constr t in
+    let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
     decompEqThen (fun _ -> tac) data cl
   end }
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 57358bb76..ea95fb1ad 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -276,9 +276,11 @@ let strip_params env c =
 let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+    let c = EConstr.of_constr c in
+    let cty = EConstr.of_constr cty in
     let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
-	  { cl.templval with rebus = strip_params env cl.templval.rebus };
+	  { cl.templval with rebus = EConstr.of_constr (strip_params env (EConstr.Unsafe.to_constr cl.templval.rebus)) };
 	env = empty_env}
   in
   let code = match p.code.obj with
@@ -765,9 +767,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
     match kind_of_term cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
-        let ce = mk_clenv_from_env env sigma' None (c,cty) in
+        let ce = mk_clenv_from_env env sigma' None (EConstr.of_constr c,EConstr.of_constr cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.of_constr c') in
+	let pat = Patternops.pattern_of_constr env ce.evd c' in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -912,10 +914,10 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
   let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in
-  let ce = mk_clenv_from_env env sigma None (c,t) in
+  let ce = mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.of_constr (clenv_type ce)));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               db = None;
               secvars = secvars_of_constr env c;
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 85910355e..16a048af8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -258,8 +258,8 @@ let add_inversion_lemma_exn na com comsort bool tac =
 
 let lemInv id c gls =
   try
-    let clause = mk_clenv_type_of gls c in
-    let clause = clenv_constrain_last_binding (mkVar id) clause in
+    let clause = mk_clenv_type_of gls (EConstr.of_constr c) in
+    let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 02909243d..459947051 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -622,20 +622,22 @@ module New = struct
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
       isrec allnames tac predicate ind (c, t) =
+    let c = EConstr.of_constr c in
+    let t = EConstr.of_constr t in
     Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Proofview.Goal.nf_enter { enter = begin fun gl ->
     let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim))) gl in
+    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (EConstr.of_constr elim,EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim)))) gl in
     let indmv =
-      match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with
+      match kind_of_term (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
       | _         -> anomaly (str"elimination")
     in
     let pmv =
-      let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
+      let p, _ = decompose_app (EConstr.Unsafe.to_constr elimclause.templtyp.Evd.rebus) in
       match kind_of_term p with
       | Meta p -> p
       | _ ->
@@ -655,11 +657,11 @@ module New = struct
     let elimclause' =
       match predicate with
       | None   -> elimclause'
-      | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
+      | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) (EConstr.of_constr p) elimclause'
     in
     let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
     let after_tac i =
-      let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
+      let (hd,largs) = decompose_app (EConstr.Unsafe.to_constr clenv'.templtyp.Evd.rebus) in
       let ba = { branchsign = branchsigns.(i);
                  branchnames = brnames.(i);
                  nassums = List.length branchsigns.(i);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b9a219a2c..f262aefa7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1301,11 +1301,11 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
     else clenv
   in
   let new_hyp_typ = clenv_type clenv in
+  let new_hyp_typ = EConstr.Unsafe.to_constr new_hyp_typ in
   if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
   if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
-  let new_hyp_prf = EConstr.of_constr new_hyp_prf in
   let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
   let naming = NamingMustBe (dloc,targetid) in
   let with_clear = do_replace (Some id) naming in
@@ -1396,9 +1396,12 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let elim = contract_letin_in_lam_header elim in
+  let bindings = Miscops.map_bindings EConstr.of_constr bindings in
+  let elim = EConstr.of_constr elim in
+  let elimty = EConstr.of_constr elimty in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv =
-    (match kind_of_term (nth_arg i elimclause.templval.rebus) with
+    (match kind_of_term (nth_arg i (EConstr.Unsafe.to_constr elimclause.templval.rebus)) with
        | Meta mv -> mv
        | _  -> user_err ~hdr:"elimination_clause"
              (str "The type of elimination clause is not well-formed."))
@@ -1438,8 +1441,10 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   let sigma = Tacmach.New.project gl in
   let ct = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let t = try snd (reduce_to_quantified_ind env sigma (EConstr.of_constr ct)) with UserError _ -> ct in
+  let t = EConstr.of_constr t in
   let elimtac = elimination_clause_scheme with_evars in
-  let indclause  = make_clenv_binding env sigma (c, t) lbindc in
+  let lbindc = Miscops.map_bindings EConstr.of_constr lbindc in
+  let indclause  = make_clenv_binding env sigma (EConstr.of_constr c, t) lbindc in
   let sigma = meta_merge sigma (clear_metas indclause.evd) in
   Proofview.Unsafe.tclEVARS sigma <*>
   Tacticals.New.tclTHEN
@@ -1561,8 +1566,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let elim = contract_letin_in_lam_header elim in
+  let elim = EConstr.of_constr elim in
+  let elimty = EConstr.of_constr elimty in
+  let bindings = Miscops.map_bindings EConstr.of_constr bindings in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
-  let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
+  let indmv = destMeta (nth_arg i (EConstr.Unsafe.to_constr elimclause.templval.rebus)) in
   let hypmv =
     try match List.remove Int.equal indmv (clenv_independent elimclause) with
       | [a] -> a
@@ -1570,12 +1578,13 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
     with Failure _ -> user_err ~hdr:"elimination_clause"
           (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
-  let hyp = mkVar id in
-  let hyp_typ = Retyping.get_type_of env sigma (EConstr.of_constr hyp) in
+  let hyp = EConstr.mkVar id in
+  let hyp_typ = Retyping.get_type_of env sigma hyp in
+  let hyp_typ = EConstr.of_constr hyp_typ in
   let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
-  if Term.eq_constr hyp_typ new_hyp_typ then
+  if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
     user_err ~hdr:"general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id id sigma elimclause''
@@ -1728,9 +1737,11 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
     let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) in
     let try_apply thm_ty nprod =
       try
-        let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in
+        let thm_ty = EConstr.of_constr thm_ty in
+        let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
         if n<0 then error "Applied theorem has not enough premisses.";
-        let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
+        let lbind = Miscops.map_bindings EConstr.of_constr lbind in
+        let clause = make_clenv_binding_apply env sigma (Some n) (EConstr.of_constr c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
       with exn when catchable_exception exn ->
         Proofview.tclZERO exn
@@ -1851,7 +1862,9 @@ let progress_with_clause flags innerclause clause =
   with Not_found -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause env sigma (d,lbind) =
-  let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr d))) in
+  let d = EConstr.of_constr d in
+  let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma d)) in
+  let thm = EConstr.of_constr thm in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
@@ -1859,6 +1872,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> iraise e
   in
+  let lbind = Miscops.map_bindings EConstr.of_constr lbind in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
 let apply_in_once sidecond_first with_delta with_destruct with_evars naming
@@ -1870,7 +1884,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
   let flags =
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
-  let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
+  let innerclause = mk_clenv_from_env env sigma (Some 0) (EConstr.mkVar id,EConstr.of_constr t') in
   let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
   let rec aux idstoclear with_destruct c =
     Proofview.Goal.enter { enter = begin fun gl ->
@@ -2939,10 +2953,12 @@ let specialize (c,lbind) ipat =
       let sigma = Typeclasses.resolve_typeclasses env sigma in
       sigma, nf_evar sigma c
     else
-      let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma (EConstr.of_constr c)) lbind in
+      let c = EConstr.of_constr c in
+      let lbind = Miscops.map_bindings EConstr.of_constr lbind in
+      let clause = make_clenv_binding env sigma (c,EConstr.of_constr (Retyping.get_type_of env sigma c)) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
-      let (thd,tstack) = whd_nored_stack clause.evd (EConstr.of_constr (clenv_value clause)) in
+      let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
       let rec chk = function
       | [] -> []
       | t::l -> if occur_meta clause.evd t then [] else EConstr.Unsafe.to_constr t :: chk l
@@ -4107,7 +4123,7 @@ let get_eliminator elim dep s gl =
    of lid are parameters (first ones), the other are
    arguments. Returns the clause obtained.  *)
 let recolle_clenv i params args elimclause gl =
-  let _,arr = destApp elimclause.templval.rebus in
+  let _,arr = destApp (EConstr.Unsafe.to_constr elimclause.templval.rebus) in
   let lindmv =
     Array.map
       (fun x ->
@@ -4132,6 +4148,8 @@ let recolle_clenv i params args elimclause gl =
       (* from_n (Some 0) means that x should be taken "as is" without
          trying to unify (which would lead to trying to apply it to
          evars if y is a product). *)
+      let x = EConstr.of_constr x in
+      let y = EConstr.of_constr y in
       let indclause  = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in
       let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
       elimclause')
@@ -4149,6 +4167,9 @@ let induction_tac with_evars params indvars elim =
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimc = contract_letin_in_lam_header elimc in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
+  let elimc = EConstr.of_constr elimc in
+  let elimt = EConstr.of_constr elimt in
+  let lbindelimc = Miscops.map_bindings EConstr.of_constr lbindelimc in
   let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
   (* elimclause' is built from elimclause by instanciating all args and params. *)
   let elimclause' = recolle_clenv i params indvars elimclause gl in
@@ -4294,11 +4315,14 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
       typ in
   let rec find_clause typ =
     try
+      let typ = EConstr.of_constr typ in
+      let c = EConstr.of_constr c in
+      let lbind = Miscops.map_bindings EConstr.of_constr lbind in
       let indclause = make_clenv_binding env sigma (c,typ) lbind in
-      if must_be_closed && occur_meta indclause.evd (EConstr.of_constr (clenv_value indclause)) then
+      if must_be_closed && occur_meta indclause.evd (clenv_value indclause) then
         error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
-      let (sigma, c) = pose_all_metas_as_evars env indclause.evd (EConstr.of_constr (clenv_value indclause)) in
+      let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
       Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr c, sigma)
     with e when catchable_exception e ->
     try find_clause (try_red_product env sigma (EConstr.of_constr typ))
@@ -4308,13 +4332,15 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
 let check_expected_type env sigma (elimc,bl) elimt =
   (* Compute the expected template type of the term in case a using
      clause is given *)
-  let sign,_ = splay_prod env sigma (EConstr.of_constr elimt) in
+  let open EConstr in
+  let elimt = EConstr.of_constr elimt in
+  let sign,_ = splay_prod env sigma elimt in
   let n = List.length sign in
   if n == 0 then error "Scheme cannot be applied.";
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
-  let (_,u,_) = destProd cl.cl_concl in
-  fun t -> Evarconv.e_cumul env (ref sigma) t (EConstr.of_constr u)
+  let (_,u,_) = destProd sigma cl.cl_concl in
+  fun t -> Evarconv.e_cumul env (ref sigma) t u
 
 let check_enough_applied env sigma elim =
   let sigma = Sigma.to_evar_map sigma in
@@ -4327,6 +4353,7 @@ let check_enough_applied env sigma elim =
   | Some elimc ->
       let elimt = Retyping.get_type_of env sigma (EConstr.of_constr (fst elimc)) in
       let scheme = compute_elim_sig ~elimc elimt in
+      let elimc = Miscops.map_with_bindings EConstr.of_constr elimc in
       match scheme.indref with
       | None ->
          (* in the absence of information, do not assume it may be
@@ -4607,12 +4634,13 @@ let simple_destruct = function
 
 let elim_scheme_type elim t =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let elim = EConstr.of_constr elim in
   let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
-  match kind_of_term (last_arg clause.templval.rebus) with
+  match kind_of_term (last_arg (EConstr.Unsafe.to_constr clause.templval.rebus)) with
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
-	  clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
+	  clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL (EConstr.of_constr t)
             (clenv_meta_type clause mv) clause in
 	Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
     | _ -> anomaly (Pp.str "elim_scheme_type")