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.

---
 pretyping/reductionops.ml | 41 +++++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 20 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a85e493eae..820974888e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -197,14 +197,14 @@ module Cst_stack = struct
 
   (** [best_replace d cst_l c] makes the best replacement for [d]
       by [cst_l] in [c] *)
-  let best_replace d cst_l c =
+  let best_replace sigma d cst_l c =
     let reconstruct_head = List.fold_left
       (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
     List.fold_right
-      (fun (cst,params,args) t -> Termops.replace_term
-	(reconstruct_head d args)
-	(applist (cst, List.rev params))
-	t) cst_l c
+      (fun (cst,params,args) t -> Termops.replace_term sigma
+	(EConstr.of_constr (reconstruct_head d args))
+	(EConstr.of_constr (applist (cst, List.rev params)))
+	(EConstr.of_constr t)) cst_l c
 
   let pr l =
     let open Pp in
@@ -612,8 +612,9 @@ let safe_meta_value sigma ev =
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
-  strongrec env t
+    let t = EConstr.of_constr (whdfun env sigma (EConstr.Unsafe.to_constr t)) in
+    map_constr_with_full_binders sigma push_rel strongrec env t in
+  EConstr.Unsafe.to_constr (strongrec env (EConstr.of_constr t))
 
 let local_strong whdfun sigma =
   let rec strongrec t = Constr.map strongrec (whdfun sigma t) in
@@ -712,14 +713,14 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies))
   substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env refold cst_l cofix sk =
+let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
   let raw_answer =
     let env = if refold then Some env else None in
     contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in
   apply_subst
     (fun x (t,sk') ->
       let t' =
-        if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in
+        if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
       recfun x (t',sk'))
     [] refold Cst_stack.empty raw_answer sk
 
@@ -757,7 +758,7 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
-let reduce_and_refold_fix recfun env refold cst_l fix sk =
+let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
   let raw_answer =
     let env = if refold then None else Some env in
     contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
@@ -765,7 +766,7 @@ let reduce_and_refold_fix recfun env refold cst_l fix sk =
     (fun x (t,sk') ->
       let t' =
         if refold then
-          Cst_stack.best_replace (mkFix fix) cst_l t
+          Cst_stack.best_replace sigma (mkFix fix) cst_l t
         else t
       in recfun x (t',sk'))
     [] refold Cst_stack.empty raw_answer sk
@@ -947,7 +948,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop u,Stack.empty),Cst_stack.empty else fold ()
+	      if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty),Cst_stack.empty else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
@@ -974,7 +975,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
 	  let x' = Stack.zip(x,args) in
 	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
-	  reduce_and_refold_fix whrec env refold cst_l f out_sk
+	  reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
 	|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
 	  let x' = Stack.zip(x,args) in
 	  begin match remains with
@@ -1010,7 +1011,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
-	  reduce_and_refold_cofix whrec env refold cst_l cofix stack
+	  reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack
 	|_ -> fold ()
       else fold ()
 
@@ -1043,7 +1044,7 @@ let local_whd_state_gen flags sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop u,Stack.empty) else s
+	      if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)
@@ -1568,10 +1569,10 @@ let meta_reducible_instance evd b =
   in
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
-    let u = whd_betaiota Evd.empty u in
+    let u = whd_betaiota Evd.empty u (** FIXME *) in
     match kind_of_term u with
-    | Case (ci,p,c,bl) when isMeta (strip_outer_cast c) ->
-	let m = destMeta (strip_outer_cast c) in
+    | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) ->
+	let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
@@ -1581,8 +1582,8 @@ let meta_reducible_instance evd b =
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when isMeta (strip_outer_cast f) ->
-	let m = destMeta (strip_outer_cast f) in
+    | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr f))) ->
+	let m = destMeta (strip_outer_cast evd (EConstr.of_constr f)) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
-- 
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.

---
 pretyping/reductionops.ml | 445 +++++++++++++++++++++++++---------------------
 1 file changed, 245 insertions(+), 200 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 820974888e..69d47e8e69 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -156,6 +156,7 @@ end
 
 (** Machinery about stack of unfolded constants *)
 module Cst_stack = struct
+  open EConstr
 (** constant * params * args
 
 - constant applied to params = term in head applied to args
@@ -191,8 +192,8 @@ module Cst_stack = struct
     | (cst,params,[])::_ -> Some(cst,params)
     | _ -> None
 
-  let reference t = match best_cst t with
-    | Some (c, _) when Term.isConst c -> Some (fst (Term.destConst c))
+  let reference sigma t = match best_cst t with
+    | Some (c, _) when isConst sigma c -> Some (fst (destConst sigma c))
     | _ -> None
 
   (** [best_replace d cst_l c] makes the best replacement for [d]
@@ -201,14 +202,14 @@ module Cst_stack = struct
     let reconstruct_head = List.fold_left
       (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
     List.fold_right
-      (fun (cst,params,args) t -> Termops.replace_term sigma
-	(EConstr.of_constr (reconstruct_head d args))
-	(EConstr.of_constr (applist (cst, List.rev params)))
-	(EConstr.of_constr t)) cst_l c
+      (fun (cst,params,args) t -> EConstr.of_constr (Termops.replace_term sigma
+	(reconstruct_head d args)
+	(applist (cst, List.rev params))
+	t)) cst_l c
 
   let pr l =
     let open Pp in
-    let p_c = Termops.print_constr in
+    let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
     prlist_with_sep pr_semicolon
       (fun (c,params,args) ->
 	hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
@@ -220,6 +221,7 @@ end
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 module Stack :
 sig
+  open EConstr
   type 'a app_node
   val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
 
@@ -231,7 +233,7 @@ sig
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
   | Proj of int * int * projection * Cst_stack.t
-  | Fix of fixpoint * 'a t * Cst_stack.t
+  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   | Shift of int
   | Update of 'a
@@ -242,10 +244,10 @@ sig
   val append_app : 'a array -> 'a t -> 'a t
   val decomp : 'a t -> ('a * 'a t) option
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
-  val equal : ('a * int -> 'a * int -> bool) -> (fixpoint * int -> fixpoint * int -> bool)
+  val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool)
     -> 'a t -> 'a t -> (int * int) option
   val compare_shape : 'a t -> 'a t -> bool
-  val map : (constr -> constr) -> constr t -> constr t
+  val map : ('a -> 'a) -> 'a t -> 'a t
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a * int * int
   val append_app_list : 'a list -> 'a t -> 'a t
@@ -258,10 +260,11 @@ sig
   val args_size : 'a t -> int
   val tail : int -> 'a t -> 'a t
   val nth : 'a t -> int -> 'a
-  val best_state : constr * constr t -> Cst_stack.t -> constr * constr t
-  val zip : ?refold:bool -> constr * constr t -> constr
+  val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
+  val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
 end =
 struct
+  open EConstr
   type 'a app_node = int * 'a array * int
   (* first releavnt position, arguments, last relevant position *)
 
@@ -286,7 +289,7 @@ struct
   | App of 'a app_node
   | Case of Term.case_info * 'a * 'a array * Cst_stack.t
   | Proj of int * int * projection * Cst_stack.t
-  | Fix of fixpoint * 'a t * Cst_stack.t
+  | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   | Shift of int
   | Update of 'a
@@ -305,7 +308,7 @@ struct
       str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
 	pr_comma () ++ pr_con (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
-       str "ZFix(" ++ Termops.pr_fix Termops.print_constr f
+       str "ZFix(" ++ Termops.pr_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
     | Cst (mem,curr,remains,params,cst_l) ->
       str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
@@ -533,11 +536,11 @@ struct
     | None -> raise Not_found
 
   (** This function breaks the abstraction of Cst_stack ! *)
-  let best_state (_,sk as s) l =
+  let best_state sigma (_,sk as s) l =
     let rec aux sk def = function
       |(cst, params, []) -> (cst, append_app_list (List.rev params) sk)
       |(cst, params, (i,t)::q) -> match decomp sk with
-	| Some (el,sk') when Constr.equal el t.(i) ->
+	| Some (el,sk') when EConstr.eq_constr sigma el t.(i) ->
 	  if i = pred (Array.length t)
 	  then aux sk' def (cst, params, q)
 	  else aux sk' def (cst, params, (succ i,t)::q)
@@ -552,53 +555,66 @@ struct
       | Some (hd, sk) -> mkProj (p, hd), sk
       | None -> assert false
 
-  let rec zip ?(refold=false) = function
+  let zip ?(refold=false) sigma s =
+  let rec zip = function
     | f, [] -> f
     | f, (App (i,a,j) :: s) ->
        let a' = if Int.equal i 0 && Int.equal j (Array.length a - 1)
 		then a
 		else Array.sub a i (j - i + 1) in
-       zip ~refold (mkApp (f, a'), s)
+       zip (mkApp (f, a'), s)
     | f, (Case (ci,rt,br,cst_l)::s) when refold ->
-      zip ~refold (best_state (mkCase (ci,rt,f,br), s) cst_l)
-    | f, (Case (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
+      zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l)
+    | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s)
     | f, (Fix (fix,st,cst_l)::s) when refold ->
-      zip ~refold (best_state (mkFix fix, st @ (append_app [|f|] s)) cst_l)
-  | f, (Fix (fix,st,_)::s) -> zip ~refold
+      zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
+  | f, (Fix (fix,st,_)::s) -> zip
     (mkFix fix, st @ (append_app [|f|] s))
   | f, (Cst (cst,_,_,params,cst_l)::s) when refold ->
-    zip ~refold (best_state (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
+    zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
   | f, (Cst (cst,_,_,params,_)::s) ->
-    zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s)))
-  | f, (Shift n::s) -> zip ~refold (lift n f, s)
+    zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
+  | f, (Shift n::s) -> zip (Vars.lift n f, s)
   | f, (Proj (n,m,p,cst_l)::s) when refold ->
-    zip ~refold (best_state (mkProj (p,f),s) cst_l)
-  | f, (Proj (n,m,p,_)::s) -> zip ~refold (mkProj (p,f),s)
+    zip (best_state sigma (mkProj (p,f),s) cst_l)
+  | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
   | _, (Update _::_) -> assert false
+  in
+  zip s
+
 end
 
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
-type state = constr * constr Stack.t
+type state = EConstr.t * EConstr.t Stack.t
 
-type  contextual_reduction_function = env ->  evar_map -> constr -> constr
-type  reduction_function =  contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
+type reduction_function = contextual_reduction_function
+type local_reduction_function = evar_map -> EConstr.t -> constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
 
-type  contextual_stack_reduction_function =
-    env ->  evar_map -> constr -> constr * constr list
-type  stack_reduction_function =  contextual_stack_reduction_function
+type contextual_stack_reduction_function =
+    env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function =
-    evar_map -> constr -> constr * constr list
+    evar_map -> EConstr.t -> EConstr.t * EConstr.t list
 
-type  contextual_state_reduction_function =
-    env ->  evar_map -> state -> state
-type  state_reduction_function =  contextual_state_reduction_function
+type contextual_state_reduction_function =
+    env -> evar_map -> state -> state
+type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
 let pr_state (tm,sk) =
   let open Pp in
-  h 0 (Termops.print_constr tm ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr sk)
+  let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+  h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
+
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
 
 (*************************************)
 (*** Reduction Functions Operators ***)
@@ -612,19 +628,19 @@ let safe_meta_value sigma ev =
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    let t = EConstr.of_constr (whdfun env sigma (EConstr.Unsafe.to_constr t)) in
+    let t = EConstr.of_constr (whdfun env sigma t) in
     map_constr_with_full_binders sigma push_rel strongrec env t in
-  EConstr.Unsafe.to_constr (strongrec env (EConstr.of_constr t))
+  EConstr.Unsafe.to_constr (strongrec env t)
 
 let local_strong whdfun sigma =
-  let rec strongrec t = Constr.map strongrec (whdfun sigma t) in
-  strongrec
+  let rec strongrec t = EConstr.map sigma strongrec (EConstr.of_constr (whdfun sigma t)) in
+  fun c -> EConstr.Unsafe.to_constr (strongrec c)
 
 let rec strong_prodspine redfun sigma c =
-  let x = redfun sigma c in
-  match kind_of_term x with
-    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
-    | _ -> x
+  let x = EConstr.of_constr (redfun sigma c) in
+  match EConstr.kind sigma x with
+    | Prod (na,a,b) -> mkProd (na, EConstr.Unsafe.to_constr a,strong_prodspine redfun sigma b)
+    | _ -> EConstr.Unsafe.to_constr x
 
 (*************************************)
 (*** Reduction using bindingss ***)
@@ -634,31 +650,36 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA]
 
 (* Beta Reduction tools *)
 
-let apply_subst recfun env refold cst_l t stack =
+let apply_subst recfun env sigma refold cst_l t stack =
   let rec aux env cst_l t stack =
-    match (Stack.decomp stack,kind_of_term t) with
+    match (Stack.decomp stack, EConstr.kind sigma t) with
     | Some (h,stacktl), Lambda (_,_,c) ->
        let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
        aux (h::env) cst_l' c stacktl
-    | _ -> recfun cst_l (substl env t, stack)
+    | _ -> recfun sigma cst_l (EConstr.Vars.substl env t, stack)
   in aux env cst_l t stack
 
-let stacklam recfun env t stack =
-  apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack
+let stacklam recfun env sigma t stack =
+  apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
+
+let beta_app sigma (c,l) =
+  let zip s = Stack.zip sigma s in
+  stacklam zip [] sigma c (Stack.append_app l Stack.empty)
 
-let beta_applist (c,l) =
-  stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
+let beta_applist sigma (c,l) =
+  let zip s = Stack.zip sigma s in
+  EConstr.Unsafe.to_constr (stacklam zip [] sigma c (Stack.append_app_list l Stack.empty))
 
 (* Iota reduction tools *)
 
 type 'a miota_args = {
-  mP      : constr;     (* the result type *)
-  mconstr : constr;     (* the constructor *)
+  mP      : EConstr.t;     (* the result type *)
+  mconstr : EConstr.t;     (* the constructor *)
   mci     : case_info;  (* special info to re-build pattern *)
   mcargs  : 'a list;    (* the constructor's arguments *)
   mlf     : 'a array }  (* the branch code vector *)
 
-let reducible_mind_case c = match kind_of_term c with
+let reducible_mind_case sigma c = match EConstr.kind sigma c with
   | Construct _ | CoFix _ -> true
   | _  -> false
 
@@ -672,9 +693,10 @@ let reducible_mind_case c = match kind_of_term c with
     f x := t. End M. Definition f := u. and say goodbye to any hope
     of refolding M.f this way ...
 *)
-let magicaly_constant_of_fixbody env reference bd = function
+let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
+    let open EConstr in
     try
       let (cst_mod,cst_sect,_) = Constant.repr3 reference in
       let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
@@ -682,7 +704,7 @@ let magicaly_constant_of_fixbody env reference bd = function
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
-        let csts = Universes.eq_constr_universes t bd in
+        let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in
         begin match csts with
         | Some csts ->
           let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
@@ -696,7 +718,8 @@ let magicaly_constant_of_fixbody env reference bd = function
     with
     | Not_found -> bd
 
-let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) =
+let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+  let open EConstr in
   let nbodies = Array.length bodies in
   let make_Fi j =
     let ind = nbodies-j-1 in
@@ -708,37 +731,40 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies))
       | Some e ->
         match reference with
         | None -> bd
-        | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in
+        | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
   let closure = List.init nbodies make_Fi in
-  substl closure bodies.(bodynum)
+  Vars.substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
 let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
+  let open EConstr in
   let raw_answer =
     let env = if refold then Some env else None in
-    contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in
+    contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
   apply_subst
-    (fun x (t,sk') ->
+    (fun sigma x (t,sk') ->
       let t' =
         if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
       recfun x (t',sk'))
-    [] refold Cst_stack.empty raw_answer sk
+    [] sigma refold Cst_stack.empty raw_answer sk
 
-let reduce_mind_case mia =
-  match kind_of_term mia.mconstr with
+let reduce_mind_case sigma mia =
+  let open EConstr in
+  match EConstr.kind sigma mia.mconstr with
     | Construct ((ind_sp,i),u) ->
 (*	let ncargs = (fst mia.mci).(i-1) in*)
 	let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
     | CoFix cofix ->
-	let cofix_def = contract_cofix cofix in
+	let cofix_def = contract_cofix sigma cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+    let open EConstr in
     let nbodies = Array.length recindices in
     let make_Fi j =
       let ind = nbodies-j-1 in
@@ -750,26 +776,27 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
 	| Some e ->
           match reference with
           | None -> bd
-          | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in
+          | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
     let closure = List.init nbodies make_Fi in
-    substl closure bodies.(bodynum)
+    Vars.substl closure bodies.(bodynum)
 
 (** First we substitute the Rel bodynum by the fixpoint and then we try to
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
 let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
+  let open EConstr in
   let raw_answer =
     let env = if refold then None else Some env in
-    contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
+    contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
   apply_subst
-    (fun x (t,sk') ->
+    (fun sigma x (t,sk') ->
       let t' =
         if refold then
           Cst_stack.best_replace sigma (mkFix fix) cst_l t
         else t
       in recfun x (t',sk'))
-    [] refold Cst_stack.empty raw_answer sk
+    [] sigma refold Cst_stack.empty raw_answer sk
 
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum && bodynum < Array.length recindices);
@@ -802,51 +829,53 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_RAKAM:=a);
 }
 
-let equal_stacks (x, l) (y, l') =
-  let f_equal (x,lft1) (y,lft2) = Constr.equal (Vars.lift lft1 x) (Vars.lift lft2 y) in
-  let eq_fix (a,b) (c,d) = f_equal (Constr.mkFix a, b) (Constr.mkFix c, d) in
+let equal_stacks sigma (x, l) (y, l') =
+  let open EConstr in
+  let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in
+  let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in
     match Stack.equal f_equal eq_fix l l' with
     | None -> false
     | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) 
 
 let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
+  let open EConstr in
   let open Context.Named.Declaration in
-  let rec whrec cst_l (x, stack as s) =
+  let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
 	let open Pp in
+	let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
 	Feedback.msg_notice
-             (h 0 (str "<<" ++ Termops.print_constr x ++
+             (h 0 (str "<<" ++ pr x ++
 		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
-		   str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
+		   str "|" ++ cut () ++ Stack.pr pr stack ++
 		   str ">>"))
     in
+    let c0 = EConstr.kind sigma x in
     let fold () =
       let () = if !debug_RAKAM then
 	  let open Pp in Feedback.msg_notice (str "<><><><><>") in
-      (s,cst_l)
+      ((EConstr.of_kind c0, stack),cst_l)
     in
-    match kind_of_term x with
+    match c0 with
     | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (EConstr.of_constr (lift n body), stack)
       | _ -> fold ())
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) ->
-	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
+	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (EConstr.of_constr body, stack)
       | _ -> fold ())
-    | Evar ev ->
-      (match safe_evar_value sigma ev with
-      | Some body -> whrec cst_l (body, stack)
-      | None -> fold ())
+    | Evar ev -> fold ()
     | Meta ev ->
       (match safe_meta_value sigma ev with
-      | Some body -> whrec cst_l (body, stack)
+      | Some body -> whrec cst_l (EConstr.of_constr body, stack)
       | None -> fold ())
     | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) ->
        (match constant_opt_value_in env const with
 	| None -> fold ()
 	| Some body ->
+          let body = EConstr.of_constr body in
 	   if not tactic_mode
 	   then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
 		      (body, stack)
@@ -863,12 +892,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		    let (tm',sk'),cst_l' =
 		      whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
 		    in
-		    let rec is_case x = match kind_of_term x with
+		    let rec is_case x = match EConstr.kind sigma x with
 		      | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
 		      | App (hd, _) -> is_case hd
 		      | Case _ -> true
 		      | _ -> false in
-		    if equal_stacks (x, app_sk) (tm', sk')
+		    if equal_stacks sigma (x, app_sk) (tm', sk')
 		       || Stack.will_expose_iota sk'
 		       || is_case tm'
 		      then fold ()
@@ -896,7 +925,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	 | None ->
 	   let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
 	   let stack'', csts = whrec Cst_stack.empty stack' in
-	     if equal_stacks stack' stack'' then fold ()
+	     if equal_stacks sigma stack' stack'' then fold ()
 	     else stack'', csts
 	 | Some (recargs, nargs, flags) ->
 	   if (List.mem `ReductionNeverUnfold flags
@@ -926,7 +955,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 				      Stack.append_app [|c|] bef,cst_l)::s'))
 
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
-      apply_subst whrec [b] refold cst_l c stack
+      apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
     | Cast (c,_,_) -> whrec cst_l (c, stack)
     | App (f,cl)  ->
       whrec
@@ -935,20 +964,20 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     | Lambda (na,t,c) ->
       (match Stack.decomp stack with
       | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
-	apply_subst whrec [] refold cst_l x stack
+	apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
-	let env' = push_rel (LocalAssum (na,t)) env in
+	let env' = push_rel (local_assum (na, t)) env in
 	let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
-        (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with
+        (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
         | App (f,cl) ->
 	  let napp = Array.length cl in
 	  if napp > 0 then
 	    let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
-            match kind_of_term x', l' with
+            match EConstr.kind sigma x', l' with
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
-	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty),Cst_stack.empty else fold ()
+	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
+	      if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
@@ -973,11 +1002,11 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	|args, (Stack.Proj (n,m,p,_)::s') when use_match ->
 	  whrec Cst_stack.empty (Stack.nth args (n+m), s')
 	|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
-	  let x' = Stack.zip(x,args) in
+	  let x' = Stack.zip sigma (x, args) in
 	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
 	  reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
 	|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
-	  let x' = Stack.zip(x,args) in
+	  let x' = Stack.zip sigma (x, args) in
 	  begin match remains with
 	  | [] -> 
 	    (match const with
@@ -985,6 +1014,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	      (match constant_opt_value_in env const with
 	      | None -> fold ()
 	      | Some body ->
+                let body = EConstr.of_constr body in
 		whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
 		  (body, s' @ (Stack.append_app [|x'|] s'')))
 	    | Stack.Cst_proj p ->
@@ -1020,31 +1050,34 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   in
   fun xs ->
   let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
-  if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res
+  if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
 
 (** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags sigma =
-  let rec whrec (x, stack as s) =
-    match kind_of_term x with
+  let open EConstr in
+  let rec whrec (x, stack) =
+    let c0 = EConstr.kind sigma x in
+    let s = (EConstr.of_kind c0, stack) in
+    match c0 with
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
-      stacklam whrec [b] c stack
+      stacklam whrec [b] sigma c stack
     | Cast (c,_,_) -> whrec (c, stack)
     | App (f,cl)  -> whrec (f, Stack.append_app cl stack)
     | Lambda (_,_,c) ->
       (match Stack.decomp stack with
       | Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
-	stacklam whrec [a] c m
+	stacklam whrec [a] sigma c m
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
-        (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with
+        (match EConstr.kind sigma (Stack.zip sigma (whrec (c, Stack.empty))) with
         | App (f,cl) ->
 	  let napp = Array.length cl in
 	  if napp > 0 then
 	    let x', l' = whrec (Array.last cl, Stack.empty) in
-            match kind_of_term x', l' with
+            match EConstr.kind sigma x', l' with
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
-	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty) else s
+	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
+	      if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)
@@ -1064,14 +1097,10 @@ let local_whd_state_gen flags sigma =
       |None -> s
       |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,Cst_stack.empty)::s'))
 
-    | Evar ev ->
-      (match safe_evar_value sigma ev with
-        Some c -> whrec (c,stack)
-      | None -> s)
-
+    | Evar ev -> s
     | Meta ev ->
       (match safe_meta_value sigma ev with
-        Some c -> whrec (c,stack)
+        Some c -> whrec (EConstr.of_constr c,stack)
       | None -> s)
 
     | Construct ((ind,c),u) ->
@@ -1084,8 +1113,8 @@ let local_whd_state_gen flags sigma =
 	|args, (Stack.Proj (n,m,p,_) :: s') when use_match ->
 	  whrec (Stack.nth args (n+m), s')
 	|args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
-	  let x' = Stack.zip(x,args) in
-	  whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s''))
+	  let x' = Stack.zip sigma (x,args) in
+	  whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s''))
 	|_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false
 	|_, _ -> s
       else s
@@ -1094,7 +1123,7 @@ let local_whd_state_gen flags sigma =
       if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
-	  whrec (contract_cofix cofix, stack)
+	  whrec (contract_cofix sigma cofix, stack)
 	|_ -> s
       else s
 
@@ -1107,7 +1136,7 @@ let raw_whd_state_gen flags env =
   f
 
 let stack_red_of_state_red f =
-  let f sigma x = decompose_app (Stack.zip (f sigma (x, Stack.empty))) in
+  let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in
   f
 
 (* Drops the Cst_stack *)
@@ -1115,11 +1144,11 @@ let iterate_whd_gen refold flags env sigma s =
   let rec aux t =
   let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
   let whd_sk = Stack.map aux sk in
-  Stack.zip ~refold (hd,whd_sk)
+  Stack.zip sigma ~refold (hd,whd_sk)
   in aux s
 
 let red_of_state_red f sigma x =
-  Stack.zip (f sigma (x,Stack.empty))
+  EConstr.Unsafe.to_constr (Stack.zip sigma (f sigma (x,Stack.empty)))
 
 (* 0. No Reduction Functions *)
 
@@ -1174,7 +1203,7 @@ let whd_allnolet env =
 
 (* 4. Ad-hoc eta reduction, does not subsitute evars *)
 
-let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty))
+let shrink_eta c = EConstr.Unsafe.to_constr (Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)))
 
 (* 5. Zeta Reduction Functions *)
 
@@ -1198,7 +1227,7 @@ let clos_norm_flags flgs env sigma t =
     let evars ev = safe_evar_value sigma ev in
     CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
-      (CClosure.inject t)
+      (CClosure.inject (EConstr.Unsafe.to_constr t))
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
@@ -1239,7 +1268,15 @@ let report_anomaly _ =
   let e = CErrors.push e in
   iraise e
 
-let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
+let f_conv ?l2r ?reds env ?evars x y =
+  let inj = EConstr.Unsafe.to_constr in
+  Reduction.conv ?l2r ?reds env ?evars (inj x) (inj y)
+
+let f_conv_leq ?l2r ?reds env ?evars x y =
+  let inj = EConstr.Unsafe.to_constr in
+  Reduction.conv_leq ?l2r ?reds env ?evars (inj x) (inj y)
+
+let test_trans_conversion (f: EConstr.t Reduction.extended_conversion_function) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
     let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
@@ -1247,16 +1284,16 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red
   with Reduction.NotConvertible -> false
     | e when is_anomaly e -> report_anomaly e
 
-let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv reds env sigma
-let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq reds env sigma
+let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma
+let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma
 let is_fconv ?(reds=full_transparent_state) = function
   | Reduction.CONV -> is_conv ~reds
   | Reduction.CUMUL -> is_conv_leq ~reds
 
 let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
   let f = match pb with
-    | Reduction.CONV -> Reduction.conv
-    | Reduction.CUMUL -> Reduction.conv_leq
+    | Reduction.CONV -> f_conv
+    | Reduction.CUMUL -> f_conv_leq
   in
     try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true
     with Reduction.NotConvertible -> false
@@ -1320,37 +1357,38 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta sigma c = match kind_of_term c with
-  | Meta p -> (try meta_value sigma p with Not_found -> c)
-  | _ -> c
+let whd_meta sigma c = match EConstr.kind sigma c with
+  | Meta p -> (try meta_value sigma p with Not_found -> EConstr.Unsafe.to_constr c)
+  | _ -> EConstr.Unsafe.to_constr c
 
 let default_plain_instance_ident = Id.of_string "H"
 
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
-let plain_instance s c =
-  let rec irec n u = match kind_of_term u with
-    | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
-    | App (f,l) when isCast f ->
-        let (f,_,t) = destCast f in
+let plain_instance sigma s c =
+  let open EConstr in
+  let rec irec n u = match EConstr.kind sigma u with
+    | Meta p -> (try Vars.lift n (Metamap.find p s) with Not_found -> u)
+    | App (f,l) when isCast sigma f ->
+        let (f,_,t) = destCast sigma f in
         let l' = CArray.Fun1.smartmap irec n l in
-        (match kind_of_term f with
+        (match EConstr.kind sigma f with
         | Meta p ->
 	    (* Don't flatten application nodes: this is used to extract a
                proof-term from a proof-tree and we want to keep the structure
                of the proof-tree *)
 	    (try let g = Metamap.find p s in
-	    match kind_of_term g with
+	    match EConstr.kind sigma g with
             | App _ ->
-                let l' = CArray.Fun1.smartmap lift 1 l' in
+                let l' = CArray.Fun1.smartmap Vars.lift 1 l' in
                 mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
         | _ -> mkApp (irec n f,l'))
-    | Cast (m,_,_) when isMeta m ->
-	(try lift n (Metamap.find (destMeta m) s) with Not_found -> u)
+    | Cast (m,_,_) when isMeta sigma m ->
+	(try Vars.lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
     | _ ->
-	map_constr_with_binders succ irec n u
+	map_with_binders sigma succ irec n u
   in
   if Metamap.is_empty s then c
   else irec 0 c
@@ -1391,7 +1429,7 @@ let plain_instance s c =
 
 let instance sigma s c =
   (* if s = [] then c else *)
-  local_strong whd_betaiota sigma (plain_instance s c)
+  local_strong whd_betaiota sigma (plain_instance sigma s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -1400,34 +1438,40 @@ let instance sigma s c =
  * error message. *)
 
 let hnf_prod_app env sigma t n =
-  match kind_of_term (whd_all env sigma t) with
-    | Prod (_,_,b) -> subst1 n b
+  let open EConstr in
+  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+    | Prod (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
 let hnf_prod_appvect env sigma t nl =
-  Array.fold_left (hnf_prod_app env sigma) t nl
+  Array.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let hnf_prod_applist env sigma t nl =
-  List.fold_left (hnf_prod_app env sigma) t nl
+  List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let hnf_lam_app env sigma t n =
-  match kind_of_term (whd_all env sigma t) with
-    | Lambda (_,_,b) -> subst1 n b
+  let open EConstr in
+  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+    | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
     | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
 let hnf_lam_appvect env sigma t nl =
-  Array.fold_left (hnf_lam_app env sigma) t nl
+  Array.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let hnf_lam_applist env sigma t nl =
-  List.fold_left (hnf_lam_app env sigma) t nl
+  List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+
+let bind_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  (na, inj t)
 
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match kind_of_term t with
+    match EConstr.kind sigma (EConstr.of_constr t) with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (LocalAssum (n,a)) env)
-	    ((n,a)::m) c0
+	  decrec (push_rel (local_assum (n,a)) env)
+	    (bind_assum (n,a)::m) c0
       | _ -> m,t
   in
   decrec env []
@@ -1435,10 +1479,10 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match kind_of_term t with
+    match EConstr.kind sigma (EConstr.of_constr t) with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (LocalAssum (n,a)) env)
-	    ((n,a)::m) c0
+	  decrec (push_rel (local_assum (n,a)) env)
+	    (bind_assum (n,a)::m) c0
       | _ -> m,t
   in
   decrec env []
@@ -1446,51 +1490,51 @@ let splay_lam env sigma =
 let splay_prod_assum env sigma =
   let rec prodec_rec env l c =
     let t = whd_allnolet env sigma c in
-    match kind_of_term t with
+    match EConstr.kind sigma (EConstr.of_constr t) with
     | Prod (x,t,c)  ->
-	prodec_rec (push_rel (LocalAssum (x,t)) env)
-	  (Context.Rel.add (LocalAssum (x,t)) l) c
+	prodec_rec (push_rel (local_assum (x,t)) env)
+	  (Context.Rel.add (local_assum (x,t)) l) c
     | LetIn (x,b,t,c) ->
-	prodec_rec (push_rel (LocalDef (x,b,t)) env)
-	  (Context.Rel.add (LocalDef (x,b,t)) l) c
+	prodec_rec (push_rel (local_def (x,b,t)) env)
+	  (Context.Rel.add (local_def (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
-      let t' = whd_all env sigma t in
+      let t' = whd_all env sigma (EConstr.of_constr t) in
 	if Term.eq_constr t t' then l,t
-	else prodec_rec env l t'
+	else prodec_rec env l (EConstr.of_constr t')
   in
   prodec_rec env Context.Rel.empty
 
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
-  match kind_of_term c with
+  match EConstr.kind sigma (EConstr.of_constr c) with
     | Sort s -> l,s
     | _ -> invalid_arg "splay_arity"
 
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
-    match kind_of_term (whd_all env sigma c) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
+    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (LocalAssum (n,a)) env)
-	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
+	  decrec (push_rel (local_assum (n,a)) env)
+	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_prod_n"
   in
   decrec env n Context.Rel.empty
 
 let splay_lam_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
-    match kind_of_term (whd_all env sigma c) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
+    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (LocalAssum (n,a)) env)
-	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
+	  decrec (push_rel (local_assum (n,a)) env)
+	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_lam_n"
   in
   decrec env n Context.Rel.empty
 
 let is_sort env sigma t =
-  match kind_of_term (whd_all env sigma t) with
+  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
   | Sort s -> true
   | _ -> false
 
@@ -1498,6 +1542,7 @@ let is_sort env sigma t =
    of case/fix (heuristic used by evar_conv) *)
 
 let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+  let open EConstr in
   let refold = get_refolding_in_reduction () in
   let tactic_mode = false in
   let rec whrec csts s =
@@ -1506,15 +1551,15 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
       |args, (Stack.Case _ :: _ as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
-	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+	if reducible_mind_case sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Fix _ :: _ as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
-	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+	if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Proj (n,m,p,_) :: stack'') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
-	if isConstruct t_o then
+	if isConstruct sigma t_o then
 	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
 	else s,csts'
       |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
@@ -1523,9 +1568,9 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_all env sigma c in
-    match kind_of_term t with
-      | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
-      | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
+    match EConstr.kind sigma (EConstr.of_constr t) with
+      | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
+      | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | t -> t
   in
   decrec env
@@ -1539,11 +1584,12 @@ let is_arity env sigma c =
 (* Metas *)
 
 let meta_value evd mv =
+  let open EConstr in
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      instance evd metas b.rebus
+      EConstr.of_constr (instance evd metas (EConstr.of_constr b.rebus))
     | None -> mkMeta mv
   in
   valrec mv
@@ -1553,7 +1599,7 @@ let meta_instance sigma b =
   if Metaset.is_empty fm then b.rebus
   else
     let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    instance sigma c_sigma b.rebus
+    instance sigma c_sigma (EConstr.of_constr b.rebus)
 
 let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
 
@@ -1569,7 +1615,7 @@ let meta_reducible_instance evd b =
   in
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
-    let u = whd_betaiota Evd.empty u (** FIXME *) in
+    let u = whd_betaiota Evd.empty (EConstr.of_constr u) (** FIXME *) in
     match kind_of_term u with
     | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) ->
 	let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in
@@ -1615,32 +1661,31 @@ let meta_reducible_instance evd b =
   else irec b.rebus
 
 
-let head_unfold_under_prod ts env _ c =
+let head_unfold_under_prod ts env sigma c =
+  let open EConstr in
   let unfold (cst,u as cstu) =
     if Cpred.mem cst (snd ts) then
       match constant_opt_value_in env cstu with
-	| Some c -> c
+	| Some c -> EConstr.of_constr c
 	| None -> mkConstU cstu
     else mkConstU cstu in
   let rec aux c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
       | Prod (n,t,c) -> mkProd (n,aux t, aux c)
       | _ ->
-	  let (h,l) = decompose_app c in
-	  match kind_of_term h with
-	    | Const cst -> beta_applist (unfold cst,l)
+	  let (h,l) = decompose_app_vect sigma c in
+	  match EConstr.kind sigma (EConstr.of_constr h) with
+	    | Const cst -> beta_app sigma (unfold cst, Array.map EConstr.of_constr l)
 	    | _ -> c in
-  aux c
+  EConstr.Unsafe.to_constr (aux c)
 
 let betazetaevar_applist sigma n c l =
+  let open EConstr in
   let rec stacklam n env t stack =
-    if Int.equal n 0 then applist (substl env t, stack) else
-    match kind_of_term t, stack with
+    if Int.equal n 0 then applist (Vars.substl env t, stack) else
+    match EConstr.kind sigma t, stack with
     | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-    | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
-    | Evar ev, _ ->
-      (match safe_evar_value sigma ev with
-      | Some body -> stacklam n env body stack
-      | None -> applist (substl env t, stack))
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (Vars.substl env b::env) c stack
+    | Evar _, _ -> applist (Vars.substl env t, stack)
     | _ -> anomaly (Pp.str "Not enough lambda/let's") in
-  stacklam n [] c l
+  EConstr.Unsafe.to_constr (stacklam n [] c l)
-- 
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.

---
 pretyping/reductionops.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 69d47e8e69..0b97cd253b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1317,6 +1317,8 @@ let sigma_univ_state =
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
+  let x = EConstr.Unsafe.to_constr x in
+  let y = EConstr.Unsafe.to_constr y in
   try
     let fold cstr sigma =
       try Some (Evd.add_universe_constraints sigma cstr)
-- 
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.

---
 pretyping/reductionops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0b97cd253b..510417879e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1203,7 +1203,7 @@ let whd_allnolet env =
 
 (* 4. Ad-hoc eta reduction, does not subsitute evars *)
 
-let shrink_eta c = EConstr.Unsafe.to_constr (Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)))
+let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty))
 
 (* 5. Zeta Reduction Functions *)
 
-- 
cgit v1.2.3


From 536026f3e20f761e8ef366ed732da7d3b626ac5e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 15:39:01 +0100
Subject: Cleaning up opening of the EConstr module in pretyping folder.

---
 pretyping/reductionops.ml | 100 +++++++++++++++++++++-------------------------
 1 file changed, 45 insertions(+), 55 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 510417879e..0e0b807441 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -10,10 +10,11 @@ open CErrors
 open Util
 open Names
 open Term
-open Vars
 open Termops
 open Univ
 open Evd
+open EConstr
+open Vars
 open Environ
 open Context.Rel.Declaration
 
@@ -574,7 +575,7 @@ struct
     zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
   | f, (Cst (cst,_,_,params,_)::s) ->
     zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
-  | f, (Shift n::s) -> zip (Vars.lift n f, s)
+  | f, (Shift n::s) -> zip (lift n f, s)
   | f, (Proj (n,m,p,cst_l)::s) when refold ->
     zip (best_state sigma (mkProj (p,f),s) cst_l)
   | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
@@ -585,18 +586,18 @@ struct
 end
 
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
-type state = EConstr.t * EConstr.t Stack.t
+type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
+type contextual_reduction_function = env -> evar_map -> constr -> Constr.constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> EConstr.t -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
+type local_reduction_function = evar_map -> constr -> Constr.constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (Constr.constr, 'r) Sigma.sigma }
 
 type contextual_stack_reduction_function =
-    env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+    env -> evar_map -> constr -> constr * constr list
 type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function =
-    evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+    evar_map -> constr -> constr * constr list
 
 type contextual_state_reduction_function =
     env -> evar_map -> state -> state
@@ -639,7 +640,7 @@ let local_strong whdfun sigma =
 let rec strong_prodspine redfun sigma c =
   let x = EConstr.of_constr (redfun sigma c) in
   match EConstr.kind sigma x with
-    | Prod (na,a,b) -> mkProd (na, EConstr.Unsafe.to_constr a,strong_prodspine redfun sigma b)
+    | Prod (na,a,b) -> EConstr.Unsafe.to_constr (mkProd (na,a,EConstr.of_constr (strong_prodspine redfun sigma b)))
     | _ -> EConstr.Unsafe.to_constr x
 
 (*************************************)
@@ -656,7 +657,7 @@ let apply_subst recfun env sigma refold cst_l t stack =
     | Some (h,stacktl), Lambda (_,_,c) ->
        let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
        aux (h::env) cst_l' c stacktl
-    | _ -> recfun sigma cst_l (EConstr.Vars.substl env t, stack)
+    | _ -> recfun sigma cst_l (substl env t, stack)
   in aux env cst_l t stack
 
 let stacklam recfun env sigma t stack =
@@ -673,8 +674,8 @@ let beta_applist sigma (c,l) =
 (* Iota reduction tools *)
 
 type 'a miota_args = {
-  mP      : EConstr.t;     (* the result type *)
-  mconstr : EConstr.t;     (* the constructor *)
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
   mci     : case_info;  (* special info to re-build pattern *)
   mcargs  : 'a list;    (* the constructor's arguments *)
   mlf     : 'a array }  (* the branch code vector *)
@@ -696,7 +697,6 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
 let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
-    let open EConstr in
     try
       let (cst_mod,cst_sect,_) = Constant.repr3 reference in
       let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
@@ -719,7 +719,6 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
     | Not_found -> bd
 
 let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
-  let open EConstr in
   let nbodies = Array.length bodies in
   let make_Fi j =
     let ind = nbodies-j-1 in
@@ -733,11 +732,10 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo
         | None -> bd
         | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
   let closure = List.init nbodies make_Fi in
-  Vars.substl closure bodies.(bodynum)
+  substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
 let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
-  let open EConstr in
   let raw_answer =
     let env = if refold then Some env else None in
     contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
@@ -749,7 +747,6 @@ let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
     [] sigma refold Cst_stack.empty raw_answer sk
 
 let reduce_mind_case sigma mia =
-  let open EConstr in
   match EConstr.kind sigma mia.mconstr with
     | Construct ((ind_sp,i),u) ->
 (*	let ncargs = (fst mia.mci).(i-1) in*)
@@ -764,7 +761,6 @@ let reduce_mind_case sigma mia =
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
 let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
-    let open EConstr in
     let nbodies = Array.length recindices in
     let make_Fi j =
       let ind = nbodies-j-1 in
@@ -778,14 +774,13 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
           | None -> bd
           | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
     let closure = List.init nbodies make_Fi in
-    Vars.substl closure bodies.(bodynum)
+    substl closure bodies.(bodynum)
 
 (** First we substitute the Rel bodynum by the fixpoint and then we try to
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
 let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
-  let open EConstr in
   let raw_answer =
     let env = if refold then None else Some env in
     contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
@@ -830,7 +825,6 @@ let _ = Goptions.declare_bool_option {
 }
 
 let equal_stacks sigma (x, l) (y, l') =
-  let open EConstr in
   let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in
   let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in
     match Stack.equal f_equal eq_fix l l' with
@@ -838,7 +832,6 @@ let equal_stacks sigma (x, l) (y, l') =
     | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) 
 
 let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
-  let open EConstr in
   let open Context.Named.Declaration in
   let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
@@ -859,7 +852,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     match c0 with
     | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | LocalDef (_,body,_) -> whrec Cst_stack.empty (EConstr.of_constr (lift n body), stack)
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n (EConstr.of_constr body), stack)
       | _ -> fold ())
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
@@ -977,7 +970,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-	      if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
+	      if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
@@ -1054,7 +1047,6 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 
 (** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags sigma =
-  let open EConstr in
   let rec whrec (x, stack) =
     let c0 = EConstr.kind sigma x in
     let s = (EConstr.of_kind c0, stack) in
@@ -1077,7 +1069,7 @@ let local_whd_state_gen flags sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-	      if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
+	      if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)
@@ -1276,7 +1268,7 @@ let f_conv_leq ?l2r ?reds env ?evars x y =
   let inj = EConstr.Unsafe.to_constr in
   Reduction.conv_leq ?l2r ?reds env ?evars (inj x) (inj y)
 
-let test_trans_conversion (f: EConstr.t Reduction.extended_conversion_function) reds env sigma x y =
+let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
     let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
@@ -1368,9 +1360,8 @@ let default_plain_instance_ident = Id.of_string "H"
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
 let plain_instance sigma s c =
-  let open EConstr in
   let rec irec n u = match EConstr.kind sigma u with
-    | Meta p -> (try Vars.lift n (Metamap.find p s) with Not_found -> u)
+    | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
     | App (f,l) when isCast sigma f ->
         let (f,_,t) = destCast sigma f in
         let l' = CArray.Fun1.smartmap irec n l in
@@ -1382,13 +1373,13 @@ let plain_instance sigma s c =
 	    (try let g = Metamap.find p s in
 	    match EConstr.kind sigma g with
             | App _ ->
-                let l' = CArray.Fun1.smartmap Vars.lift 1 l' in
+                let l' = CArray.Fun1.smartmap lift 1 l' in
                 mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
         | _ -> mkApp (irec n f,l'))
     | Cast (m,_,_) when isMeta sigma m ->
-	(try Vars.lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
+	(try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
     | _ ->
 	map_with_binders sigma succ irec n u
   in
@@ -1440,9 +1431,8 @@ let instance sigma s c =
  * error message. *)
 
 let hnf_prod_app env sigma t n =
-  let open EConstr in
   match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Prod (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
+    | Prod (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
 let hnf_prod_appvect env sigma t nl =
@@ -1452,9 +1442,8 @@ let hnf_prod_applist env sigma t nl =
   List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let hnf_lam_app env sigma t n =
-  let open EConstr in
   match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
+    | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
     | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
 let hnf_lam_appvect env sigma t nl =
@@ -1544,7 +1533,6 @@ let is_sort env sigma t =
    of case/fix (heuristic used by evar_conv) *)
 
 let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
-  let open EConstr in
   let refold = get_refolding_in_reduction () in
   let tactic_mode = false in
   let rec whrec csts s =
@@ -1586,7 +1574,6 @@ let is_arity env sigma c =
 (* Metas *)
 
 let meta_value evd mv =
-  let open EConstr in
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
@@ -1617,54 +1604,58 @@ let meta_reducible_instance evd b =
   in
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
-    let u = whd_betaiota Evd.empty (EConstr.of_constr u) (** FIXME *) in
-    match kind_of_term u with
-    | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) ->
-	let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in
+    let u = whd_betaiota Evd.empty u (** FIXME *) in
+    let u = EConstr.of_constr u in
+    match EConstr.kind evd u with
+    | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd c)) ->
+	let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd c)) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
+	    let g = EConstr.of_constr g in
             let is_coerce = match s with CoerceToType -> true | _ -> false in
-	    if isConstruct g || not is_coerce then Some g else None
+	    if isConstruct evd g || not is_coerce then Some g else None
 	  with Not_found -> None
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr f))) ->
-	let m = destMeta (strip_outer_cast evd (EConstr.of_constr f)) in
+    | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd f)) ->
+	let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd f)) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
+	    let g = EConstr.of_constr g in
             let is_coerce = match s with CoerceToType -> true | _ -> false in
-	    if isLambda g || not is_coerce then Some g else None
+	    if isLambda evd g || not is_coerce then Some g else None
 	  with Not_found -> None
 	 with
 	   | Some g -> irec (mkApp (g,l))
 	   | None -> mkApp (f,Array.map irec l))
     | Meta m ->
 	(try let g, s = Metamap.find m metas in
+          let g = EConstr.of_constr g in
           let is_coerce = match s with CoerceToType -> true | _ -> false in
           if not is_coerce then irec g else u
 	 with Not_found -> u)
-    | Proj (p,c) when isMeta c || isCast c && isMeta (pi1 (destCast c)) ->
-	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+    | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) ->
+	let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in
 	  (match
 	  try
 	    let g, s = Metamap.find m metas in
+            let g = EConstr.of_constr g in
             let is_coerce = match s with CoerceToType -> true | _ -> false in
-	    if isConstruct g || not is_coerce then Some g else None
+	    if isConstruct evd g || not is_coerce then Some g else None
 	  with Not_found -> None
 	  with
 	    | Some g -> irec (mkProj (p,g))
 	    | None -> mkProj (p,c))
-    | _ -> Constr.map irec u
+    | _ -> EConstr.map evd irec u
   in
   if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
-  else irec b.rebus
+  else EConstr.Unsafe.to_constr (irec (EConstr.of_constr b.rebus))
 
 
 let head_unfold_under_prod ts env sigma c =
-  let open EConstr in
   let unfold (cst,u as cstu) =
     if Cpred.mem cst (snd ts) then
       match constant_opt_value_in env cstu with
@@ -1682,12 +1673,11 @@ let head_unfold_under_prod ts env sigma c =
   EConstr.Unsafe.to_constr (aux c)
 
 let betazetaevar_applist sigma n c l =
-  let open EConstr in
   let rec stacklam n env t stack =
-    if Int.equal n 0 then applist (Vars.substl env t, stack) else
+    if Int.equal n 0 then applist (substl env t, stack) else
     match EConstr.kind sigma t, stack with
     | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-    | LetIn(_,b,_,c), _ -> stacklam (n-1) (Vars.substl env b::env) c stack
-    | Evar _, _ -> applist (Vars.substl env t, stack)
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
+    | Evar _, _ -> applist (substl env t, stack)
     | _ -> anomaly (Pp.str "Not enough lambda/let's") in
   EConstr.Unsafe.to_constr (stacklam n [] c l)
-- 
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.

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

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0e0b807441..0dd615bfb7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1588,9 +1588,11 @@ let meta_instance sigma b =
   if Metaset.is_empty fm then b.rebus
   else
     let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    instance sigma c_sigma (EConstr.of_constr b.rebus)
+    EConstr.of_constr (instance sigma c_sigma b.rebus)
 
-let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
+let nf_meta sigma c =
+  let cl = mk_freelisted c in
+  EConstr.Unsafe.to_constr (meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus })
 
 (* Instantiate metas that create beta/iota redexes *)
 
@@ -1652,7 +1654,7 @@ let meta_reducible_instance evd b =
     | _ -> EConstr.map evd irec u
   in
   if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
-  else EConstr.Unsafe.to_constr (irec (EConstr.of_constr b.rebus))
+  else irec b.rebus
 
 
 let head_unfold_under_prod ts env sigma c =
-- 
cgit v1.2.3


From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:07:35 +0100
Subject: Inv API using EConstr.

---
 pretyping/reductionops.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0dd615bfb7..480ec23192 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1453,13 +1453,13 @@ let hnf_lam_applist env sigma t nl =
   List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let bind_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  (na, inj t)
+  (na, t)
 
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
@@ -1470,7 +1470,8 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
@@ -1498,7 +1499,7 @@ let splay_prod_assum env sigma =
 
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
-  match EConstr.kind sigma (EConstr.of_constr c) with
+  match EConstr.kind sigma c with
     | Sort s -> l,s
     | _ -> invalid_arg "splay_arity"
 
-- 
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.

---
 pretyping/reductionops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 480ec23192..31354217fd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1592,8 +1592,9 @@ let meta_instance sigma b =
     EConstr.of_constr (instance sigma c_sigma b.rebus)
 
 let nf_meta sigma c =
+  let c = EConstr.Unsafe.to_constr c in
   let cl = mk_freelisted c in
-  EConstr.Unsafe.to_constr (meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus })
+  meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus }
 
 (* Instantiate metas that create beta/iota redexes *)
 
-- 
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

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

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 31354217fd..6ec3cd985c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -669,7 +669,7 @@ let beta_app sigma (c,l) =
 
 let beta_applist sigma (c,l) =
   let zip s = Stack.zip sigma s in
-  EConstr.Unsafe.to_constr (stacklam zip [] sigma c (Stack.append_app_list l Stack.empty))
+  stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)
 
 (* Iota reduction tools *)
 
@@ -1611,8 +1611,8 @@ let meta_reducible_instance evd b =
     let u = whd_betaiota Evd.empty u (** FIXME *) in
     let u = EConstr.of_constr u in
     match EConstr.kind evd u with
-    | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd c)) ->
-	let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd c)) in
+    | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
+	let m = destMeta evd (strip_outer_cast evd c) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
@@ -1623,8 +1623,8 @@ let meta_reducible_instance evd b =
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd f)) ->
-	let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd f)) in
+    | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
+	let m = destMeta evd (strip_outer_cast evd f) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
@@ -1671,8 +1671,8 @@ let head_unfold_under_prod ts env sigma c =
       | Prod (n,t,c) -> mkProd (n,aux t, aux c)
       | _ ->
 	  let (h,l) = decompose_app_vect sigma c in
-	  match EConstr.kind sigma (EConstr.of_constr h) with
-	    | Const cst -> beta_app sigma (unfold cst, Array.map EConstr.of_constr l)
+	  match EConstr.kind sigma h with
+	    | Const cst -> beta_app sigma (unfold cst, l)
 	    | _ -> c in
   EConstr.Unsafe.to_constr (aux c)
 
-- 
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.

---
 pretyping/reductionops.ml | 79 +++++++++++++++++++++++------------------------
 1 file changed, 38 insertions(+), 41 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6ec3cd985c..45e7abcb79 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -588,10 +588,10 @@ end
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> constr -> Constr.constr
+type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> Constr.constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (Constr.constr, 'r) Sigma.sigma }
+type local_reduction_function = evar_map -> constr -> constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
 
 type contextual_stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
@@ -629,19 +629,18 @@ let safe_meta_value sigma ev =
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    let t = EConstr.of_constr (whdfun env sigma t) in
-    map_constr_with_full_binders sigma push_rel strongrec env t in
-  EConstr.Unsafe.to_constr (strongrec env t)
+    map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
+  strongrec env t
 
 let local_strong whdfun sigma =
-  let rec strongrec t = EConstr.map sigma strongrec (EConstr.of_constr (whdfun sigma t)) in
-  fun c -> EConstr.Unsafe.to_constr (strongrec c)
+  let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in
+  strongrec
 
 let rec strong_prodspine redfun sigma c =
-  let x = EConstr.of_constr (redfun sigma c) in
+  let x = redfun sigma c in
   match EConstr.kind sigma x with
-    | Prod (na,a,b) -> EConstr.Unsafe.to_constr (mkProd (na,a,EConstr.of_constr (strong_prodspine redfun sigma b)))
-    | _ -> EConstr.Unsafe.to_constr x
+    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
+    | _ -> x
 
 (*************************************)
 (*** Reduction using bindingss ***)
@@ -1140,7 +1139,7 @@ let iterate_whd_gen refold flags env sigma s =
   in aux s
 
 let red_of_state_red f sigma x =
-  EConstr.Unsafe.to_constr (Stack.zip sigma (f sigma (x,Stack.empty)))
+  Stack.zip sigma (f sigma (x,Stack.empty))
 
 (* 0. No Reduction Functions *)
 
@@ -1217,9 +1216,9 @@ let nf_evar = Evarutil.nf_evar
 let clos_norm_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
-    CClosure.norm_val
+    EConstr.of_constr (CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
-      (CClosure.inject (EConstr.Unsafe.to_constr t))
+      (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
@@ -1309,6 +1308,7 @@ let sigma_univ_state =
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
+  (** FIXME *)
   let x = EConstr.Unsafe.to_constr x in
   let y = EConstr.Unsafe.to_constr y in
   try
@@ -1352,8 +1352,8 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 (********************************************************************)
 
 let whd_meta sigma c = match EConstr.kind sigma c with
-  | Meta p -> (try meta_value sigma p with Not_found -> EConstr.Unsafe.to_constr c)
-  | _ -> EConstr.Unsafe.to_constr c
+  | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c)
+  | _ -> c
 
 let default_plain_instance_ident = Id.of_string "H"
 
@@ -1431,26 +1431,26 @@ let instance sigma s c =
  * error message. *)
 
 let hnf_prod_app env sigma t n =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Prod (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
 let hnf_prod_appvect env sigma t nl =
-  Array.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
 
 let hnf_prod_applist env sigma t nl =
-  List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  List.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
 
 let hnf_lam_app env sigma t n =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Lambda (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
 let hnf_lam_appvect env sigma t nl =
-  Array.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
 
 let hnf_lam_applist env sigma t nl =
-  List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  List.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
 
 let bind_assum (na, t) =
   (na, t)
@@ -1458,7 +1458,6 @@ let bind_assum (na, t) =
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
@@ -1470,7 +1469,6 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
@@ -1482,7 +1480,7 @@ let splay_lam env sigma =
 let splay_prod_assum env sigma =
   let rec prodec_rec env l c =
     let t = whd_allnolet env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    match EConstr.kind sigma t with
     | Prod (x,t,c)  ->
 	prodec_rec (push_rel (local_assum (x,t)) env)
 	  (Context.Rel.add (local_assum (x,t)) l) c
@@ -1491,9 +1489,9 @@ let splay_prod_assum env sigma =
 	  (Context.Rel.add (local_def (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
-      let t' = whd_all env sigma (EConstr.of_constr t) in
-	if Term.eq_constr t t' then l,t
-	else prodec_rec env l (EConstr.of_constr t')
+      let t' = whd_all env sigma t in
+	if EConstr.eq_constr sigma t t' then l,t
+	else prodec_rec env l t'
   in
   prodec_rec env Context.Rel.empty
 
@@ -1506,8 +1504,8 @@ let splay_arity env sigma c =
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
+    match EConstr.kind sigma (whd_all env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
@@ -1516,8 +1514,8 @@ let splay_prod_n env sigma n =
   decrec env n Context.Rel.empty
 
 let splay_lam_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
+    match EConstr.kind sigma (whd_all env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
@@ -1526,7 +1524,7 @@ let splay_lam_n env sigma n =
   decrec env n Context.Rel.empty
 
 let is_sort env sigma t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
   | Sort s -> true
   | _ -> false
 
@@ -1559,7 +1557,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    match EConstr.kind sigma t with
       | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | t -> t
@@ -1579,7 +1577,7 @@ let meta_value evd mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      EConstr.of_constr (instance evd metas (EConstr.of_constr b.rebus))
+      instance evd metas (EConstr.of_constr b.rebus)
     | None -> mkMeta mv
   in
   valrec mv
@@ -1589,7 +1587,7 @@ let meta_instance sigma b =
   if Metaset.is_empty fm then b.rebus
   else
     let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    EConstr.of_constr (instance sigma c_sigma b.rebus)
+    instance sigma c_sigma b.rebus
 
 let nf_meta sigma c =
   let c = EConstr.Unsafe.to_constr c in
@@ -1609,7 +1607,6 @@ let meta_reducible_instance evd b =
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
     let u = whd_betaiota Evd.empty u (** FIXME *) in
-    let u = EConstr.of_constr u in
     match EConstr.kind evd u with
     | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
 	let m = destMeta evd (strip_outer_cast evd c) in
@@ -1674,7 +1671,7 @@ let head_unfold_under_prod ts env sigma c =
 	  match EConstr.kind sigma h with
 	    | Const cst -> beta_app sigma (unfold cst, l)
 	    | _ -> c in
-  EConstr.Unsafe.to_constr (aux c)
+  aux c
 
 let betazetaevar_applist sigma n c l =
   let rec stacklam n env t stack =
@@ -1684,4 +1681,4 @@ let betazetaevar_applist sigma n c l =
     | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
     | Evar _, _ -> applist (substl env t, stack)
     | _ -> anomaly (Pp.str "Not enough lambda/let's") in
-  EConstr.Unsafe.to_constr (stacklam n [] c l)
+  stacklam n [] c l
-- 
cgit v1.2.3


From fa638c3e71752b6a59261776b36f1bed7d9c26d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 12:07:55 +0100
Subject: Cc API using EConstr.

---
 pretyping/reductionops.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 45e7abcb79..c796a91caa 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1221,6 +1221,14 @@ let clos_norm_flags flgs env sigma t =
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
+let clos_whd_flags flgs env sigma t =
+  try
+    let evars ev = safe_evar_value sigma ev in
+    EConstr.of_constr (CClosure.whd_val
+      (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.inject (EConstr.Unsafe.to_constr t)))
+  with e when is_anomaly e -> error "Tried to normalize ill-typed term"
+
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
 let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
 let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())
-- 
cgit v1.2.3


From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 15:50:17 +0100
Subject: Removing some return type compatibility layers in Termops.

---
 pretyping/reductionops.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c796a91caa..90c5b241b8 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -203,10 +203,10 @@ module Cst_stack = struct
     let reconstruct_head = List.fold_left
       (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
     List.fold_right
-      (fun (cst,params,args) t -> EConstr.of_constr (Termops.replace_term sigma
+      (fun (cst,params,args) t -> Termops.replace_term sigma
 	(reconstruct_head d args)
 	(applist (cst, List.rev params))
-	t)) cst_l c
+	t) cst_l c
 
   let pr l =
     let open Pp in
@@ -969,7 +969,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-	      if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
+	      if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
@@ -1068,7 +1068,7 @@ let local_whd_state_gen flags sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else mkApp (f,lc) in
-	      if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
+	      if noccurn sigma 1 u then (pop u,Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)
-- 
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.

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

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 90c5b241b8..bc5c629f4e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -210,7 +210,7 @@ module Cst_stack = struct
 
   let pr l =
     let open Pp in
-    let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+    let p_c c = Termops.print_constr c in
     prlist_with_sep pr_semicolon
       (fun (c,params,args) ->
 	hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
@@ -606,7 +606,7 @@ type local_state_reduction_function = evar_map -> state -> state
 
 let pr_state (tm,sk) =
   let open Pp in
-  let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+  let pr c = Termops.print_constr c in
   h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
 
 let local_assum (na, t) =
@@ -835,7 +835,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
 	let open Pp in
-	let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+	let pr c = Termops.print_constr c in
 	Feedback.msg_notice
              (h 0 (str "<<" ++ pr x ++
 		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
-- 
cgit v1.2.3


From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
---
 pretyping/reductionops.ml | 40 ++++++++++++++++------------------------
 1 file changed, 16 insertions(+), 24 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bc5c629f4e..a1585ef52b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -13,9 +13,9 @@ open Term
 open Termops
 open Univ
 open Evd
+open Environ
 open EConstr
 open Vars
-open Environ
 open Context.Rel.Declaration
 
 exception Elimconst
@@ -609,14 +609,6 @@ let pr_state (tm,sk) =
   let pr c = Termops.print_constr c in
   h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 (*************************************)
 (*** Reduction Functions Operators ***)
 (*************************************)
@@ -851,12 +843,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     match c0 with
     | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n (EConstr.of_constr body), stack)
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
       | _ -> fold ())
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) ->
-	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (EConstr.of_constr body, stack)
+	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
       | _ -> fold ())
     | Evar ev -> fold ()
     | Meta ev ->
@@ -958,7 +950,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
 	apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
-	let env' = push_rel (local_assum (na, t)) env in
+	let env' = push_rel (LocalAssum (na, t)) env in
 	let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
         (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
         | App (f,cl) ->
@@ -1468,7 +1460,7 @@ let splay_prod env sigma =
     let t = whd_all env sigma c in
     match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
+	  decrec (push_rel (LocalAssum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
       | _ -> m,t
   in
@@ -1479,7 +1471,7 @@ let splay_lam env sigma =
     let t = whd_all env sigma c in
     match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
+	  decrec (push_rel (LocalAssum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
       | _ -> m,t
   in
@@ -1490,11 +1482,11 @@ let splay_prod_assum env sigma =
     let t = whd_allnolet env sigma c in
     match EConstr.kind sigma t with
     | Prod (x,t,c)  ->
-	prodec_rec (push_rel (local_assum (x,t)) env)
-	  (Context.Rel.add (local_assum (x,t)) l) c
+	prodec_rec (push_rel (LocalAssum (x,t)) env)
+	  (Context.Rel.add (LocalAssum (x,t)) l) c
     | LetIn (x,b,t,c) ->
-	prodec_rec (push_rel (local_def (x,b,t)) env)
-	  (Context.Rel.add (local_def (x,b,t)) l) c
+	prodec_rec (push_rel (LocalDef (x,b,t)) env)
+	  (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
       let t' = whd_all env sigma t in
@@ -1515,8 +1507,8 @@ let splay_prod_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match EConstr.kind sigma (whd_all env sigma c) with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
-	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
+	  decrec (push_rel (LocalAssum (n,a)) env)
+	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_prod_n"
   in
   decrec env n Context.Rel.empty
@@ -1525,8 +1517,8 @@ let splay_lam_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match EConstr.kind sigma (whd_all env sigma c) with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
-	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
+	  decrec (push_rel (LocalAssum (n,a)) env)
+	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_lam_n"
   in
   decrec env n Context.Rel.empty
@@ -1566,8 +1558,8 @@ let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_all env sigma c in
     match EConstr.kind sigma t with
-      | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
-      | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
+      | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
+      | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
       | t -> t
   in
   decrec env
-- 
cgit v1.2.3


From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 pretyping/reductionops.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8be3b8328f..2703205386 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -550,7 +550,7 @@ struct
 
   let constr_of_cst_member f sk =
     match f with
-    | Cst_const (c, u) -> mkConstU (c,u), sk
+    | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk
     | Cst_proj p -> 
       match decomp sk with
       | Some (hd, sk) -> mkProj (p, hd), sk
@@ -703,7 +703,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
             csts Univ.LMap.empty
           in
           let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-          mkConstU (cst,inst)
+          mkConstU (cst, EInstance.make inst)
         | None -> bd
         end
     with
@@ -856,7 +856,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       | Some body -> whrec cst_l (EConstr.of_constr body, stack)
       | None -> fold ())
     | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) ->
-       (match constant_opt_value_in env const with
+        let u' = EInstance.kind sigma u in
+       (match constant_opt_value_in env (fst const, u') with
 	| None -> fold ()
 	| Some body ->
           let body = EConstr.of_constr body in
@@ -895,7 +896,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		    | None -> fold ()
 		    | Some (bef,arg,s') ->
 		      whrec Cst_stack.empty 
-			(arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s')
+			(arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
        )
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p env in
@@ -998,6 +999,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	      (match constant_opt_value_in env const with
 	      | None -> fold ()
 	      | Some body ->
+                let const = (fst const, EInstance.make (snd const)) in
                 let body = EConstr.of_constr body in
 		whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
 		  (body, s' @ (Stack.append_app [|x'|] s'')))
@@ -1657,12 +1659,13 @@ let meta_reducible_instance evd b =
 
 
 let head_unfold_under_prod ts env sigma c =
-  let unfold (cst,u as cstu) =
+  let unfold (cst,u) =
+    let cstu = (cst, EInstance.kind sigma u) in
     if Cpred.mem cst (snd ts) then
       match constant_opt_value_in env cstu with
 	| Some c -> EConstr.of_constr c
-	| None -> mkConstU cstu
-    else mkConstU cstu in
+	| None -> mkConstU (cst, u)
+    else mkConstU (cst, u) in
   let rec aux c =
     match EConstr.kind sigma c with
       | Prod (n,t,c) -> mkProd (n,aux t, aux c)
-- 
cgit v1.2.3