From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 proofs/clenv.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fad656223a..34bc830970 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -77,7 +77,7 @@ let clenv_push_prod cl =
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
 	let mv = new_meta () in
-	let dep = dependent (mkRel 1) u in
+	let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) in
 	let na' = if dep then na else Anonymous in
 	let e' = meta_declare mv t ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
@@ -332,7 +332,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta ty then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
@@ -404,7 +404,7 @@ type arg_bindings = constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  let mvs = collect_metas (clenv_value clenv) in
+  let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -522,7 +522,7 @@ let clenv_match_args bl clenv =
 exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
-  let all_mvs = collect_metas clenv.templval.rebus in
+  let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in
   let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
@@ -612,7 +612,7 @@ let make_evar_clause env sigma ?len t =
       let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
       let sigma = Sigma.to_evar_map sigma in
-      let dep = dependent (mkRel 1) t2 in
+      let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in
       let hole = {
         hole_evar = ev;
         hole_type = t1;
@@ -682,9 +682,9 @@ let solve_evar_clause env sigma hyp_only clause = function
     if h.hole_deps then
       (** Some subsequent term uses the hole *)
       let (ev, _) = destEvar h.hole_evar in
-      let is_dep hole = occur_evar ev hole.hole_type in
+      let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in
       let in_hyp = List.exists is_dep holes in
-      let in_ccl = occur_evar ev clause.cl_concl in
+      let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in
       let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
       let h = { h with hole_deps = dep } in
       h :: holes
-- 
cgit v1.2.3


From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 proofs/clenv.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 34bc830970..d64cd9fffd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (EConstr.of_constr (clenv_type cl)) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -264,7 +264,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -482,7 +482,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -498,8 +498,8 @@ let clenv_unify_binding_type clenv c t u =
 	  TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k c =
-  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-  let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+  let k_typ = clenv_hnf_constr clenv (EConstr.of_constr (clenv_meta_type clenv k)) in
+  let c_typ = nf_betaiota clenv.evd (EConstr.of_constr (clenv_get_type_of clenv c)) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
-- 
cgit v1.2.3


From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Nov 2016 14:48:36 +0100
Subject: Retyping API using EConstr.

---
 proofs/clenv.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d64cd9fffd..f4ac094b80 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -67,7 +67,7 @@ let refresh_undefined_univs clenv =
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
-let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
+let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c)
 
 exception NotExtensibleClause
 
@@ -667,8 +667,8 @@ let evar_of_binder holes = function
     user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
-  let t = Retyping.get_type_of env sigma ev in
-  let ty = Retyping.get_type_of env sigma c in
+  let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
+  let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
   let (ev, _) = destEvar ev in
-- 
cgit v1.2.3


From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 17:21:44 +0100
Subject: Typing API using EConstr.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f4ac094b80..c2130a64a3 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -29,7 +29,7 @@ open Sigma.Notations
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c)
 
 (******************************************************************)
 (* Clausal environments *)
-- 
cgit v1.2.3


From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Nov 2016 20:33:06 +0100
Subject: Coercion API using EConstr.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c2130a64a3..0515e41986 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -670,7 +670,7 @@ let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
   let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
   let (ev, _) = destEvar ev in
   let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
-- 
cgit v1.2.3


From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 19:02:40 +0100
Subject: Pretyping API using EConstr.

---
 proofs/clenv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0515e41986..68aeaef5e1 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -337,7 +337,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = Sigma.Unsafe.of_evar_map clenv.evd in
-	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
+	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in
 	let evd = Sigma.to_evar_map evd in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
@@ -610,7 +610,7 @@ let make_evar_clause env sigma ?len t =
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
+      let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in
       let sigma = Sigma.to_evar_map sigma in
       let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in
       let hole = {
-- 
cgit v1.2.3


From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Nov 2016 11:39:27 +0100
Subject: Unification API using EConstr.

---
 proofs/clenv.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 68aeaef5e1..2d621e97cb 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -257,7 +257,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
   { clenv with
-      evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
+      evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) }
 
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
@@ -482,13 +482,15 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then
+  let u = EConstr.of_constr u in
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
     (* Enough information so as to try a coercion now *)
     try
-      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
+      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in
+      let c = EConstr.Unsafe.to_constr c in
       TypeProcessed, { clenv with evd = evd }, c
     with 
       | PretypeError (_,_,ActualTypeNotCoercible (_,_,
-- 
cgit v1.2.3


From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 00:29:02 +0100
Subject: Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
---
 proofs/clenv.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2d621e97cb..956be88c8a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -669,12 +669,14 @@ let evar_of_binder holes = function
     user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
+  let c = EConstr.of_constr c in
   let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
-  let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+  let ty = Retyping.get_type_of env sigma c in
+  let ty = EConstr.of_constr ty in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
   let (ev, _) = destEvar ev in
-  let sigma = Evd.define ev j.Environ.uj_val sigma in
+  let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
-- 
cgit v1.2.3


From 7267dfafe9215c35275a39814c8af451961e997c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 17:48:47 +0100
Subject: Goal API using EConstr.

---
 proofs/clenv.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 956be88c8a..67ed5daaa1 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -264,6 +264,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  let concl = EConstr.Unsafe.to_constr concl in
   if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
-- 
cgit v1.2.3


From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 proofs/clenv.ml | 129 +++++++++++++++++++++++++++++---------------------------
 1 file changed, 68 insertions(+), 61 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 67ed5daaa1..3e3889cbb3 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,11 +12,12 @@ open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
 open Namegen
 open Environ
 open Evd
+open EConstr
+open Vars
 open Reduction
 open Reductionops
 open Tacred
@@ -29,7 +30,7 @@ open Sigma.Notations
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c)
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
 
 (******************************************************************)
 (* Clausal environments *)
@@ -43,12 +44,6 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let map_clenv sub clenv =
-  { templval = map_fl sub clenv.templval;
-    templtyp = map_fl sub clenv.templtyp;
-    evd = cmap sub clenv.evd;
-    env = clenv.env }
-
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -56,30 +51,34 @@ let clenv_value clenv = meta_instance clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
 
 let refresh_undefined_univs clenv =
-  match kind_of_term clenv.templval.rebus with
+  match EConstr.kind clenv.evd clenv.templval.rebus with
   | Var _ -> clenv, Univ.empty_level_subst
-  | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+  | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
   | _ ->  
     let evd', subst = Evd.refresh_undefined_universes clenv.evd in
     let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
       { clenv with evd = evd'; templval = map_freelisted clenv.templval;
 	templtyp = map_freelisted clenv.templtyp }, subst
 
-let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
+let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t)
 
-let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c)
+let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
 
 exception NotExtensibleClause
 
+let mk_freelisted c =
+  map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
+
 let clenv_push_prod cl =
-  let typ = whd_all (cl_env cl) (cl_sigma cl) (EConstr.of_constr (clenv_type cl)) in
-  let rec clrec typ = match kind_of_term typ with
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = EConstr.of_constr typ in
+  let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
 	let mv = new_meta () in
-	let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) in
+	let dep = not (noccurn (cl_sigma cl) 1 u) in
 	let na' = if dep then na else Anonymous in
-	let e' = meta_declare mv t ~name:na' cl.evd in
+	let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
 	let def = applist (cl.templval.rebus,[mkMeta mv]) in
 	{ templval = mk_freelisted def;
@@ -103,14 +102,17 @@ let clenv_push_prod cl =
    and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 
 let clenv_environments evd bound t =
+  let open EConstr in
+  let open Vars in
   let rec clrec (e,metas) n t =
-    match n, kind_of_term t with
+    match n, EConstr.kind evd t with
       | (Some 0, _) -> (e, List.rev metas, t)
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = not (noccurn 1 t2) in
+	  let dep = not (noccurn evd 1 t2) in
 	  let na' = if dep then na else Anonymous in
+	  let t1 = EConstr.Unsafe.to_constr t1 in
 	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
@@ -132,7 +134,7 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t))
 
 (******************************************************************)
 
@@ -168,13 +170,13 @@ let clenv_assign mv rhs clenv =
     error "clenv_assign: circularity in unification";
   try
     if meta_defined clenv.evd mv then
-      if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+      if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
     else
       let st = (Conv,TypeNotProcessed) in
-      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+      {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
     error "clenv_assign: undefined meta"
 
@@ -219,7 +221,7 @@ let clenv_assign mv rhs clenv =
 *)
 
 let clenv_metas_in_type_of_meta evd mv =
-  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+  (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
@@ -257,15 +259,14 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
   { clenv with
-      evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) }
+      evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
 
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  let concl = EConstr.Unsafe.to_constr concl in
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then
+  if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus))))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -275,23 +276,19 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
 let adjust_meta_source evd mv = function
   | loc,Evar_kinds.VarInstance id ->
     let rec match_name c l =
-      match kind_of_term c, l with
-      | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+      match EConstr.kind evd c, l with
+      | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id
       | Lambda (_,_,c), a::l -> match_name c l
       | _ -> None in
     (* This is very ad hoc code so that an evar inherits the name of the binder
        in situations like "ex_intro (fun x => P) ?ev p" *)
     let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
       if Metaset.mem mv t.freemetas then
-        let f,l = decompose_app t.rebus in
-        match kind_of_term f with
+        let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+        match EConstr.kind evd f with
         | Meta mv'' ->
           (match meta_opt_fvalue evd mv'' with
-          | Some (c,_) -> match_name c.rebus l
-          | None -> None)
-        | Evar ev ->
-          (match existential_opt_value evd ev with
-          | Some c -> match_name c l
+          | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
           | None -> None)
         | _ -> None
       else None in
@@ -333,13 +330,14 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = Sigma.Unsafe.of_evar_map clenv.evd in
-	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in
+	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
 	let evd = Sigma.to_evar_map evd in
+	let evar = EConstr.of_constr evar in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
@@ -405,7 +403,7 @@ type arg_bindings = constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in
+  let mvs = collect_metas clenv.evd (clenv_value clenv) in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -483,15 +481,13 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  let u = EConstr.of_constr u in
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+  if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u))))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
     (* Enough information so as to try a coercion now *)
     try
-      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in
-      let c = EConstr.Unsafe.to_constr c in
+      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
       | PretypeError (_,_,ActualTypeNotCoercible (_,_,
@@ -501,9 +497,11 @@ let clenv_unify_binding_type clenv c t u =
 	  TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k c =
-  let k_typ = clenv_hnf_constr clenv (EConstr.of_constr (clenv_meta_type clenv k)) in
-  let c_typ = nf_betaiota clenv.evd (EConstr.of_constr (clenv_get_type_of clenv c)) in
+  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+  let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+  let c_typ = EConstr.of_constr c_typ in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
+  let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
@@ -516,7 +514,7 @@ let clenv_match_args bl clenv =
       (fun clenv (loc,b,c) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+          if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
@@ -525,7 +523,7 @@ let clenv_match_args bl clenv =
 exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
-  let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in
+  let all_mvs = collect_metas clenv.evd clenv.templval.rebus in
   let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
@@ -560,8 +558,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
+      let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in
       let clause = mk_clenv_from_env env sigma n
-	(c,rename_bound_vars_as_displayed [] [] t)
+	(c, t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
@@ -579,43 +578,49 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 (* Pretty-print *)
 
 let pr_clenv clenv =
+  let inj = EConstr.Unsafe.to_constr in
   h 0
-    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
-     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+    (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++
+     str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
 
 (****************************************************************)
 (** Evar version of mk_clenv *)
 
 type hole = {
-  hole_evar : constr;
-  hole_type : types;
+  hole_evar : EConstr.constr;
+  hole_type : EConstr.types;
   hole_deps  : bool;
   hole_name : Name.t;
 }
 
 type clause = {
   cl_holes : hole list;
-  cl_concl : types;
+  cl_concl : EConstr.types;
 }
 
 let make_evar_clause env sigma ?len t =
+  let open EConstr in
+  let open Vars in
   let bound = match len with
   | None -> -1
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
+  let t = EConstr.Unsafe.to_constr t in
   let t = rename_bound_vars_as_displayed [] [] t in
+  let t = EConstr.of_constr t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
-    else match kind_of_term t with
+    else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in
+      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
       let sigma = Sigma.to_evar_map sigma in
-      let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in
+      let ev = EConstr.of_constr ev in
+      let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
         hole_type = t1;
@@ -670,26 +675,28 @@ let evar_of_binder holes = function
     user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
-  let c = EConstr.of_constr c in
-  let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
+  let open EConstr in
+  let t = Retyping.get_type_of env sigma ev in
+  let t = EConstr.of_constr t in
   let ty = Retyping.get_type_of env sigma c in
   let ty = EConstr.of_constr ty in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
-  let (ev, _) = destEvar ev in
+  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+  let (ev, _) = destEvar sigma ev in
   let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
 | NoBindings -> sigma
 | ImplicitBindings largs ->
+  let open EConstr in
   let fold holes h =
     if h.hole_deps then
       (** Some subsequent term uses the hole *)
-      let (ev, _) = destEvar h.hole_evar in
-      let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in
+      let (ev, _) = destEvar sigma h.hole_evar in
+      let is_dep hole = occur_evar sigma ev hole.hole_type in
       let in_hyp = List.exists is_dep holes in
-      let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in
+      let in_ccl = occur_evar sigma ev clause.cl_concl in
       let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
       let h = { h with hole_deps = dep } in
       h :: holes
-- 
cgit v1.2.3


From 45562afa065aadc207dca4e904e309d835cb66ef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:28:45 +0100
Subject: Tacticals API using EConstr.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 3e3889cbb3..fd88e3c518 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -44,7 +44,7 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let clenv_nf_meta clenv c = nf_meta clenv.evd c
+let clenv_nf_meta clenv c = EConstr.of_constr (nf_meta clenv.evd (EConstr.Unsafe.to_constr c))
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
 let clenv_value clenv = meta_instance clenv.evd clenv.templval
-- 
cgit v1.2.3


From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 proofs/clenv.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fd88e3c518..514fc27e89 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -337,7 +337,6 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
         let evd = Sigma.Unsafe.of_evar_map clenv.evd in
 	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
 	let evd = Sigma.to_evar_map evd in
-	let evar = EConstr.of_constr evar in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
@@ -619,7 +618,6 @@ let make_evar_clause env sigma ?len t =
       let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
       let sigma = Sigma.to_evar_map sigma in
-      let ev = EConstr.of_constr ev in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
-- 
cgit v1.2.3


From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 03:04:13 +0100
Subject: Rewrite API using EConstr.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 514fc27e89..d986696604 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -44,7 +44,7 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let clenv_nf_meta clenv c = EConstr.of_constr (nf_meta clenv.evd (EConstr.Unsafe.to_constr c))
+let clenv_nf_meta clenv c = nf_meta clenv.evd c
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
 let clenv_value clenv = meta_instance clenv.evd clenv.templval
-- 
cgit v1.2.3


From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 20:09:26 +0100
Subject: Eliminating parts of the right-hand side compatibility layer

---
 proofs/clenv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d986696604..572db1d408 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -266,7 +266,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus))))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -480,7 +480,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u))))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
-- 
cgit v1.2.3


From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 proofs/clenv.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 572db1d408..a428ab0ed0 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -60,7 +60,7 @@ let refresh_undefined_univs clenv =
       { clenv with evd = evd'; templval = map_freelisted clenv.templval;
 	templtyp = map_freelisted clenv.templtyp }, subst
 
-let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t)
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
 
@@ -71,7 +71,6 @@ let mk_freelisted c =
 
 let clenv_push_prod cl =
   let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
-  let typ = EConstr.of_constr typ in
   let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -266,7 +265,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -480,7 +479,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -498,7 +497,6 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
-  let c_typ = EConstr.of_constr c_typ in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
   let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
-- 
cgit v1.2.3


From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 17:15:15 +0100
Subject: Removing compatibility layers in Retyping

---
 proofs/clenv.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index a428ab0ed0..393e958d38 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -62,7 +62,7 @@ let refresh_undefined_univs clenv =
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
-let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
+let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 
 exception NotExtensibleClause
 
@@ -673,9 +673,7 @@ let evar_of_binder holes = function
 let define_with_type sigma env ev c =
   let open EConstr in
   let t = Retyping.get_type_of env sigma ev in
-  let t = EConstr.of_constr t in
   let ty = Retyping.get_type_of env sigma c in
-  let ty = EConstr.of_constr ty in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
   let (ev, _) = destEvar sigma ev in
-- 
cgit v1.2.3


From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 18:18:17 +0100
Subject: Ltac now uses evar-based constrs.

---
 proofs/clenv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 393e958d38..7269c61e3d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -575,10 +575,9 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 (* Pretty-print *)
 
 let pr_clenv clenv =
-  let inj = EConstr.Unsafe.to_constr in
   h 0
-    (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++
-     str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++
+    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
+     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
 
 (****************************************************************)
-- 
cgit v1.2.3


From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7269c61e3d..e580bccc3f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -133,7 +133,7 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t))
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 (******************************************************************)
 
-- 
cgit v1.2.3


From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
---
 proofs/clenv.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e580bccc3f..5645850b23 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -555,7 +555,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in
+      let t = rename_bound_vars_as_displayed sigma [] [] t in
       let clause = mk_clenv_from_env env sigma n
 	(c, t)
       in clenv_match_args lbind clause
@@ -603,9 +603,7 @@ let make_evar_clause env sigma ?len t =
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
-  let t = EConstr.Unsafe.to_constr t in
-  let t = rename_bound_vars_as_displayed [] [] t in
-  let t = EConstr.of_constr t in
+  let t = rename_bound_vars_as_displayed sigma [] [] t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
     else match EConstr.kind sigma t with
-- 
cgit v1.2.3


From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Dec 2016 10:45:19 +0100
Subject: Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.
---
 proofs/clenv.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5645850b23..f9ebc42330 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -129,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
     env = env }
 
 let mk_clenv_from_n gls n (c,cty) =
-  mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  mk_clenv_from_env env sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
 
 (******************************************************************)
 
@@ -263,8 +265,7 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
   if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
@@ -272,6 +273,14 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let old_clenv_unique_resolver ?flags clenv gl =
+  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+  let concl = Proofview.Goal.concl gl in
+  clenv_unique_resolver_gen ?flags clenv concl
+
 let adjust_meta_source evd mv = function
   | loc,Evar_kinds.VarInstance id ->
     let rec match_name c l =
-- 
cgit v1.2.3