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/evarsolve.ml | 71 +++++++++++++++++++++++++-------------------------
 1 file changed, 36 insertions(+), 35 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bafb009f52..ea3ab17a75 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -73,7 +73,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
     match kind_of_term (whd_evar !evdref t) with
-    | App (f, args) when is_template_polymorphic env f ->
+    | App (f, args) when is_template_polymorphic env !evdref (EConstr.of_constr f) ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
     | App (f, args) when top && isEvar f -> 
@@ -356,14 +356,15 @@ let expansion_of_var aliases x =
   | [] -> x
   | a::_ -> a
 
-let rec expand_vars_in_term_using aliases t = match kind_of_term t with
+let rec expand_vars_in_term_using sigma aliases t = match kind_of_term t with
   | Rel _ | Var _ ->
       normalize_alias aliases t
   | _ ->
-      map_constr_with_full_binders
-        extend_alias expand_vars_in_term_using aliases t
+    let self aliases c = EConstr.of_constr (expand_vars_in_term_using sigma aliases (EConstr.Unsafe.to_constr c)) in
+    EConstr.Unsafe.to_constr (map_constr_with_full_binders sigma
+        extend_alias self aliases (EConstr.of_constr t))
 
-let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
+let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
@@ -430,8 +431,8 @@ let constr_list_distinct l =
     | [] -> true
   in loop l
 
-let get_actual_deps aliases l t =
-  if occur_meta_or_existential t then
+let get_actual_deps evd aliases l t =
+  if occur_meta_or_existential evd (EConstr.of_constr t) then
     (* Probably no restrictions on allowed vars in presence of evars *)
     l
   else
@@ -460,21 +461,21 @@ let remove_instance_local_defs evd evk args =
 
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
-let find_unification_pattern_args env l t =
+let find_unification_pattern_args env evd l t =
   if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
     let aliases = make_alias_map env in
     match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
-    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
+    | Some l as x when constr_list_distinct (get_actual_deps evd aliases l t) -> x
     | _ -> None
   else
     None
 
-let is_unification_pattern_meta env nb m l t =
+let is_unification_pattern_meta env evd nb m l t =
   (* Variables from context and rels > nb are implicitly all there *)
   (* so we need to be a rel <= nb *)
   if List.for_all (fun x -> isRel x && destRel x <= nb) l then
-    match find_unification_pattern_args env l t with
-    | Some _ as x when not (dependent (mkMeta m) t) -> x
+    match find_unification_pattern_args env evd l t with
+    | Some _ as x when not (dependent evd (EConstr.mkMeta m) (EConstr.of_constr t)) -> x
     | _ -> None
   else
     None
@@ -485,7 +486,7 @@ let is_unification_pattern_evar env evd (evk,args) l t =
   then
     let args = remove_instance_local_defs evd evk args in
     let n = List.length args in
-      match find_unification_pattern_args env (args @ l) t with
+      match find_unification_pattern_args env evd (args @ l) t with
       | Some l -> Some (List.skipn n l)
       | _ -> None
   else None
@@ -498,7 +499,7 @@ let is_unification_pattern_pure_evar env evd (evk,args) t =
 
 let is_unification_pattern (env,nb) evd f l t =
   match kind_of_term f with
-  | Meta m -> is_unification_pattern_meta env nb m l t
+  | Meta m -> is_unification_pattern_meta env evd nb m l t
   | Evar ev -> is_unification_pattern_evar env evd ev l t
   | _ -> None
 
@@ -509,9 +510,9 @@ let is_unification_pattern (env,nb) evd f l t =
    *implicitly* depend on Vars but lambda abstraction will not reflect this
    dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
-let solve_pattern_eqn env l c =
+let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
-    let c' = subst_term (lift 1 a) (lift 1 c) in
+    let c' = subst_term sigma (EConstr.of_constr (lift 1 a)) (EConstr.of_constr (lift 1 c)) in
     match kind_of_term a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
@@ -550,7 +551,7 @@ let make_projectable_subst aliases sigma evi args =
         | LocalAssum (id,c), a::rest ->
             let a = whd_evar sigma a in
             let cstrs =
-              let a',args = decompose_app_vect a in
+              let a',args = decompose_app_vect sigma (EConstr.of_constr a) in
               match kind_of_term a' with
               | Construct cstr ->
                   let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
@@ -923,12 +924,12 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
 let set_of_evctx l =
   List.fold_left (fun s decl -> Id.Set.add (get_id decl) s) Id.Set.empty l
 
-let filter_effective_candidates evi filter candidates =
+let filter_effective_candidates evd evi filter candidates =
   match filter with
   | None -> candidates
   | Some filter ->
       let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
-      List.filter (fun a -> Id.Set.subset (collect_vars a) ids) candidates
+      List.filter (fun a -> Id.Set.subset (collect_vars evd (EConstr.of_constr a)) ids) candidates
 
 let filter_candidates evd evk filter candidates_update =
   let evi = Evd.find_undefined evd evk in
@@ -939,7 +940,7 @@ let filter_candidates evd evk filter candidates_update =
   match candidates with
   | None -> NoUpdate
   | Some l ->
-      let l' = filter_effective_candidates evi filter l in
+      let l' = filter_effective_candidates evd evi filter l in
       if List.length l = List.length l' && candidates_update = NoUpdate then
         NoUpdate
       else
@@ -952,7 +953,7 @@ let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
-  let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
+  let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in
   let test b decl = b || Idset.mem (get_id decl) vars ||
                     match decl with
                     | LocalAssum _ ->
@@ -999,7 +1000,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
 (* ?e is assumed to have no candidates *)
 
 let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
-  let rhs = expand_vars_in_term env rhs in
+  let rhs = expand_vars_in_term env evd rhs in
   let filter =
     restrict_upon_filter evd evk
       (* Keep only variables that occur in rhs *)
@@ -1010,7 +1011,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
       (* expands only rels and vars aliases, not rels or vars bound to an *)
       (* arbitrary complex term *)
       (fun a -> not (isRel a || isVar a)
-                || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols)
+                || dependent evd (EConstr.of_constr a) (EConstr.of_constr rhs) || List.exists (fun (id,_) -> isVarId id a) sols)
       argsv in
   let filter = closure_of_filter evd evk filter in
   let candidates = extract_candidates sols in
@@ -1060,7 +1061,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
   | _, None -> filter_candidates evd evk1 filter1 NoUpdate
   | None, Some _ -> raise DoesNotPreserveCandidateRestriction
   | Some l1, Some l2 ->
-      let l1 = filter_effective_candidates evi1 filter1 l1 in
+      let l1 = filter_effective_candidates evd evi1 filter1 l1 in
       let l1' = List.filter (fun c1 ->
         let c1' = instantiate_evar_array evi1 c1 argsv1 in
         let filter c2 =
@@ -1091,9 +1092,7 @@ exception CannotProject of evar_map * existential
 *)
 
 let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args2 = decompose_app_vect t in
-  let f,args1 = decompose_app_vect (whd_evar evd f) in
-  let args = Array.append args1 args2 in
+  let f,args = decompose_app_vect evd (EConstr.of_constr t) in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
@@ -1450,7 +1449,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     | _ ->
         progress := true;
         match
-          let c,args = decompose_app_vect t in
+          let c,args = decompose_app_vect !evdref (EConstr.of_constr t) in
           match kind_of_term c with
           | Construct (cstr,u) when noccur_between 1 k t ->
             (* This is common case when inferring the return clause of match *)
@@ -1466,10 +1465,11 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             let ty = get_type_of env' !evdref t in
             let candidates =
               try
+                let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
                 let t =
-                  map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-                    imitate envk t in
-                t::l
+                  map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+                    self envk (EConstr.of_constr t) in
+                EConstr.Unsafe.to_constr t::l
               with e when CErrors.noncritical e -> l in
             (match candidates with
             | [x] -> x
@@ -1480,8 +1480,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
               evar'')
         | None ->
            (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-	   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-					imitate envk t
+          let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
+          EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+					self envk (EConstr.of_constr t))
   in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
@@ -1498,7 +1499,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     in
       is_id_subst filter_ctxt (Array.to_list argsv) &&
       closed0 rhs &&
-      Idset.subset (collect_vars rhs) !names 
+      Idset.subset (collect_vars evd (EConstr.of_constr rhs)) !names 
   in
   let body =
     if fast rhs then nf_evar evd rhs
@@ -1530,7 +1531,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
   with NoCandidates ->
   try
     let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in
-    if occur_meta body then raise MetaOccurInBodyInternal;
+    if occur_meta evd' (EConstr.of_constr body) then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
     if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
-- 
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/evarsolve.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ea3ab17a75..17bb1406e2 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -145,7 +145,7 @@ let recheck_applications conv_algo env evdref t =
        let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
-	 match kind_of_term (whd_all env !evdref ty) with
+	 match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with
 	 | Prod (na, dom, codom) ->
 	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
@@ -525,7 +525,7 @@ let solve_pattern_eqn env sigma l c =
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
      is not in normal form *)
-  shrink_eta c'
+  shrink_eta (EConstr.of_constr c')
 
 (*****************************************)
 (* Refining/solving unification problems *)
@@ -683,7 +683,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
       List.filter (fun (args',id) ->
         (* is_conv is maybe too strong (and source of useless computation) *)
         (* (at least expansion of aliases is needed) *)
-        Array.for_all2 (is_conv env evd) args args') l in
+        Array.for_all2 (fun c1 c2 -> is_conv env evd (EConstr.of_constr c1) (EConstr.of_constr c2)) args args') l in
     List.map snd l
   with Not_found ->
     []
@@ -808,7 +808,7 @@ let rec do_projection_effects define_fun env ty evd = function
       let evd = Evd.define evk (mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = whd_all env evd (Lazy.force ty) in
+      let ty = whd_all env evd (EConstr.of_constr (Lazy.force ty)) in
       if not (isSort ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -1484,7 +1484,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
 					self envk (EConstr.of_constr t))
   in
-  let rhs = whd_beta evd rhs (* heuristic *) in
+  let rhs = whd_beta evd (EConstr.of_constr rhs) (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
     let names = ref Idset.empty in
@@ -1566,10 +1566,10 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         raise e
     | OccurCheckIn (evd,rhs) ->
         (* last chance: rhs actually reduces to ev *)
-        let c = whd_all env evd rhs in
+        let c = whd_all env evd (EConstr.of_constr rhs) in
         match kind_of_term c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
-	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
+	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma (EConstr.of_constr c) (EConstr.of_constr c'))
               env evd pbty evk argsv argsv2
         | _ ->
 	    raise (OccurCheckIn (evd,rhs))
@@ -1638,5 +1638,5 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
     | IllTypedInstance (env,t,u) ->
         UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))
     | IncompatibleCandidates ->
-        UnifFailure (evd,ConversionFailed (env,mkEvar ev1,t2))
+        UnifFailure (evd,ConversionFailed (env,mkEvar ev1, EConstr.Unsafe.to_constr t2))
 
-- 
cgit v1.2.3


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

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

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 17bb1406e2..86ef8f56f1 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -141,8 +141,8 @@ let recheck_applications conv_algo env evdref t =
     match kind_of_term t with
     | App (f, args) ->
        let () = aux env f in
-       let fty = Retyping.get_type_of env !evdref f in
-       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
+       let fty = Retyping.get_type_of env !evdref (EConstr.of_constr f) in
+       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref (EConstr.of_constr x)) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
 	 match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with
@@ -634,7 +634,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in
       let id = next_name_away na avoid in
       let evd,t_in_sign =
-        let s = Retyping.get_sort_of env evd t_in_env in
+        let s = Retyping.get_sort_of env evd (EConstr.of_constr t_in_env) in
         let evd,ty_t_in_sign = refresh_universes
 	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
@@ -653,7 +653,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
   in
   let evd,ev2ty_in_sign =
-    let s = Retyping.get_sort_of env evd ty_in_env in
+    let s = Retyping.get_sort_of env evd (EConstr.of_constr ty_in_env) in
     let evd,ty_t_in_sign = refresh_universes
      ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
@@ -1161,7 +1161,7 @@ let check_evar_instance evd evk1 body conv_algo =
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
-    try Retyping.get_type_of ~lax:true evenv evd body
+    try Retyping.get_type_of ~lax:true evenv evd (EConstr.of_constr body)
     with Retyping.RetypeError _ -> error "Ill-typed evar instance"
   in
   match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
@@ -1365,7 +1365,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | (id,p)::_::_ ->
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
-      let ty = lazy (Retyping.get_type_of env !evdref t) in
+      let ty = lazy (Retyping.get_type_of env !evdref (EConstr.of_constr t)) in
       let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
       evdref := evd;
       c
@@ -1428,7 +1428,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           if not !progress then
             raise (NotEnoughInformationEvarEvar t);
           (* Make the virtual left evar real *)
-          let ty = get_type_of env' evd t in
+          let ty = get_type_of env' evd (EConstr.of_constr t) in
           let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
@@ -1462,7 +1462,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           | _ -> None
         with
         | Some l ->
-            let ty = get_type_of env' !evdref t in
+            let ty = get_type_of env' !evdref (EConstr.of_constr t) in
             let candidates =
               try
                 let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
-- 
cgit v1.2.3


From b7fd585b89ac5e0b7770f52739c33fe179f2eed8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Nov 2016 21:36:40 +0100
Subject: Evarsolve API using EConstr.

---
 pretyping/evarsolve.ml | 475 ++++++++++++++++++++++++++-----------------------
 1 file changed, 255 insertions(+), 220 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 86ef8f56f1..8a22aed2f2 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -22,13 +22,14 @@ open Pretype_errors
 open Sigma.Notations
 
 let normalize_evar evd ev =
-  match kind_of_term (whd_evar evd (mkEvar ev)) with
+  let open EConstr in
+  match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
   | _ -> assert false
 
-let get_polymorphic_positions f = 
+let get_polymorphic_positions sigma f =
   let open Declarations in
-  match kind_of_term f with
+  match EConstr.kind sigma f with
   | Ind (ind, u) | Construct ((ind, _), u) -> 
     let mib,oib = Global.lookup_inductive ind in
       (match oib.mind_arity with
@@ -49,10 +50,11 @@ let refresh_level evd s =
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
+  let open EConstr in
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
-    match kind_of_term t with
+    match EConstr.kind !evdref t with
     | Sort (Type u as s) when
       (match Univ.universe_level u with
       | None -> true
@@ -72,20 +74,20 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
-    match kind_of_term (whd_evar !evdref t) with
-    | App (f, args) when is_template_polymorphic env !evdref (EConstr.of_constr f) ->
-      let pos = get_polymorphic_positions f in
+    match EConstr.kind !evdref t with
+    | App (f, args) when is_template_polymorphic env !evdref f ->
+      let pos = get_polymorphic_positions !evdref f in
 	refresh_polymorphic_positions args pos
-    | App (f, args) when top && isEvar f -> 
+    | App (f, args) when top && isEvar !evdref f -> 
       refresh_term_evars true false f; 
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh univ_flexible true evi.evar_concl in
+      let ty' = refresh univ_flexible true (EConstr.of_constr evi.evar_concl) in
 	if !modified then 
-	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
+	  evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'}
 	else ()
-    | _ -> Constr.iter (refresh_term_evars onevars false) t
+    | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t
   and refresh_polymorphic_positions args pos =
     let rec aux i = function
       | Some l :: ls -> 
@@ -100,17 +102,17 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
     in aux 0 pos
   in
   let t' = 
-    if isArity t then
+    if isArity !evdref t then
       (match pbty with
       | None -> t
       | Some dir -> refresh status dir t)
     else (refresh_term_evars false true t; t)
   in
-    if !modified then !evdref, t' else !evdref, t
+    if !modified then !evdref, EConstr.Unsafe.to_constr t' else !evdref, EConstr.Unsafe.to_constr t
 
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
-    refresh_universes (Some false) env sigma ty
+    refresh_universes (Some false) env sigma (EConstr.of_constr ty)
 		      
 
 (************************)
@@ -127,6 +129,8 @@ let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
 let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
+  let t1 = EConstr.Unsafe.to_constr t1 in
+  let t2 = EConstr.Unsafe.to_constr t2 in
   match pbty with
   | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
   | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
@@ -134,29 +138,30 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
 
 (* We retype applications to ensure the universe constraints are collected *)
 
-exception IllTypedInstance of env * types * types
+exception IllTypedInstance of env * EConstr.types * EConstr.types
 
 let recheck_applications conv_algo env evdref t =
+  let open EConstr in
   let rec aux env t =
-    match kind_of_term t with
+    match EConstr.kind !evdref t with
     | App (f, args) ->
        let () = aux env f in
-       let fty = Retyping.get_type_of env !evdref (EConstr.of_constr f) in
-       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref (EConstr.of_constr x)) args in
+       let fty = Retyping.get_type_of env !evdref f in
+       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
-	 match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with
+	 match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with
 	 | Prod (na, dom, codom) ->
-	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
+	    (match conv_algo env !evdref Reduction.CUMUL (EConstr.of_constr argsty.(i)) dom with
 	     | Success evd -> evdref := evd;
-			     aux (succ i) (subst1 args.(i) codom)
+			     aux (succ i) (Vars.subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
-		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
-	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
+		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), EConstr.Unsafe.to_constr dom))
+	 | _ -> raise (IllTypedInstance (env, ty, EConstr.of_constr argsty.(i)))
        else ()
-     in aux 0 fty
+     in aux 0 (EConstr.of_constr fty)
     | _ ->
-       iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t
+       iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t
   in aux env t
 
 	  
@@ -169,7 +174,7 @@ type 'a update =
 | NoUpdate
 
 open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
+let inst_of_vars sign = Array.map_of_list (get_id %> EConstr.mkVar) sign
 
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
@@ -186,7 +191,7 @@ let restrict_evar_key evd evk filter candidates =
       | Some filter -> filter in
       let candidates = match candidates with
       | NoUpdate -> evi.evar_candidates
-      | UpdateWith c -> Some c in
+      | UpdateWith c -> Some (List.map EConstr.Unsafe.to_constr c) in
       let sigma = Sigma.Unsafe.of_evar_map evd in
       let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
       (Sigma.to_evar_map sigma, evk)
@@ -216,27 +221,25 @@ let restrict_instance evd evk filter argsv =
 
 open Context.Rel.Declaration
 let noccur_evar env evd evk c =
+  let open EConstr in
   let cache = ref Int.Set.empty (* cache for let-ins *) in
   let rec occur_rec check_types (k, env as acc) c =
-  match kind_of_term c with
+  match EConstr.kind evd c with
   | Evar (evk',args' as ev') ->
-      (match safe_evar_value evd ev' with
-       | Some c -> occur_rec check_types acc c
-       | None ->
-           if Evar.equal evk evk' then raise Occur
-           else (if check_types then
-                   occur_rec false acc (existential_type evd ev');
-                 Array.iter (occur_rec check_types acc) args'))
+    if Evar.equal evk evk' then raise Occur
+    else (if check_types then
+            occur_rec false acc (existential_type evd ev');
+          Array.iter (occur_rec check_types acc) args')
   | Rel i when i > k ->
      if not (Int.Set.mem (i-k) !cache) then
        let decl = Environ.lookup_rel i env in
        if check_types then
-         (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (get_type decl)));
+         (cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr (get_type decl))));
        (match decl with
         | LocalAssum _ -> ()
-        | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b))
+        | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr b)))
   | Proj (p,c) -> occur_rec true acc c
-  | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
+  | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env))
     (occur_rec check_types) acc c
   in
   try occur_rec false (0,env) c; true with Occur -> false
@@ -249,13 +252,14 @@ let noccur_evar env evd evk c =
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
 
-let compute_var_aliases sign =
+let compute_var_aliases sign sigma =
   let open Context.Named.Declaration in
   List.fold_right (fun decl aliases ->
     let id = get_id decl in
     match decl with
     | LocalDef (_,t,_) ->
-        (match kind_of_term t with
+        let t = EConstr.of_constr t in
+        (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_id =
               try Id.Map.find id' aliases with Not_found -> [] in
@@ -265,13 +269,16 @@ let compute_var_aliases sign =
     | LocalAssum _ -> aliases)
     sign Id.Map.empty
 
-let compute_rel_aliases var_aliases rels =
+let compute_rel_aliases var_aliases rels sigma =
+  let open EConstr in
   snd (List.fold_right
 	 (fun decl (n,aliases) ->
 	  (n-1,
 	   match decl with
 	   | LocalDef (_,t,u) ->
-	      (match kind_of_term t with
+              let t = EConstr.of_constr t in
+              let u = EConstr.of_constr u in
+	      (match EConstr.kind sigma t with
 	       | Var id' ->
 		  let aliases_of_n =
 		    try Id.Map.find id' var_aliases with Not_found -> [] in
@@ -281,52 +288,57 @@ let compute_rel_aliases var_aliases rels =
 		    try Int.Map.find (p+n) aliases with Not_found -> [] in
 		  Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
 	       | _ ->
-		  Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
+		  Int.Map.add n [Vars.lift n (mkCast(t,DEFAULTcast,u))] aliases)
 	   | LocalAssum _ -> aliases)
 	 )
 	 rels
 	 (List.length rels,Int.Map.empty))
 
-let make_alias_map env =
+let make_alias_map env sigma =
   (* We compute the chain of aliases for each var and rel *)
-  let var_aliases = compute_var_aliases (named_context env) in
-  let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
+  let var_aliases = compute_var_aliases (named_context env) sigma in
+  let rel_aliases = compute_rel_aliases var_aliases (rel_context env) sigma in
   (var_aliases,rel_aliases)
 
 let lift_aliases n (var_aliases,rel_aliases as aliases) =
+  let open EConstr in
   if Int.equal n 0 then aliases else
   (var_aliases,
-   Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
+   Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (Vars.lift n) l))
      rel_aliases Int.Map.empty)
 
-let get_alias_chain_of aliases x = match kind_of_term x with
+let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with
   | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
   | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> [])
   | _ -> []
 
-let normalize_alias_opt aliases x =
-  match get_alias_chain_of aliases x with
+let normalize_alias_opt sigma aliases x =
+  let open EConstr in
+  match get_alias_chain_of sigma aliases x with
   | []  -> None
-  | a::_ when isRel a || isVar a -> Some a
+  | a::_ when isRel sigma a || isVar sigma a -> Some a
   | [_] -> None
   | _::a::_ -> Some a
 
-let normalize_alias aliases x =
-  match normalize_alias_opt aliases x with
+let normalize_alias sigma aliases x =
+  match normalize_alias_opt sigma aliases x with
   | Some a -> a
   | None -> x
 
-let normalize_alias_var var_aliases id =
-  destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id))
+let normalize_alias_var sigma var_aliases id =
+  let open EConstr in
+  destVar sigma (normalize_alias sigma (var_aliases,Int.Map.empty) (mkVar id))
 
-let extend_alias decl (var_aliases,rel_aliases) =
+let extend_alias sigma decl (var_aliases,rel_aliases) =
+  let open EConstr in
   let rel_aliases =
-    Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
+    Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (Vars.lift 1) l))
       rel_aliases Int.Map.empty in
   let rel_aliases =
     match decl with
     | LocalDef(_,t,_) ->
-        (match kind_of_term t with
+        let t = EConstr.of_constr t in
+        (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_binder =
               try Id.Map.find id' var_aliases with Not_found -> [] in
@@ -336,37 +348,38 @@ let extend_alias decl (var_aliases,rel_aliases) =
               try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
             Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
         | _ ->
-            Int.Map.add 1 [lift 1 t] rel_aliases)
+            Int.Map.add 1 [Vars.lift 1 t] rel_aliases)
     | LocalAssum _ -> rel_aliases in
   (var_aliases, rel_aliases)
 
-let expand_alias_once aliases x =
-  match get_alias_chain_of aliases x with
+let expand_alias_once sigma aliases x =
+  match get_alias_chain_of sigma aliases x with
   | []  -> None
   | l -> Some (List.last l)
 
-let expansions_of_var aliases x =
-  match get_alias_chain_of aliases x with
+let expansions_of_var sigma aliases x =
+  let open EConstr in
+  match get_alias_chain_of sigma aliases x with
   | [] -> [x]
-  | a::_ as l when isRel a || isVar a -> x :: List.rev l
+  | a::_ as l when isRel sigma a || isVar sigma a -> x :: List.rev l
   | _::l -> x :: List.rev l
 
-let expansion_of_var aliases x =
-  match get_alias_chain_of aliases x with
+let expansion_of_var sigma aliases x =
+  match get_alias_chain_of sigma aliases x with
   | [] -> x
   | a::_ -> a
 
-let rec expand_vars_in_term_using sigma aliases t = match kind_of_term t with
+let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with
   | Rel _ | Var _ ->
-      normalize_alias aliases t
+      normalize_alias sigma aliases t
   | _ ->
-    let self aliases c = EConstr.of_constr (expand_vars_in_term_using sigma aliases (EConstr.Unsafe.to_constr c)) in
-    EConstr.Unsafe.to_constr (map_constr_with_full_binders sigma
-        extend_alias self aliases (EConstr.of_constr t))
+    let self aliases c = expand_vars_in_term_using sigma aliases c in
+    map_constr_with_full_binders sigma (extend_alias sigma) self aliases t
 
-let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env)
+let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
 
-let free_vars_and_rels_up_alias_expansion aliases c =
+let free_vars_and_rels_up_alias_expansion sigma aliases c =
+  let open EConstr in
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
   let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
@@ -379,25 +392,25 @@ let free_vars_and_rels_up_alias_expansion aliases c =
     | Var s -> cache_var := Id.Set.add s !cache_var
     | _ -> () in
   let rec frec (aliases,depth) c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Rel _ | Var _ as ck ->
       if is_in_cache depth ck then () else begin
       put_in_cache depth ck;
-      let c' = expansion_of_var aliases c in
-      (if c != c' then (* expansion, hence a let-in *)
-        match kind_of_term c with
+      let c' = expansion_of_var sigma aliases c in
+      (if c != c' then (* expansion, hence a let-in *) (** FIXME *)
+        match EConstr.kind sigma c with
         | Var id -> acc4 := Id.Set.add id !acc4
         | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
         | _ -> ());
-      match kind_of_term c' with
+      match EConstr.kind sigma c' with
         | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        acc2 := Id.Set.union (vars_of_global (Global.env()) c) !acc2
+        acc2 := Id.Set.union (vars_of_global (Global.env()) (EConstr.to_constr sigma c)) !acc2
     | _ ->
-        iter_constr_with_full_binders
-          (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
+        iter_with_full_binders sigma
+          (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
           frec (aliases,depth) c
   in
   frec (aliases,0) c;
@@ -407,11 +420,11 @@ let free_vars_and_rels_up_alias_expansion aliases c =
 (* Managing pattern-unification *)
 (********************************)
 
-let rec expand_and_check_vars aliases = function
+let rec expand_and_check_vars sigma aliases = function
   | [] -> []
-  | a::l when isRel a || isVar a ->
-      let a = expansion_of_var aliases a in
-      if isRel a || isVar a then a :: expand_and_check_vars aliases l
+  | a::l when EConstr.isRel sigma a || EConstr.isVar sigma a ->
+      let a = expansion_of_var sigma aliases a in
+      if EConstr.isRel sigma a || EConstr.isVar sigma a then a :: expand_and_check_vars sigma aliases l
       else raise Exit
   | _ ->
       raise Exit
@@ -422,24 +435,25 @@ module Constrhash = Hashtbl.Make
           let hash = hash_constr
    end)
 
-let constr_list_distinct l =
+let constr_list_distinct sigma l =
   let visited = Constrhash.create 23 in
   let rec loop = function
     | h::t ->
+        let h = EConstr.to_constr sigma h in
         if Constrhash.mem visited h then false
         else (Constrhash.add visited h h; loop t)
     | [] -> true
   in loop l
 
 let get_actual_deps evd aliases l t =
-  if occur_meta_or_existential evd (EConstr.of_constr t) then
+  if occur_meta_or_existential evd t then
     (* Probably no restrictions on allowed vars in presence of evars *)
     l
   else
     (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in
+    let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion evd aliases t in
     List.filter (fun c ->
-      match kind_of_term c with
+      match EConstr.kind evd c with
       | Var id -> Id.Set.mem id fv_ids
       | Rel n -> Int.Set.mem n fv_rels
       | _ -> assert false) l
@@ -462,10 +476,11 @@ let remove_instance_local_defs evd evk args =
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
 let find_unification_pattern_args env evd l t =
-  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
-    let aliases = make_alias_map env in
-    match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
-    | Some l as x when constr_list_distinct (get_actual_deps evd aliases l t) -> x
+  let open EConstr in
+  if List.for_all (fun x -> isRel evd x || isVar evd x) l (* common failure case *) then
+    let aliases = make_alias_map env evd in
+    match (try Some (expand_and_check_vars evd aliases l) with Exit -> None) with
+    | Some l as x when constr_list_distinct evd (get_actual_deps evd aliases l t) -> x
     | _ -> None
   else
     None
@@ -473,15 +488,17 @@ let find_unification_pattern_args env evd l t =
 let is_unification_pattern_meta env evd nb m l t =
   (* Variables from context and rels > nb are implicitly all there *)
   (* so we need to be a rel <= nb *)
-  if List.for_all (fun x -> isRel x && destRel x <= nb) l then
+  let open EConstr in
+  if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then
     match find_unification_pattern_args env evd l t with
-    | Some _ as x when not (dependent evd (EConstr.mkMeta m) (EConstr.of_constr t)) -> x
+    | Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x
     | _ -> None
   else
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l 
+  let open EConstr in
+  if List.for_all (fun x -> isRel evd x || isVar evd x) l 
     && noccur_evar env evd evk t
   then
     let args = remove_instance_local_defs evd evk args in
@@ -498,7 +515,7 @@ let is_unification_pattern_pure_evar env evd (evk,args) t =
   | Some _ -> true
 
 let is_unification_pattern (env,nb) evd f l t =
-  match kind_of_term f with
+  match EConstr.kind evd f with
   | Meta m -> is_unification_pattern_meta env evd nb m l t
   | Evar ev -> is_unification_pattern_evar env evd ev l t
   | _ -> None
@@ -511,21 +528,23 @@ let is_unification_pattern (env,nb) evd f l t =
    dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
 let solve_pattern_eqn env sigma l c =
+  let open EConstr in
   let c' = List.fold_right (fun a c ->
-    let c' = subst_term sigma (EConstr.of_constr (lift 1 a)) (EConstr.of_constr (lift 1 c)) in
-    match kind_of_term a with
+    let c' = subst_term sigma (Vars.lift 1 a) (Vars.lift 1 c) in
+    match EConstr.kind sigma a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let open Context.Rel.Declaration in
           let d = map_constr (lift n) (lookup_rel n env) in
+          let c' = EConstr.of_constr c' in
           mkLambda_or_LetIn d c'
       | Var id ->
-          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
+          let d = lookup_named id env in EConstr.of_constr (mkNamedLambda_or_LetIn d c')
       | _ -> assert false)
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
      is not in normal form *)
-  shrink_eta (EConstr.of_constr c')
+  shrink_eta c'
 
 (*****************************************)
 (* Refining/solving unification problems *)
@@ -543,35 +562,33 @@ let solve_pattern_eqn env sigma l c =
 
 let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
-  let evar_aliases = compute_var_aliases sign in
+  let evar_aliases = compute_var_aliases sign sigma in
   let (_,full_subst,cstr_subst) =
     List.fold_right
       (fun decl (args,all,cstrs) ->
         match decl,args with
         | LocalAssum (id,c), a::rest ->
-            let a = whd_evar sigma a in
             let cstrs =
-              let a',args = decompose_app_vect sigma (EConstr.of_constr a) in
-              match kind_of_term a' with
+              let a',args = decompose_app_vect sigma a in
+              match EConstr.kind sigma (EConstr.of_constr a') with
               | Construct cstr ->
                   let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
                   Constrmap.add (fst cstr) ((args,id)::l) cstrs
               | _ -> cstrs in
-            (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
+            (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)
         | LocalDef (id,c,_), a::rest ->
-            let a = whd_evar sigma a in
-            (match kind_of_term c with
+            (match EConstr.kind sigma (EConstr.of_constr c) with
             | Var id' ->
-                let idc = normalize_alias_var evar_aliases id' in
+                let idc = normalize_alias_var sigma evar_aliases id' in
                 let sub = try Id.Map.find idc all with Not_found -> [] in
-                if List.exists (fun (c,_,_) -> Term.eq_constr a c) sub then
+                if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then
                   (rest,all,cstrs)
                 else
                   (rest,
-                   Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
+                   Id.Map.add idc ((a,normalize_alias_opt sigma aliases a,id)::sub) all,
                    cstrs)
             | _ ->
-                (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
+                (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs))
         | _ -> anomaly (Pp.str "Instance does not match its signature"))
       sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
   (full_subst,cstr_subst)
@@ -587,15 +604,18 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
+  let open EConstr in
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in
   let evd = Sigma.to_evar_map evd in
-  let t_in_env = whd_evar evd t_in_env in
-  let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
+  let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
+  let evar_in_env = EConstr.of_constr evar_in_env in
+  let (evk, _) = destEvar evd evar_in_env in
+  let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
-  let evar_in_sign = mkEvar (fst (destEvar evar_in_env), inst_in_sign) in
-  (evd,whd_evar evd evar_in_sign)
+  let evar_in_sign = mkEvar (evk, inst_in_sign) in
+  (evd,whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign))
 
 (* We have x1..xq |- ?e1 : τ and had to solve something like
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
@@ -617,10 +637,11 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
 exception MorePreciseOccurCheckNeeeded
 
 let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+  let open EConstr in
   if Evd.is_defined evd evk1 then
       (* Some circularity somewhere (see e.g. #3209) *)
       raise MorePreciseOccurCheckNeeeded;
-  let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in
+  let (evk1,args1) = EConstr.destEvar evd (EConstr.mkEvar (evk1,args1)) in
   let evi1 = Evd.find_undefined evd evk1 in
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
@@ -634,36 +655,38 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in
       let id = next_name_away na avoid in
       let evd,t_in_sign =
-        let s = Retyping.get_sort_of env evd (EConstr.of_constr t_in_env) in
+        let t_in_env = EConstr.of_constr t_in_env in
+        let s = Retyping.get_sort_of env evd t_in_env in
         let evd,ty_t_in_sign = refresh_universes
-	 ~status:univ_flexible (Some false) env evd (mkSort s) in
+	 ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,d' = match d with
       | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
       | LocalDef (_,b,_) ->
+          let b = EConstr.of_constr b in
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
           evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
       (push_named_context_val d' sign, Filter.extend 1 filter,
-       (mkRel 1)::(List.map (lift 1) inst_in_env),
-       (mkRel 1)::(List.map (lift 1) inst_in_sign),
+       (mkRel 1)::(List.map (Vars.lift 1) inst_in_env),
+       (mkRel 1)::(List.map (Vars.lift 1) inst_in_sign),
        push_rel d env,evd,id::avoid))
       rel_sign
       (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
   in
   let evd,ev2ty_in_sign =
-    let s = Retyping.get_sort_of env evd (EConstr.of_constr ty_in_env) in
+    let s = Retyping.get_sort_of env evd ty_in_env in
     let evd,ty_t_in_sign = refresh_universes
-     ~status:univ_flexible (Some false) env evd (mkSort s) in
+     ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (ev2_in_sign, evd, _) =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
+    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src (List.map EConstr.Unsafe.to_constr inst2_in_sign) in
   let evd = Sigma.to_evar_map evd in
-  let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
-  (evd, ev2_in_sign, ev2_in_env)
+  let ev2_in_env = (fst (destEvar evd (EConstr.of_constr ev2_in_sign)), Array.of_list inst2_in_env) in
+  (evd, EConstr.of_constr ev2_in_sign, ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
   let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
@@ -722,7 +745,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
 
 type evar_projection =
 | ProjectVar
-| ProjectEvar of existential * evar_info * Id.t * evar_projection
+| ProjectEvar of EConstr.existential * evar_info * Id.t * evar_projection
 
 exception NotUnique
 exception NotUniqueInType of (Id.t * evar_projection) list
@@ -730,19 +753,19 @@ exception NotUniqueInType of (Id.t * evar_projection) list
 let rec assoc_up_to_alias sigma aliases y yc = function
   | [] -> raise Not_found
   | (c,cc,id)::l ->
-      let c' = whd_evar sigma c in
-      if Term.eq_constr y c' then id
+      if EConstr.eq_constr sigma y c then id
       else
         match l with
         | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
         | [] ->
           (* Last chance, we reason up to alias conversion *)
-          match (if c == c' then cc else normalize_alias_opt aliases c') with
-          | Some cc when Term.eq_constr yc cc -> id
-          | _ -> if Term.eq_constr yc c then id else raise Not_found
+          match (normalize_alias_opt sigma aliases c) with
+          | Some cc when EConstr.eq_constr sigma yc cc -> id
+          | _ -> if EConstr.eq_constr sigma yc c then id else raise Not_found
 
 let rec find_projectable_vars with_evars aliases sigma y subst =
-  let yc = normalize_alias aliases y in
+  let open EConstr in
+  let yc = normalize_alias sigma aliases y in
   let is_projectable idc idcl subst' =
     (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
     try
@@ -752,12 +775,12 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
     (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
     (* projectable on [y] *)
       if with_evars then
-        let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in
+        let f (c,_,id) = isEvar sigma c in
         let idcl' = List.filter f idcl in
         match idcl' with
         | [c,_,id] ->
           begin
-            let (evk,argsv as t) = destEvar c in
+            let (evk,argsv as t) = destEvar sigma c in
             let evi = Evd.find sigma evk in
             let subst,_ = make_projectable_subst aliases sigma evi argsv in
             let l = find_projectable_vars with_evars aliases sigma y subst in
@@ -805,19 +828,19 @@ let rec find_solution_type evarenv = function
 let rec do_projection_effects define_fun env ty evd = function
   | ProjectVar -> evd
   | ProjectEvar ((evk,argsv),evi,id,p) ->
-      let evd = Evd.define evk (mkVar id) evd in
+      let open EConstr in
+      let evd = Evd.define evk (Constr.mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = whd_all env evd (EConstr.of_constr (Lazy.force ty)) in
-      if not (isSort ty) then
+      let ty = EConstr.of_constr (whd_all env evd (Lazy.force ty)) in
+      if not (isSort evd ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
            one (however, regarding coercions, because t is obtained by
            unif, we know that no coercion can be inserted) *)
         let subst = make_pure_subst evi argsv in
-        let ty' = replace_vars subst evi.evar_concl in
-        let ty' = whd_evar evd ty' in
-        if isEvar ty' then define_fun env evd (Some false) (destEvar ty') ty else evd
+        let ty' = Vars.replace_vars subst (EConstr.of_constr evi.evar_concl) in
+        if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd
       else
         evd
 
@@ -843,7 +866,7 @@ let rec do_projection_effects define_fun env ty evd = function
 
 type projectibility_kind =
   | NoUniqueProjection
-  | UniqueProjection of constr * evar_projection list
+  | UniqueProjection of EConstr.constr * evar_projection list
 
 type projectibility_status =
   | CannotInvert
@@ -851,16 +874,16 @@ type projectibility_status =
 
 let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
   let effects = ref [] in
+  let open EConstr in
   let rec aux k t =
-    let t = whd_evar evd t in
-    match kind_of_term t with
+    match EConstr.kind evd t with
     | Rel i when i>k0+k -> aux' k (mkRel (i-k))
     | Var id -> aux' k t
-    | _ -> map_constr_with_binders succ aux k t
+    | _ -> map_with_binders evd succ aux k t
   and aux' k t =
-    try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
+    try EConstr.of_constr (project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders)
     with Not_found ->
-      match expand_alias_once aliases t with
+      match expand_alias_once evd aliases t with
       | None -> raise Not_found
       | Some c -> aux k c in
   try
@@ -895,7 +918,7 @@ let extract_unique_projection = function
 let extract_candidates sols =
   try
     UpdateWith
-      (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
+      (List.map (function (id,ProjectVar) -> EConstr.mkVar id | _ -> raise Exit) sols)
   with Exit ->
     NoUpdate
 
@@ -929,12 +952,12 @@ let filter_effective_candidates evd evi filter candidates =
   | None -> candidates
   | Some filter ->
       let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
-      List.filter (fun a -> Id.Set.subset (collect_vars evd (EConstr.of_constr a)) ids) candidates
+      List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates
 
 let filter_candidates evd evk filter candidates_update =
   let evi = Evd.find_undefined evd evk in
   let candidates = match candidates_update with
-  | NoUpdate -> evi.evar_candidates
+  | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
   | UpdateWith c -> Some c
   in
   match candidates with
@@ -982,17 +1005,18 @@ let restrict_hyps evd evk filter candidates =
     let typablefilter = closure_of_filter evd evk (Some filter) in
     (typablefilter,candidates)
 
-exception EvarSolvedWhileRestricting of evar_map * constr
+exception EvarSolvedWhileRestricting of evar_map * EConstr.constr
 
 let do_restrict_hyps evd (evk,args as ev) filter candidates =
+  let open EConstr in
   let filter,candidates = match filter with
   | None -> None,candidates
   | Some filter -> restrict_hyps evd evk filter candidates in
   match candidates,filter with
   | UpdateWith [], _ -> error "Not solvable."
   | UpdateWith [nc],_ ->
-      let evd = Evd.define evk nc evd in
-      raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev)))
+      let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in
+      raise (EvarSolvedWhileRestricting (evd,mkEvar ev))
   | NoUpdate, None -> evd,ev
   | _ -> restrict_applied_evar evd ev filter candidates
 
@@ -1000,6 +1024,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
 (* ?e is assumed to have no candidates *)
 
 let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
+  let open EConstr in
   let rhs = expand_vars_in_term env evd rhs in
   let filter =
     restrict_upon_filter evd evk
@@ -1010,8 +1035,8 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
       (* that says that the body is hidden. Note that expand_vars_in_term *)
       (* expands only rels and vars aliases, not rels or vars bound to an *)
       (* arbitrary complex term *)
-      (fun a -> not (isRel a || isVar a)
-                || dependent evd (EConstr.of_constr a) (EConstr.of_constr rhs) || List.exists (fun (id,_) -> isVarId id a) sols)
+      (fun a -> not (isRel evd a || isVar evd a)
+                || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols)
       argsv in
   let filter = closure_of_filter evd evk filter in
   let candidates = extract_candidates sols in
@@ -1042,6 +1067,9 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
  * Note: argument f is the function used to instantiate evars.
  *)
 
+let instantiate_evar_array evi c args =
+  EConstr.of_constr (instantiate_evar_array evi (EConstr.Unsafe.to_constr c) (Array.map EConstr.Unsafe.to_constr args))
+
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
   match conv_algo env evd Reduction.CONV rhs c' with
@@ -1061,6 +1089,8 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
   | _, None -> filter_candidates evd evk1 filter1 NoUpdate
   | None, Some _ -> raise DoesNotPreserveCandidateRestriction
   | Some l1, Some l2 ->
+      let l1 = List.map EConstr.of_constr l1 in
+      let l2 = List.map EConstr.of_constr l2 in
       let l1 = filter_effective_candidates evd evi1 filter1 l1 in
       let l1' = List.filter (fun c1 ->
         let c1' = instantiate_evar_array evi1 c1 argsv1 in
@@ -1075,7 +1105,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
       if Int.equal (List.length l1) (List.length l1') then NoUpdate
       else UpdateWith l1'
 
-exception CannotProject of evar_map * existential
+exception CannotProject of evar_map * EConstr.existential
 
 (* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
    Can ?n be instantiated by a term u depending essentially on xi such that the
@@ -1092,15 +1122,15 @@ exception CannotProject of evar_map * existential
 *)
 
 let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args = decompose_app_vect evd (EConstr.of_constr t) in
-  match kind_of_term f with
+  let f,args = decompose_app_vect evd t in
+  match EConstr.kind evd (EConstr.of_constr f) with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false evd k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
+      Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) args
   | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
   | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
@@ -1109,30 +1139,31 @@ let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
   | _ -> (* We don't try to be more clever *) true
 
 let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
-  let t' = expansion_of_var aliases t in
+  let t' = expansion_of_var evd aliases t in
   if t' != t then
     (* t is a local definition, we keep it only if appears in the list *)
     (* of let-in variables effectively occurring on the right-hand side, *)
     (* which is the only reason to keep it when inverting arguments *)
-    match kind_of_term t with
+    match EConstr.kind evd t with
     | Var id -> Id.Set.mem id let_ids
     | Rel n -> Int.Set.mem n let_rels
     | _ -> assert false
   else
     (* t is an instance for a proper variable; we filter it along *)
     (* the free variables allowed to occur *)
-    match kind_of_term t with
+    match EConstr.kind evd t with
     | Var id -> Id.Set.mem id fv_ids
     | Rel n -> n <= k || Int.Set.mem n fv_rels
     | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
 
-exception EvarSolvedOnTheFly of evar_map * constr
+exception EvarSolvedOnTheFly of evar_map * EConstr.constr
 
 (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
    the common domain of definition *)
 let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+  let open EConstr in
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
-  let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
+  let fvs2 = free_vars_and_rels_up_alias_expansion evd aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
     (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
     argsv1 in
@@ -1161,12 +1192,12 @@ let check_evar_instance evd evk1 body conv_algo =
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
-    try Retyping.get_type_of ~lax:true evenv evd (EConstr.of_constr body)
+    try EConstr.of_constr (Retyping.get_type_of ~lax:true evenv evd body)
     with Retyping.RetypeError _ -> error "Ill-typed evar instance"
   in
-  match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
+  match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
   | Success evd -> evd
-  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
+  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,EConstr.of_constr evi.evar_concl))
 
 let update_evar_source ev1 ev2 evd =
   let loc, evs2 = evar_source ev2 evd in
@@ -1178,9 +1209,10 @@ let update_evar_source ev1 ev2 evd =
   
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
+    let open EConstr in
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
-    let evd' = Evd.define evk2 body evd in
-    let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in
+    let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in
+    let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
@@ -1197,7 +1229,8 @@ let preferred_orientation evd evk1 evk2 =
   | _ -> true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
-  let aliases = make_alias_map env in
+  let open EConstr in
+  let aliases = make_alias_map env evd in
   if preferred_orientation evd evk1 evk2 then
     try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
@@ -1244,10 +1277,10 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
   solve_evar_evar_aux force f g env evd pbty ev1 ev2
 
 type conv_fun =
-  env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
+  env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result
 
 type conv_fun_bool =
-  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+  env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool
 
 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
  * definitions. We try to unify the ti with the ui pairwise. The pairs
@@ -1255,8 +1288,9 @@ type conv_fun_bool =
  * depend on these args). *)
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
+  let open EConstr in
   let evdref = ref evd in
-  if Array.equal (e_eq_constr_univs evdref) argsv1 argsv2 then !evdref else
+  if Array.equal (fun c1 c2 -> e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) ) argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
@@ -1288,14 +1322,14 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
   | Some l ->
       let l' =
         List.map_filter
-          (filter_compatible_candidates conv_algo env evd evi argsv rhs) l in
+          (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs (EConstr.of_constr c)) l in
       match l' with
       | [] -> raise IncompatibleCandidates
       | [c,evd] ->
           (* solve_candidates might have been called recursively in the mean *)
           (* time and the evar been solved by the filtering process *)
          if Evd.is_undefined evd evk then
-	   let evd' = Evd.define evk c evd in
+	   let evd' = Evd.define evk (EConstr.Unsafe.to_constr c) evd in
 	     check_evar_instance evd' evk c conv_algo
 	 else evd
       | l when List.length l < List.length l' ->
@@ -1304,7 +1338,9 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
       | l -> evd
 
 let occur_evar_upto_types sigma n c =
+  let c = EConstr.Unsafe.to_constr c in
   let seen = ref Evar.Set.empty in
+  (** FIXME: Is that supposed to be evar-insensitive? *)
   let rec occur_rec c = match kind_of_term c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | Evar (sp,args as e) ->
@@ -1341,14 +1377,15 @@ let occur_evar_upto_types sigma n c =
  *                Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
  *)
 
-exception NotInvertibleUsingOurAlgorithm of constr
+exception NotInvertibleUsingOurAlgorithm of EConstr.constr
 exception NotEnoughInformationToProgress of (Id.t * evar_projection) list
-exception NotEnoughInformationEvarEvar of constr
-exception OccurCheckIn of evar_map * constr
+exception NotEnoughInformationEvarEvar of EConstr.constr
+exception OccurCheckIn of evar_map * EConstr.constr
 exception MetaOccurInBodyInternal
 
 let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
-  let aliases = make_alias_map env in
+  let open EConstr in
+  let aliases = make_alias_map env evd in
   let evdref = ref evd in
   let progress = ref false in
   let evi = Evd.find evd evk in
@@ -1365,7 +1402,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | (id,p)::_::_ ->
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
-      let ty = lazy (Retyping.get_type_of env !evdref (EConstr.of_constr t)) in
+      let ty = lazy (EConstr.of_constr (Retyping.get_type_of env !evdref t)) in
       let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
       evdref := evd;
       c
@@ -1377,18 +1414,18 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
           let ty = find_solution_type (evar_filtered_env evi) sols in
-          let ty' = instantiate_evar_array evi ty argsv in
+          let ty' = instantiate_evar_array evi (EConstr.of_constr ty) argsv in
           let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in
-          let ts = expansions_of_var aliases t in
-          let test c = isEvar c || List.mem_f Constr.equal c ts in
+          let ts = expansions_of_var evd aliases t in
+          let test c = isEvar evd c || List.mem_f (EConstr.eq_constr evd) c ts in
           let filter = restrict_upon_filter evd evk test argsv' in
           let filter = closure_of_filter evd evk' filter in
           let candidates = extract_candidates sols in
           let evd = match candidates with
           | NoUpdate ->
             let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in
-            Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd
+            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t) evd
           | UpdateWith _ ->
             restrict_evar evd evk' filter candidates
           in
@@ -1396,29 +1433,28 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           evar in
 
   let rec imitate (env',k as envk) t =
-    let t = whd_evar !evdref t in
-    match kind_of_term t with
+    match EConstr.kind !evdref t with
     | Rel i when i>k ->
         let open Context.Rel.Declaration in
         (match Environ.lookup_rel (i-k) env' with
         | LocalAssum _ -> project_variable (mkRel (i-k))
         | LocalDef (_,b,_) ->
           try project_variable (mkRel (i-k))
-          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
+          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (Vars.lift i (EConstr.of_constr b)))
     | Var id ->
         (match Environ.lookup_named id env' with
         | LocalAssum _ -> project_variable t
         | LocalDef (_,b,_) ->
           try project_variable t
-          with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
+          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b))
     | LetIn (na,b,u,c) ->
-        imitate envk (subst1 b c)
+        imitate envk (Vars.subst1 b c)
     | Evar (evk',args' as ev') ->
         if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs));
         (* Evar/Evar problem (but left evar is virtual) *)
         let aliases = lift_aliases k aliases in
         (try
-          let ev = (evk,Array.map (lift k) argsv) in
+          let ev = (evk,Array.map (Vars.lift k) argsv) in
           let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
@@ -1428,7 +1464,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           if not !progress then
             raise (NotEnoughInformationEvarEvar t);
           (* Make the virtual left evar real *)
-          let ty = get_type_of env' evd (EConstr.of_constr t) in
+          let ty = EConstr.of_constr (get_type_of env' evd t) in
           let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
@@ -1437,7 +1473,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
              (* Try to project (a restriction of) the left evar ... *)
             try
               let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
-              let evd = Evd.define evk' body evd in
+              let evd = Evd.define evk' (EConstr.Unsafe.to_constr body) evd in
 		check_evar_instance evd evk' body conv_algo
             with
             | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
@@ -1449,9 +1485,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     | _ ->
         progress := true;
         match
-          let c,args = decompose_app_vect !evdref (EConstr.of_constr t) in
-          match kind_of_term c with
-          | Construct (cstr,u) when noccur_between 1 k t ->
+          let c,args = decompose_app_vect !evdref t in
+          match EConstr.kind !evdref (EConstr.of_constr c) with
+          | Construct (cstr,u) when Vars.noccur_between !evdref 1 k t ->
             (* This is common case when inferring the return clause of match *)
             (* (currently rudimentary: we do not treat the case of multiple *)
             (*  possible inversions; we do not treat overlap with a possible *)
@@ -1462,14 +1498,13 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           | _ -> None
         with
         | Some l ->
-            let ty = get_type_of env' !evdref (EConstr.of_constr t) in
+            let ty = EConstr.of_constr (get_type_of env' !evdref t) in
             let candidates =
               try
-                let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
                 let t =
                   map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
-                    self envk (EConstr.of_constr t) in
-                EConstr.Unsafe.to_constr t::l
+                    imitate envk t in
+                t::l
               with e when CErrors.noncritical e -> l in
             (match candidates with
             | [x] -> x
@@ -1480,11 +1515,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
               evar'')
         | None ->
            (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-          let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
-          EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
-					self envk (EConstr.of_constr t))
+          map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+					imitate envk t
   in
-  let rhs = whd_beta evd (EConstr.of_constr rhs) (* heuristic *) in
+  let rhs = EConstr.of_constr (whd_beta evd rhs) (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
     let names = ref Idset.empty in
@@ -1493,16 +1527,16 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
       | (decl :: ctxt'), (c :: s') ->
         let id = get_id decl in
         names := Idset.add id !names;
-        isVarId id c && is_id_subst ctxt' s'
+        isVarId evd id c && is_id_subst ctxt' s'
       | [], [] -> true
       | _ -> false 
     in
       is_id_subst filter_ctxt (Array.to_list argsv) &&
-      closed0 rhs &&
-      Idset.subset (collect_vars evd (EConstr.of_constr rhs)) !names 
+      Vars.closed0 evd rhs &&
+      Idset.subset (collect_vars evd rhs) !names 
   in
   let body =
-    if fast rhs then nf_evar evd rhs
+    if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
     else
       let t' = imitate (env,0) rhs in
 	if !progress then
@@ -1518,7 +1552,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
  *)
 
 and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
-  match kind_of_term rhs with
+  match EConstr.kind evd rhs with
   | Evar (evk2,argsv2 as ev2) ->
       if Evar.equal evk evk2 then
         solve_refl ~can_drop:choose
@@ -1531,7 +1565,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
   with NoCandidates ->
   try
     let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in
-    if occur_meta evd' (EConstr.of_constr body) then raise MetaOccurInBodyInternal;
+    if occur_meta evd' body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
     if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
@@ -1553,23 +1587,23 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
-    let evd' = check_evar_instance evd' evk body conv_algo in
+    let evd' = check_evar_instance evd' evk (EConstr.of_constr body) conv_algo in
     Evd.define evk body evd'
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd pbty ev sols rhs
     | NotEnoughInformationEvarEvar t ->
-        add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
+        add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,t) evd
     | MorePreciseOccurCheckNeeeded ->
-        add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
+        add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,rhs) evd
     | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
         raise e
     | OccurCheckIn (evd,rhs) ->
         (* last chance: rhs actually reduces to ev *)
-        let c = whd_all env evd (EConstr.of_constr rhs) in
-        match kind_of_term c with
+        let c = EConstr.of_constr (whd_all env evd rhs) in
+        match EConstr.kind evd c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
-	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma (EConstr.of_constr c) (EConstr.of_constr c'))
+	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
               env evd pbty evk argsv argsv2
         | _ ->
 	    raise (OccurCheckIn (evd,rhs))
@@ -1610,7 +1644,7 @@ let reconsider_conv_pbs conv_algo evd =
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
        | Success evd ->
-           (match conv_algo env evd pbty t1 t2 with
+           (match conv_algo env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with
            | Success _ as x -> x
            | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
        | UnifFailure _ as x -> x)
@@ -1624,8 +1658,9 @@ let reconsider_conv_pbs conv_algo evd =
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
+  let open EConstr in
   try
-    let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
+    let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
       reconsider_conv_pbs conv_algo evd
   with
@@ -1638,5 +1673,5 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
     | IllTypedInstance (env,t,u) ->
         UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))
     | IncompatibleCandidates ->
-        UnifFailure (evd,ConversionFailed (env,mkEvar ev1, EConstr.Unsafe.to_constr t2))
+        UnifFailure (evd,ConversionFailed (env,mkEvar ev1,t2))
 
-- 
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/evarsolve.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8a22aed2f2..3bcea4cee5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -606,7 +606,7 @@ let make_projectable_subst aliases sigma evi args =
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
   let open EConstr in
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in
   let evd = Sigma.to_evar_map evd in
   let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
   let evar_in_env = EConstr.of_constr evar_in_env in
@@ -682,6 +682,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd = Sigma.Unsafe.of_evar_map evd in
+  let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in
   let Sigma (ev2_in_sign, evd, _) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src (List.map EConstr.Unsafe.to_constr inst2_in_sign) in
   let evd = Sigma.to_evar_map evd in
-- 
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/evarsolve.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3bcea4cee5..b1fc7cbe9a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -147,17 +147,17 @@ let recheck_applications conv_algo env evdref t =
     | App (f, args) ->
        let () = aux env f in
        let fty = Retyping.get_type_of env !evdref f in
-       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
+       let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
 	 match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with
 	 | Prod (na, dom, codom) ->
-	    (match conv_algo env !evdref Reduction.CUMUL (EConstr.of_constr argsty.(i)) dom with
+	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
 			     aux (succ i) (Vars.subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
-		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), EConstr.Unsafe.to_constr dom))
-	 | _ -> raise (IllTypedInstance (env, ty, EConstr.of_constr argsty.(i)))
+		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
+	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
        else ()
      in aux 0 (EConstr.of_constr fty)
     | _ ->
-- 
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/evarsolve.ml | 79 ++++++++++++++++++--------------------------------
 1 file changed, 28 insertions(+), 51 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b1fc7cbe9a..b7db51d5c5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,14 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
 open Util
 open CErrors
 open Names
 open Term
-open Vars
 open Environ
 open Termops
 open Evd
+open EConstr
+open Vars
 open Namegen
 open Retyping
 open Reductionops
@@ -22,7 +24,6 @@ open Pretype_errors
 open Sigma.Notations
 
 let normalize_evar evd ev =
-  let open EConstr in
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
   | _ -> assert false
@@ -50,7 +51,6 @@ let refresh_level evd s =
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
-  let open EConstr in
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
@@ -141,7 +141,6 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
 exception IllTypedInstance of env * EConstr.types * EConstr.types
 
 let recheck_applications conv_algo env evdref t =
-  let open EConstr in
   let rec aux env t =
     match EConstr.kind !evdref t with
     | App (f, args) ->
@@ -154,7 +153,7 @@ let recheck_applications conv_algo env evdref t =
 	 | Prod (na, dom, codom) ->
 	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
-			     aux (succ i) (Vars.subst1 args.(i) codom)
+			     aux (succ i) (subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
 		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
 	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
@@ -221,7 +220,6 @@ let restrict_instance evd evk filter argsv =
 
 open Context.Rel.Declaration
 let noccur_evar env evd evk c =
-  let open EConstr in
   let cache = ref Int.Set.empty (* cache for let-ins *) in
   let rec occur_rec check_types (k, env as acc) c =
   match EConstr.kind evd c with
@@ -234,10 +232,10 @@ let noccur_evar env evd evk c =
      if not (Int.Set.mem (i-k) !cache) then
        let decl = Environ.lookup_rel i env in
        if check_types then
-         (cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr (get_type decl))));
+         (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr (get_type decl))));
        (match decl with
         | LocalAssum _ -> ()
-        | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr b)))
+        | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr b)))
   | Proj (p,c) -> occur_rec true acc c
   | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env))
     (occur_rec check_types) acc c
@@ -270,7 +268,6 @@ let compute_var_aliases sign sigma =
     sign Id.Map.empty
 
 let compute_rel_aliases var_aliases rels sigma =
-  let open EConstr in
   snd (List.fold_right
 	 (fun decl (n,aliases) ->
 	  (n-1,
@@ -288,7 +285,7 @@ let compute_rel_aliases var_aliases rels sigma =
 		    try Int.Map.find (p+n) aliases with Not_found -> [] in
 		  Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
 	       | _ ->
-		  Int.Map.add n [Vars.lift n (mkCast(t,DEFAULTcast,u))] aliases)
+		  Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
 	   | LocalAssum _ -> aliases)
 	 )
 	 rels
@@ -301,10 +298,9 @@ let make_alias_map env sigma =
   (var_aliases,rel_aliases)
 
 let lift_aliases n (var_aliases,rel_aliases as aliases) =
-  let open EConstr in
   if Int.equal n 0 then aliases else
   (var_aliases,
-   Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (Vars.lift n) l))
+   Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
      rel_aliases Int.Map.empty)
 
 let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with
@@ -313,7 +309,6 @@ let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with
   | _ -> []
 
 let normalize_alias_opt sigma aliases x =
-  let open EConstr in
   match get_alias_chain_of sigma aliases x with
   | []  -> None
   | a::_ when isRel sigma a || isVar sigma a -> Some a
@@ -326,13 +321,11 @@ let normalize_alias sigma aliases x =
   | None -> x
 
 let normalize_alias_var sigma var_aliases id =
-  let open EConstr in
   destVar sigma (normalize_alias sigma (var_aliases,Int.Map.empty) (mkVar id))
 
 let extend_alias sigma decl (var_aliases,rel_aliases) =
-  let open EConstr in
   let rel_aliases =
-    Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (Vars.lift 1) l))
+    Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
       rel_aliases Int.Map.empty in
   let rel_aliases =
     match decl with
@@ -348,7 +341,7 @@ let extend_alias sigma decl (var_aliases,rel_aliases) =
               try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
             Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
         | _ ->
-            Int.Map.add 1 [Vars.lift 1 t] rel_aliases)
+            Int.Map.add 1 [lift 1 t] rel_aliases)
     | LocalAssum _ -> rel_aliases in
   (var_aliases, rel_aliases)
 
@@ -358,7 +351,6 @@ let expand_alias_once sigma aliases x =
   | l -> Some (List.last l)
 
 let expansions_of_var sigma aliases x =
-  let open EConstr in
   match get_alias_chain_of sigma aliases x with
   | [] -> [x]
   | a::_ as l when isRel sigma a || isVar sigma a -> x :: List.rev l
@@ -379,7 +371,6 @@ let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t w
 let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
 
 let free_vars_and_rels_up_alias_expansion sigma aliases c =
-  let open EConstr in
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
   let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
@@ -430,7 +421,7 @@ let rec expand_and_check_vars sigma aliases = function
       raise Exit
 
 module Constrhash = Hashtbl.Make
-  (struct type t = constr
+  (struct type t = Constr.constr
           let equal = Term.eq_constr
           let hash = hash_constr
    end)
@@ -476,7 +467,6 @@ let remove_instance_local_defs evd evk args =
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
 let find_unification_pattern_args env evd l t =
-  let open EConstr in
   if List.for_all (fun x -> isRel evd x || isVar evd x) l (* common failure case *) then
     let aliases = make_alias_map env evd in
     match (try Some (expand_and_check_vars evd aliases l) with Exit -> None) with
@@ -488,7 +478,6 @@ let find_unification_pattern_args env evd l t =
 let is_unification_pattern_meta env evd nb m l t =
   (* Variables from context and rels > nb are implicitly all there *)
   (* so we need to be a rel <= nb *)
-  let open EConstr in
   if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then
     match find_unification_pattern_args env evd l t with
     | Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x
@@ -497,7 +486,6 @@ let is_unification_pattern_meta env evd nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  let open EConstr in
   if List.for_all (fun x -> isRel evd x || isVar evd x) l 
     && noccur_evar env evd evk t
   then
@@ -528,14 +516,13 @@ let is_unification_pattern (env,nb) evd f l t =
    dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
 let solve_pattern_eqn env sigma l c =
-  let open EConstr in
   let c' = List.fold_right (fun a c ->
-    let c' = subst_term sigma (Vars.lift 1 a) (Vars.lift 1 c) in
+    let c' = subst_term sigma (lift 1 a) (lift 1 c) in
     match EConstr.kind sigma a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let open Context.Rel.Declaration in
-          let d = map_constr (lift n) (lookup_rel n env) in
+          let d = map_constr (CVars.lift n) (lookup_rel n env) in
           let c' = EConstr.of_constr c' in
           mkLambda_or_LetIn d c'
       | Var id ->
@@ -604,7 +591,6 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
-  let open EConstr in
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in
   let evd = Sigma.to_evar_map evd in
@@ -637,7 +623,6 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
 exception MorePreciseOccurCheckNeeeded
 
 let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
-  let open EConstr in
   if Evd.is_defined evd evk1 then
       (* Some circularity somewhere (see e.g. #3209) *)
       raise MorePreciseOccurCheckNeeeded;
@@ -669,8 +654,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
             t_in_sign sign filter inst_in_env in
           evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
       (push_named_context_val d' sign, Filter.extend 1 filter,
-       (mkRel 1)::(List.map (Vars.lift 1) inst_in_env),
-       (mkRel 1)::(List.map (Vars.lift 1) inst_in_sign),
+       (mkRel 1)::(List.map (lift 1) inst_in_env),
+       (mkRel 1)::(List.map (lift 1) inst_in_sign),
        push_rel d env,evd,id::avoid))
       rel_sign
       (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
@@ -707,7 +692,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
       List.filter (fun (args',id) ->
         (* is_conv is maybe too strong (and source of useless computation) *)
         (* (at least expansion of aliases is needed) *)
-        Array.for_all2 (fun c1 c2 -> is_conv env evd (EConstr.of_constr c1) (EConstr.of_constr c2)) args args') l in
+        Array.for_all2 (fun c1 c2 -> is_conv env evd c1 (EConstr.of_constr c2)) args args') l in
     List.map snd l
   with Not_found ->
     []
@@ -765,7 +750,6 @@ let rec assoc_up_to_alias sigma aliases y yc = function
           | _ -> if EConstr.eq_constr sigma yc c then id else raise Not_found
 
 let rec find_projectable_vars with_evars aliases sigma y subst =
-  let open EConstr in
   let yc = normalize_alias sigma aliases y in
   let is_projectable idc idcl subst' =
     (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
@@ -829,7 +813,6 @@ let rec find_solution_type evarenv = function
 let rec do_projection_effects define_fun env ty evd = function
   | ProjectVar -> evd
   | ProjectEvar ((evk,argsv),evi,id,p) ->
-      let open EConstr in
       let evd = Evd.define evk (Constr.mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
@@ -840,7 +823,7 @@ let rec do_projection_effects define_fun env ty evd = function
            one (however, regarding coercions, because t is obtained by
            unif, we know that no coercion can be inserted) *)
         let subst = make_pure_subst evi argsv in
-        let ty' = Vars.replace_vars subst (EConstr.of_constr evi.evar_concl) in
+        let ty' = replace_vars subst (EConstr.of_constr evi.evar_concl) in
         if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd
       else
         evd
@@ -875,14 +858,13 @@ type projectibility_status =
 
 let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
   let effects = ref [] in
-  let open EConstr in
   let rec aux k t =
     match EConstr.kind evd t with
     | Rel i when i>k0+k -> aux' k (mkRel (i-k))
     | Var id -> aux' k t
     | _ -> map_with_binders evd succ aux k t
   and aux' k t =
-    try EConstr.of_constr (project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders)
+    try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
     with Not_found ->
       match expand_alias_once evd aliases t with
       | None -> raise Not_found
@@ -983,7 +965,8 @@ let closure_of_filter evd evk = function
                     | LocalAssum _ ->
                        false
                     | LocalDef (_,c,_) ->
-                       not (isRel c || isVar c)
+                      let c = EConstr.of_constr c in
+                       not (isRel evd c || isVar evd c)
   in
   let newfilter = Filter.map_along test filter (evar_context evi) in
   (* Now ensure that restriction is at least what is was originally *)
@@ -1009,7 +992,6 @@ let restrict_hyps evd evk filter candidates =
 exception EvarSolvedWhileRestricting of evar_map * EConstr.constr
 
 let do_restrict_hyps evd (evk,args as ev) filter candidates =
-  let open EConstr in
   let filter,candidates = match filter with
   | None -> None,candidates
   | Some filter -> restrict_hyps evd evk filter candidates in
@@ -1025,7 +1007,6 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
 (* ?e is assumed to have no candidates *)
 
 let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
-  let open EConstr in
   let rhs = expand_vars_in_term env evd rhs in
   let filter =
     restrict_upon_filter evd evk
@@ -1162,7 +1143,6 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr
 (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
    the common domain of definition *)
 let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
-  let open EConstr in
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion evd aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
@@ -1210,7 +1190,6 @@ let update_evar_source ev1 ev2 evd =
   
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
-    let open EConstr in
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in
     let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
@@ -1230,7 +1209,6 @@ let preferred_orientation evd evk1 evk2 =
   | _ -> true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
-  let open EConstr in
   let aliases = make_alias_map env evd in
   if preferred_orientation evd evk1 evk2 then
     try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
@@ -1248,6 +1226,7 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
   let evi = Evd.find evd evk1 in
+  let downcast evk t evd = downcast evk (EConstr.Unsafe.to_constr t) evd in
   let evd =
     try 
       (* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j.
@@ -1289,7 +1268,6 @@ type conv_fun_bool =
  * depend on these args). *)
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
-  let open EConstr in
   let evdref = ref evd in
   if Array.equal (fun c1 c2 -> e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) ) argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
@@ -1350,7 +1328,7 @@ let occur_evar_upto_types sigma n c =
        else (
          seen := Evar.Set.add sp !seen;
 	 Option.iter occur_rec (existential_opt_value sigma e);
-	 occur_rec (existential_type sigma e))
+	 occur_rec (Evd.existential_type sigma e))
     | _ -> Constr.iter occur_rec c
   in
   try occur_rec c; false with Occur -> true
@@ -1385,7 +1363,6 @@ exception OccurCheckIn of evar_map * EConstr.constr
 exception MetaOccurInBodyInternal
 
 let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
-  let open EConstr in
   let aliases = make_alias_map env evd in
   let evdref = ref evd in
   let progress = ref false in
@@ -1441,7 +1418,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | LocalAssum _ -> project_variable (mkRel (i-k))
         | LocalDef (_,b,_) ->
           try project_variable (mkRel (i-k))
-          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (Vars.lift i (EConstr.of_constr b)))
+          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i (EConstr.of_constr b)))
     | Var id ->
         (match Environ.lookup_named id env' with
         | LocalAssum _ -> project_variable t
@@ -1449,13 +1426,13 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           try project_variable t
           with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b))
     | LetIn (na,b,u,c) ->
-        imitate envk (Vars.subst1 b c)
+        imitate envk (subst1 b c)
     | Evar (evk',args' as ev') ->
         if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs));
         (* Evar/Evar problem (but left evar is virtual) *)
         let aliases = lift_aliases k aliases in
         (try
-          let ev = (evk,Array.map (Vars.lift k) argsv) in
+          let ev = (evk,Array.map (lift k) argsv) in
           let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
@@ -1487,8 +1464,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         progress := true;
         match
           let c,args = decompose_app_vect !evdref t in
+          let args = Array.map EConstr.of_constr args in
           match EConstr.kind !evdref (EConstr.of_constr c) with
-          | Construct (cstr,u) when Vars.noccur_between !evdref 1 k t ->
+          | Construct (cstr,u) when noccur_between !evdref 1 k t ->
             (* This is common case when inferring the return clause of match *)
             (* (currently rudimentary: we do not treat the case of multiple *)
             (*  possible inversions; we do not treat overlap with a possible *)
@@ -1533,7 +1511,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
       | _ -> false 
     in
       is_id_subst filter_ctxt (Array.to_list argsv) &&
-      Vars.closed0 evd rhs &&
+      closed0 evd rhs &&
       Idset.subset (collect_vars evd rhs) !names 
   in
   let body =
@@ -1659,7 +1637,6 @@ let reconsider_conv_pbs conv_algo evd =
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
-  let open EConstr in
   try
     let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
-- 
cgit v1.2.3


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

---
 pretyping/evarsolve.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b7db51d5c5..4ce8a44adc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -518,15 +518,15 @@ let is_unification_pattern (env,nb) evd f l t =
 let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
     let c' = subst_term sigma (lift 1 a) (lift 1 c) in
+    let c' = EConstr.of_constr c' in
     match EConstr.kind sigma a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let open Context.Rel.Declaration in
           let d = map_constr (CVars.lift n) (lookup_rel n env) in
-          let c' = EConstr.of_constr c' in
           mkLambda_or_LetIn d c'
       | Var id ->
-          let d = lookup_named id env in EConstr.of_constr (mkNamedLambda_or_LetIn d c')
+          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
       | _ -> assert false)
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
@@ -592,10 +592,9 @@ let make_projectable_subst aliases sigma evi args =
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src inst_in_env in
   let evd = Sigma.to_evar_map evd in
   let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
-  let evar_in_env = EConstr.of_constr evar_in_env in
   let (evk, _) = destEvar evd evar_in_env in
   let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -669,10 +668,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in
   let Sigma (ev2_in_sign, evd, _) =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src (List.map EConstr.Unsafe.to_constr inst2_in_sign) in
+    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
   let evd = Sigma.to_evar_map evd in
-  let ev2_in_env = (fst (destEvar evd (EConstr.of_constr ev2_in_sign)), Array.of_list inst2_in_env) in
-  (evd, EConstr.of_constr ev2_in_sign, ev2_in_env)
+  let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in
+  (evd, ev2_in_sign, ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
   let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
-- 
cgit v1.2.3


From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 02:45:54 +0100
Subject: Hints API using EConstr.

---
 pretyping/evarsolve.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4ce8a44adc..7725719261 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1612,12 +1612,14 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
  * ass.
  *)
 
-let status_changed lev (pbty,_,t1,t2) =
-  (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
-  (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
+let status_changed evd lev (pbty,_,t1,t2) =
+  let t1 = EConstr.of_constr t1 in
+  let t2 = EConstr.of_constr t2 in
+  (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) ||
+  (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false)
 
 let reconsider_conv_pbs conv_algo evd =
-  let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
+  let (evd,pbs) = extract_changed_conv_pbs evd (status_changed evd) in
   List.fold_left
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
-- 
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/evarsolve.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 7725719261..65b6d287d5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -518,7 +518,6 @@ let is_unification_pattern (env,nb) evd f l t =
 let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
     let c' = subst_term sigma (lift 1 a) (lift 1 c) in
-    let c' = EConstr.of_constr c' in
     match EConstr.kind sigma a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
@@ -557,7 +556,7 @@ let make_projectable_subst aliases sigma evi args =
         | LocalAssum (id,c), a::rest ->
             let cstrs =
               let a',args = decompose_app_vect sigma a in
-              match EConstr.kind sigma (EConstr.of_constr a') with
+              match EConstr.kind sigma a' with
               | Construct cstr ->
                   let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
                   Constrmap.add (fst cstr) ((args,id)::l) cstrs
@@ -691,7 +690,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
       List.filter (fun (args',id) ->
         (* is_conv is maybe too strong (and source of useless computation) *)
         (* (at least expansion of aliases is needed) *)
-        Array.for_all2 (fun c1 c2 -> is_conv env evd c1 (EConstr.of_constr c2)) args args') l in
+        Array.for_all2 (fun c1 c2 -> is_conv env evd c1 c2) args args') l in
     List.map snd l
   with Not_found ->
     []
@@ -1104,14 +1103,14 @@ exception CannotProject of evar_map * EConstr.existential
 
 let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect evd t in
-  match EConstr.kind evd (EConstr.of_constr f) with
+  match EConstr.kind evd f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) params
-  | Ind _ -> Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) args
+      Array.for_all (is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
   | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
   | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
@@ -1463,8 +1462,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         progress := true;
         match
           let c,args = decompose_app_vect !evdref t in
-          let args = Array.map EConstr.of_constr args in
-          match EConstr.kind !evdref (EConstr.of_constr c) with
+          match EConstr.kind !evdref c with
           | Construct (cstr,u) when noccur_between !evdref 1 k t ->
             (* This is common case when inferring the return clause of match *)
             (* (currently rudimentary: we do not treat the case of multiple *)
-- 
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/evarsolve.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 65b6d287d5..27436fdd8b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -149,7 +149,7 @@ let recheck_applications conv_algo env evdref t =
        let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
-	 match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with
+	 match EConstr.kind !evdref (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
 	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
@@ -814,7 +814,7 @@ let rec do_projection_effects define_fun env ty evd = function
       let evd = Evd.define evk (Constr.mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = EConstr.of_constr (whd_all env evd (Lazy.force ty)) in
+      let ty = whd_all env evd (Lazy.force ty) in
       if not (isSort evd ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -1494,7 +1494,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
 					imitate envk t
   in
-  let rhs = EConstr.of_constr (whd_beta evd rhs) (* heuristic *) in
+  let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
     let names = ref Idset.empty in
@@ -1576,7 +1576,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         raise e
     | OccurCheckIn (evd,rhs) ->
         (* last chance: rhs actually reduces to ev *)
-        let c = EConstr.of_constr (whd_all env evd rhs) in
+        let c = whd_all env evd rhs in
         match EConstr.kind evd c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
 	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
@@ -1637,7 +1637,7 @@ let reconsider_conv_pbs conv_algo evd =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *)
+    let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
       reconsider_conv_pbs conv_algo evd
   with
-- 
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/evarsolve.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 27436fdd8b..3003620d7e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -189,8 +189,8 @@ let restrict_evar_key evd evk filter candidates =
       | None -> evar_filter evi
       | Some filter -> filter in
       let candidates = match candidates with
-      | NoUpdate -> evi.evar_candidates
-      | UpdateWith c -> Some (List.map EConstr.Unsafe.to_constr c) in
+      | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
+      | UpdateWith c -> Some c in
       let sigma = Sigma.Unsafe.of_evar_map evd in
       let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
       (Sigma.to_evar_map sigma, evk)
-- 
cgit v1.2.3


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

---
 pretyping/evarsolve.ml | 59 ++++++++++++++++++++++++++++----------------------
 1 file changed, 33 insertions(+), 26 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3003620d7e..de2e46a781 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -23,6 +23,14 @@ open Evarutil
 open Pretype_errors
 open Sigma.Notations
 
+let nlocal_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  Context.Named.Declaration.LocalAssum (na, inj t)
+
+let nlocal_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  Context.Named.Declaration.LocalDef (na, inj b, inj t)
+
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -108,11 +116,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       | Some dir -> refresh status dir t)
     else (refresh_term_evars false true t; t)
   in
-    if !modified then !evdref, EConstr.Unsafe.to_constr t' else !evdref, EConstr.Unsafe.to_constr t
+    if !modified then !evdref, t' else !evdref, t
 
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
-    refresh_universes (Some false) env sigma (EConstr.of_constr ty)
+    refresh_universes (Some false) env sigma ty
 		      
 
 (************************)
@@ -146,7 +154,7 @@ let recheck_applications conv_algo env evdref t =
     | App (f, args) ->
        let () = aux env f in
        let fty = Retyping.get_type_of env !evdref f in
-       let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in
+       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
 	 match EConstr.kind !evdref (whd_all env !evdref ty) with
@@ -158,7 +166,7 @@ let recheck_applications conv_algo env evdref t =
 		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
 	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
        else ()
-     in aux 0 (EConstr.of_constr fty)
+     in aux 0 fty
     | _ ->
        iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t
   in aux env t
@@ -173,7 +181,7 @@ type 'a update =
 | NoUpdate
 
 open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (get_id %> EConstr.mkVar) sign
+let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
 
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
@@ -413,9 +421,9 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 
 let rec expand_and_check_vars sigma aliases = function
   | [] -> []
-  | a::l when EConstr.isRel sigma a || EConstr.isVar sigma a ->
+  | a::l when isRel sigma a || isVar sigma a ->
       let a = expansion_of_var sigma aliases a in
-      if EConstr.isRel sigma a || EConstr.isVar sigma a then a :: expand_and_check_vars sigma aliases l
+      if isRel sigma a || isVar sigma a then a :: expand_and_check_vars sigma aliases l
       else raise Exit
   | _ ->
       raise Exit
@@ -480,7 +488,7 @@ let is_unification_pattern_meta env evd nb m l t =
   (* so we need to be a rel <= nb *)
   if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then
     match find_unification_pattern_args env evd l t with
-    | Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x
+    | Some _ as x when not (dependent evd (mkMeta m) t) -> x
     | _ -> None
   else
     None
@@ -591,15 +599,15 @@ let make_projectable_subst aliases sigma evi args =
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src inst_in_env in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
   let evd = Sigma.to_evar_map evd in
   let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
   let (evk, _) = destEvar evd evar_in_env in
-  let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in
+  let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
-  (evd,whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign))
+  (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign)))
 
 (* We have x1..xq |- ?e1 : τ and had to solve something like
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
@@ -624,7 +632,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   if Evd.is_defined evd evk1 then
       (* Some circularity somewhere (see e.g. #3209) *)
       raise MorePreciseOccurCheckNeeeded;
-  let (evk1,args1) = EConstr.destEvar evd (EConstr.mkEvar (evk1,args1)) in
+  let (evk1,args1) = destEvar evd (mkEvar (evk1,args1)) in
   let evi1 = Evd.find_undefined evd evk1 in
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
@@ -641,16 +649,16 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
         let t_in_env = EConstr.of_constr t_in_env in
         let s = Retyping.get_sort_of env evd t_in_env in
         let evd,ty_t_in_sign = refresh_universes
-	 ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in
+	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,d' = match d with
-      | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
+      | LocalAssum _ -> evd, nlocal_assum (id,t_in_sign)
       | LocalDef (_,b,_) ->
           let b = EConstr.of_constr b in
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
-          evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
+          evd, nlocal_def (id,b,t_in_sign) in
       (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
@@ -661,11 +669,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
     let evd,ty_t_in_sign = refresh_universes
-     ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in
+     ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in
   let Sigma (ev2_in_sign, evd, _) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
   let evd = Sigma.to_evar_map evd in
@@ -899,7 +906,7 @@ let extract_unique_projection = function
 let extract_candidates sols =
   try
     UpdateWith
-      (List.map (function (id,ProjectVar) -> EConstr.mkVar id | _ -> raise Exit) sols)
+      (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
   with Exit ->
     NoUpdate
 
@@ -1171,7 +1178,7 @@ let check_evar_instance evd evk1 body conv_algo =
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
-    try EConstr.of_constr (Retyping.get_type_of ~lax:true evenv evd body)
+    try Retyping.get_type_of ~lax:true evenv evd body
     with Retyping.RetypeError _ -> error "Ill-typed evar instance"
   in
   match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
@@ -1378,7 +1385,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | (id,p)::_::_ ->
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
-      let ty = lazy (EConstr.of_constr (Retyping.get_type_of env !evdref t)) in
+      let ty = lazy (Retyping.get_type_of env !evdref t) in
       let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
       evdref := evd;
       c
@@ -1440,7 +1447,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           if not !progress then
             raise (NotEnoughInformationEvarEvar t);
           (* Make the virtual left evar real *)
-          let ty = EConstr.of_constr (get_type_of env' evd t) in
+          let ty = get_type_of env' evd t in
           let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
@@ -1474,7 +1481,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           | _ -> None
         with
         | Some l ->
-            let ty = EConstr.of_constr (get_type_of env' !evdref t) in
+            let ty = get_type_of env' !evdref t in
             let candidates =
               try
                 let t =
@@ -1563,15 +1570,15 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
-    let evd' = check_evar_instance evd' evk (EConstr.of_constr body) conv_algo in
-    Evd.define evk body evd'
+    let evd' = check_evar_instance evd' evk body conv_algo in
+    Evd.define evk (EConstr.Unsafe.to_constr body) evd'
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd pbty ev sols rhs
     | NotEnoughInformationEvarEvar t ->
-        add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,t) evd
+        add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
     | MorePreciseOccurCheckNeeeded ->
-        add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,rhs) evd
+        add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
     | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
         raise e
     | OccurCheckIn (evd,rhs) ->
-- 
cgit v1.2.3


From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

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

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de2e46a781..3235c2505b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -601,13 +601,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
   let evd = Sigma.to_evar_map evd in
-  let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
+  let t_in_env = whd_evar evd t_in_env in
   let (evk, _) = destEvar evd evar_in_env in
   let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
-  (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign)))
+  (evd,whd_evar evd evar_in_sign)
 
 (* We have x1..xq |- ?e1 : τ and had to solve something like
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
-- 
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/evarsolve.ml | 27 ++++++++-------------------
 1 file changed, 8 insertions(+), 19 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3235c2505b..ff47365286 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -23,14 +23,6 @@ open Evarutil
 open Pretype_errors
 open Sigma.Notations
 
-let nlocal_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  Context.Named.Declaration.LocalAssum (na, inj t)
-
-let nlocal_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  Context.Named.Declaration.LocalDef (na, inj b, inj t)
-
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -264,7 +256,6 @@ let compute_var_aliases sign sigma =
     let id = get_id decl in
     match decl with
     | LocalDef (_,t,_) ->
-        let t = EConstr.of_constr t in
         (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_id =
@@ -281,8 +272,6 @@ let compute_rel_aliases var_aliases rels sigma =
 	  (n-1,
 	   match decl with
 	   | LocalDef (_,t,u) ->
-              let t = EConstr.of_constr t in
-              let u = EConstr.of_constr u in
 	      (match EConstr.kind sigma t with
 	       | Var id' ->
 		  let aliases_of_n =
@@ -338,7 +327,6 @@ let extend_alias sigma decl (var_aliases,rel_aliases) =
   let rel_aliases =
     match decl with
     | LocalDef(_,t,_) ->
-        let t = EConstr.of_constr t in
         (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_binder =
@@ -530,7 +518,7 @@ let solve_pattern_eqn env sigma l c =
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let open Context.Rel.Declaration in
-          let d = map_constr (CVars.lift n) (lookup_rel n env) in
+          let d = map_constr (lift n) (lookup_rel n env) in
           mkLambda_or_LetIn d c'
       | Var id ->
           let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
@@ -556,6 +544,7 @@ let solve_pattern_eqn env sigma l c =
 
 let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
+  let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in
   let evar_aliases = compute_var_aliases sign sigma in
   let (_,full_subst,cstr_subst) =
     List.fold_right
@@ -571,7 +560,7 @@ let make_projectable_subst aliases sigma evi args =
               | _ -> cstrs in
             (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)
         | LocalDef (id,c,_), a::rest ->
-            (match EConstr.kind sigma (EConstr.of_constr c) with
+            (match EConstr.kind sigma c with
             | Var id' ->
                 let idc = normalize_alias_var sigma evar_aliases id' in
                 let sub = try Id.Map.find idc all with Not_found -> [] in
@@ -646,19 +635,17 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in
       let id = next_name_away na avoid in
       let evd,t_in_sign =
-        let t_in_env = EConstr.of_constr t_in_env in
         let s = Retyping.get_sort_of env evd t_in_env in
         let evd,ty_t_in_sign = refresh_universes
 	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,d' = match d with
-      | LocalAssum _ -> evd, nlocal_assum (id,t_in_sign)
+      | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
       | LocalDef (_,b,_) ->
-          let b = EConstr.of_constr b in
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
-          evd, nlocal_def (id,b,t_in_sign) in
+          evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
       (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
@@ -1238,9 +1225,11 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
 	 The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *)
       let evienv = Evd.evar_env evi in
       let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in
+      let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in
       let evi2 = Evd.find evd evk2 in
       let evi2env = Evd.evar_env evi2 in
       let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in
+      let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in
       let ui, uj = univ_of_sort i, univ_of_sort j in
 	if i == j || Evd.check_eq evd ui uj
 	then (* Shortcut, i = j *) 
@@ -1397,7 +1386,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
           let ty = find_solution_type (evar_filtered_env evi) sols in
-          let ty' = instantiate_evar_array evi (EConstr.of_constr ty) argsv in
+          let ty' = instantiate_evar_array evi ty argsv in
           let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in
           let ts = expansions_of_var evd aliases t in
-- 
cgit v1.2.3


From 390fd4ac0a969103caeb5db3e5138e26f9a533de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 17:49:11 +0100
Subject: Chasing a few unsafe constr coercions.

---
 pretyping/evarsolve.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ff47365286..28e63d04b9 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1263,7 +1263,13 @@ type conv_fun_bool =
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
   let evdref = ref evd in
-  if Array.equal (fun c1 c2 -> e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) ) argsv1 argsv2 then !evdref else
+  let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+  | None -> false
+  | Some cstr ->
+    try ignore (Evd.add_universe_constraints !evdref cstr); true
+    with UniversesDiffer -> false
+  in
+  if Array.equal eq_constr argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
-- 
cgit v1.2.3


From aaf75678a13d9c26341e762ab8e56b957cf4c771 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Dec 2016 01:30:45 +0100
Subject: Dedicated datatype for aliases in Evarsolve.

---
 pretyping/evarsolve.ml | 312 +++++++++++++++++++++++++++++--------------------
 1 file changed, 187 insertions(+), 125 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 28e63d04b9..398f2665e9 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -246,6 +246,47 @@ let noccur_evar env evd evk c =
 (* Managing chains of local definitons *)
 (***************************************)
 
+type alias =
+| RelAlias of int
+| VarAlias of Id.t
+
+let of_alias = function
+| RelAlias n -> mkRel n
+| VarAlias id -> mkVar id
+
+let to_alias sigma c = match EConstr.kind sigma c with
+| Rel n -> Some (RelAlias n)
+| Var id -> Some (VarAlias id)
+| _ -> None
+
+let is_alias sigma c alias = match EConstr.kind sigma c, alias with
+| Var id, VarAlias id' -> Id.equal id id'
+| Rel n, RelAlias n' -> Int.equal n n'
+| _ -> false
+
+let eq_alias a b = match a, b with
+| RelAlias n, RelAlias m -> Int.equal m n
+| VarAlias id1, VarAlias id2 -> Id.equal id1 id2
+| _ -> false
+
+type aliasing = EConstr.t option * alias list
+
+let empty_aliasing = None, []
+let make_aliasing c = Some c, []
+let push_alias (alias, l) a = (alias, a :: l)
+let lift_aliasing n (alias, l) =
+  let map a = match a with
+  | VarAlias _ -> a
+  | RelAlias m -> RelAlias (m + n)
+  in
+  (Option.map (fun c -> lift n c) alias, List.map map l)
+
+type aliases = {
+  rel_aliases : aliasing Int.Map.t;
+  var_aliases : aliasing Id.Map.t;
+  (** Only contains [VarAlias] *)
+}
+
 (* Expand rels and vars that are bound to other rels or vars so that
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
@@ -259,10 +300,10 @@ let compute_var_aliases sign sigma =
         (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_id =
-              try Id.Map.find id' aliases with Not_found -> [] in
-            Id.Map.add id (aliases_of_id@[t]) aliases
+              try Id.Map.find id' aliases with Not_found -> empty_aliasing in
+            Id.Map.add id (push_alias aliases_of_id (VarAlias id')) aliases
         | _ ->
-            Id.Map.add id [t] aliases)
+            Id.Map.add id (make_aliasing t) aliases)
     | LocalAssum _ -> aliases)
     sign Id.Map.empty
 
@@ -275,14 +316,14 @@ let compute_rel_aliases var_aliases rels sigma =
 	      (match EConstr.kind sigma t with
 	       | Var id' ->
 		  let aliases_of_n =
-		    try Id.Map.find id' var_aliases with Not_found -> [] in
-		  Int.Map.add n (aliases_of_n@[t]) aliases
+		    try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in
+		  Int.Map.add n (push_alias aliases_of_n (VarAlias id')) aliases
 	       | Rel p ->
 		  let aliases_of_n =
-		    try Int.Map.find (p+n) aliases with Not_found -> [] in
-		  Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
+		    try Int.Map.find (p+n) aliases with Not_found -> empty_aliasing in
+		  Int.Map.add n (push_alias aliases_of_n (RelAlias (p+n))) aliases
 	       | _ ->
-		  Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
+		  Int.Map.add n (make_aliasing (lift n (mkCast(t,DEFAULTcast,u)))) aliases)
 	   | LocalAssum _ -> aliases)
 	 )
 	 rels
@@ -292,37 +333,43 @@ let make_alias_map env sigma =
   (* We compute the chain of aliases for each var and rel *)
   let var_aliases = compute_var_aliases (named_context env) sigma in
   let rel_aliases = compute_rel_aliases var_aliases (rel_context env) sigma in
-  (var_aliases,rel_aliases)
+  { var_aliases; rel_aliases }
 
-let lift_aliases n (var_aliases,rel_aliases as aliases) =
+let lift_aliases n aliases =
   if Int.equal n 0 then aliases else
-  (var_aliases,
-   Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
-     rel_aliases Int.Map.empty)
+  let rel_aliases =
+   Int.Map.fold (fun p l -> Int.Map.add (p+n) (lift_aliasing n l))
+     aliases.rel_aliases Int.Map.empty
+  in
+  { aliases with rel_aliases }
 
-let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with
-  | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
-  | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> [])
-  | _ -> []
+let get_alias_chain_of sigma aliases x = match x with
+  | RelAlias n -> (try Int.Map.find n aliases.rel_aliases with Not_found -> empty_aliasing)
+  | VarAlias id -> (try Id.Map.find id aliases.var_aliases with Not_found -> empty_aliasing)
 
-let normalize_alias_opt sigma aliases x =
+let normalize_alias_opt_alias sigma aliases x =
   match get_alias_chain_of sigma aliases x with
-  | []  -> None
-  | a::_ when isRel sigma a || isVar sigma a -> Some a
-  | [_] -> None
-  | _::a::_ -> Some a
+  | _, []  -> None
+  | _, a :: _ -> Some a
+
+let normalize_alias_opt sigma aliases x = match to_alias sigma x with
+| None -> None
+| Some a -> normalize_alias_opt_alias sigma aliases a
 
 let normalize_alias sigma aliases x =
-  match normalize_alias_opt sigma aliases x with
+  match normalize_alias_opt_alias sigma aliases x with
   | Some a -> a
   | None -> x
 
 let normalize_alias_var sigma var_aliases id =
-  destVar sigma (normalize_alias sigma (var_aliases,Int.Map.empty) (mkVar id))
+  let aliases = { var_aliases; rel_aliases = Int.Map.empty } in
+  match normalize_alias sigma aliases (VarAlias id) with
+  | VarAlias id -> id
+  | RelAlias _ -> assert false (** var only aliases to variables *)
 
-let extend_alias sigma decl (var_aliases,rel_aliases) =
+let extend_alias sigma decl { var_aliases; rel_aliases } =
   let rel_aliases =
-    Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
+    Int.Map.fold (fun n l -> Int.Map.add (n+1) (lift_aliasing 1 l))
       rel_aliases Int.Map.empty in
   let rel_aliases =
     match decl with
@@ -330,36 +377,36 @@ let extend_alias sigma decl (var_aliases,rel_aliases) =
         (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_binder =
-              try Id.Map.find id' var_aliases with Not_found -> [] in
-            Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases
+              try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in
+            Int.Map.add 1 (push_alias aliases_of_binder (VarAlias id')) rel_aliases
         | Rel p ->
             let aliases_of_binder =
-              try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
-            Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
+              try Int.Map.find (p+1) rel_aliases with Not_found -> empty_aliasing in
+            Int.Map.add 1 (push_alias aliases_of_binder (RelAlias (p+1))) rel_aliases
         | _ ->
-            Int.Map.add 1 [lift 1 t] rel_aliases)
+            Int.Map.add 1 (make_aliasing (lift 1 t)) rel_aliases)
     | LocalAssum _ -> rel_aliases in
-  (var_aliases, rel_aliases)
+  { var_aliases; rel_aliases }
 
 let expand_alias_once sigma aliases x =
   match get_alias_chain_of sigma aliases x with
-  | []  -> None
-  | l -> Some (List.last l)
+  | None, []  -> None
+  | Some a, [] -> Some a
+  | _, l -> Some (of_alias (List.last l))
 
 let expansions_of_var sigma aliases x =
-  match get_alias_chain_of sigma aliases x with
-  | [] -> [x]
-  | a::_ as l when isRel sigma a || isVar sigma a -> x :: List.rev l
-  | _::l -> x :: List.rev l
+  let (_, l) = get_alias_chain_of sigma aliases x in
+  x :: List.rev l
 
 let expansion_of_var sigma aliases x =
   match get_alias_chain_of sigma aliases x with
-  | [] -> x
-  | a::_ -> a
+  | None, [] -> (false, of_alias x)
+  | Some a, _ -> (true, a)
+  | None, a :: _ -> (true, of_alias a)
 
 let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with
-  | Rel _ | Var _ ->
-      normalize_alias sigma aliases t
+  | Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n))
+  | Var id -> of_alias (normalize_alias sigma aliases (VarAlias id))
   | _ ->
     let self aliases c = expand_vars_in_term_using sigma aliases c in
     map_constr_with_full_binders sigma (extend_alias sigma) self aliases t
@@ -371,24 +418,28 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
   let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
   let is_in_cache depth = function
-    | Rel n -> Int.Set.mem (n-depth) !cache_rel
-    | Var s -> Id.Set.mem s !cache_var
-    | _ -> false in
+    | RelAlias n -> Int.Set.mem (n-depth) !cache_rel
+    | VarAlias s -> Id.Set.mem s !cache_var
+  in
   let put_in_cache depth = function
-    | Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel
-    | Var s -> cache_var := Id.Set.add s !cache_var
-    | _ -> () in
+    | RelAlias n -> cache_rel := Int.Set.add (n-depth) !cache_rel
+    | VarAlias s -> cache_var := Id.Set.add s !cache_var
+  in
   let rec frec (aliases,depth) c =
     match EConstr.kind sigma c with
     | Rel _ | Var _ as ck ->
+      let ck = match ck with
+      | Rel n -> RelAlias n
+      | Var id -> VarAlias id
+      | _ -> assert false
+      in
       if is_in_cache depth ck then () else begin
       put_in_cache depth ck;
-      let c' = expansion_of_var sigma aliases c in
-      (if c != c' then (* expansion, hence a let-in *) (** FIXME *)
-        match EConstr.kind sigma c with
-        | Var id -> acc4 := Id.Set.add id !acc4
-        | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
-        | _ -> ());
+      let expanded, c' = expansion_of_var sigma aliases ck in
+      (if expanded then (* expansion, hence a let-in *)
+        match ck with
+        | VarAlias id -> acc4 := Id.Set.add id !acc4
+        | RelAlias n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3);
       match EConstr.kind sigma c' with
         | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
@@ -407,30 +458,33 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 (* Managing pattern-unification *)
 (********************************)
 
-let rec expand_and_check_vars sigma aliases = function
+let map_all f l =
+  let rec map_aux f l = match l with
   | [] -> []
-  | a::l when isRel sigma a || isVar sigma a ->
-      let a = expansion_of_var sigma aliases a in
-      if isRel sigma a || isVar sigma a then a :: expand_and_check_vars sigma aliases l
-      else raise Exit
-  | _ ->
-      raise Exit
-
-module Constrhash = Hashtbl.Make
-  (struct type t = Constr.constr
-          let equal = Term.eq_constr
-          let hash = hash_constr
-   end)
-
-let constr_list_distinct sigma l =
-  let visited = Constrhash.create 23 in
-  let rec loop = function
-    | h::t ->
-        let h = EConstr.to_constr sigma h in
-        if Constrhash.mem visited h then false
-        else (Constrhash.add visited h h; loop t)
-    | [] -> true
-  in loop l
+  | x :: l ->
+    match f x with
+    | None -> raise Exit
+    | Some y -> y :: map_aux f l
+  in
+  try Some (map_aux f l) with Exit -> None
+
+let expand_and_check_vars sigma aliases l =
+  let map a = match get_alias_chain_of sigma aliases a with
+  | None, [] -> Some a
+  | None, a :: _ -> Some a
+  | Some _, _ -> None
+  in
+  map_all map l
+
+let alias_distinct l =
+  let rec check (rels, vars) = function
+  | [] -> true
+  | RelAlias n :: l ->
+    not (Int.Set.mem n rels) && check (Int.Set.add n rels, vars) l
+  | VarAlias id :: l ->
+    not (Id.Set.mem id vars) && check (rels, Id.Set.add id vars) l
+  in
+  check (Int.Set.empty, Id.Set.empty) l
 
 let get_actual_deps evd aliases l t =
   if occur_meta_or_existential evd t then
@@ -439,11 +493,10 @@ let get_actual_deps evd aliases l t =
   else
     (* Probably strong restrictions coming from t being evar-closed *)
     let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion evd aliases t in
-    List.filter (fun c ->
-      match EConstr.kind evd c with
-      | Var id -> Id.Set.mem id fv_ids
-      | Rel n -> Int.Set.mem n fv_rels
-      | _ -> assert false) l
+    List.filter (function
+      | VarAlias id -> Id.Set.mem id fv_ids
+      | RelAlias n -> Int.Set.mem n fv_rels
+    ) l
 
 open Context.Named.Declaration
 let remove_instance_local_defs evd evk args =
@@ -463,34 +516,41 @@ let remove_instance_local_defs evd evk args =
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
 let find_unification_pattern_args env evd l t =
-  if List.for_all (fun x -> isRel evd x || isVar evd x) l (* common failure case *) then
-    let aliases = make_alias_map env evd in
-    match (try Some (expand_and_check_vars evd aliases l) with Exit -> None) with
-    | Some l as x when constr_list_distinct evd (get_actual_deps evd aliases l t) -> x
-    | _ -> None
-  else
-    None
+  let aliases = make_alias_map env evd in
+  match expand_and_check_vars evd aliases l with
+  | Some l as x when alias_distinct (get_actual_deps evd aliases l t) -> x
+  | _ -> None
 
 let is_unification_pattern_meta env evd nb m l t =
   (* Variables from context and rels > nb are implicitly all there *)
   (* so we need to be a rel <= nb *)
-  if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then
-    match find_unification_pattern_args env evd l t with
+  let map a = match EConstr.kind evd a with
+  | Rel n -> if n <= nb then Some (RelAlias n) else None
+  | _ -> None
+  in
+  match map_all map l with
+  | Some l ->
+    begin match find_unification_pattern_args env evd l t with
     | Some _ as x when not (dependent evd (mkMeta m) t) -> x
     | _ -> None
-  else
+    end
+  | None ->
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel evd x || isVar evd x) l 
-    && noccur_evar env evd evk t
-  then
+  match map_all (fun c -> to_alias evd c) l with
+  | Some l when noccur_evar env evd evk t ->
     let args = remove_instance_local_defs evd evk args in
+    let args = map_all (fun c -> to_alias evd c) args in
+    begin match args with
+    | None -> None
+    | Some args ->
     let n = List.length args in
       match find_unification_pattern_args env evd (args @ l) t with
       | Some l -> Some (List.skipn n l)
       | _ -> None
-  else None
+    end
+  | _ -> None
 
 let is_unification_pattern_pure_evar env evd (evk,args) t =
   let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
@@ -513,16 +573,16 @@ let is_unification_pattern (env,nb) evd f l t =
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
 let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
-    let c' = subst_term sigma (lift 1 a) (lift 1 c) in
-    match EConstr.kind sigma a with
+    let c' = subst_term sigma (lift 1 (of_alias a)) (lift 1 c) in
+    match a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
-      | Rel n ->
+      | RelAlias n ->
           let open Context.Rel.Declaration in
           let d = map_constr (lift n) (lookup_rel n env) in
           mkLambda_or_LetIn d c'
-      | Var id ->
+      | VarAlias id ->
           let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
-      | _ -> assert false)
+    )
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
      is not in normal form *)
@@ -731,15 +791,15 @@ exception NotUniqueInType of (Id.t * evar_projection) list
 let rec assoc_up_to_alias sigma aliases y yc = function
   | [] -> raise Not_found
   | (c,cc,id)::l ->
-      if EConstr.eq_constr sigma y c then id
+      if is_alias sigma c y then id
       else
         match l with
         | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
         | [] ->
           (* Last chance, we reason up to alias conversion *)
           match (normalize_alias_opt sigma aliases c) with
-          | Some cc when EConstr.eq_constr sigma yc cc -> id
-          | _ -> if EConstr.eq_constr sigma yc c then id else raise Not_found
+          | Some cc when eq_alias yc cc -> id
+          | _ -> if is_alias sigma c yc then id else raise Not_found
 
 let rec find_projectable_vars with_evars aliases sigma y subst =
   let yc = normalize_alias sigma aliases y in
@@ -852,8 +912,8 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
   let effects = ref [] in
   let rec aux k t =
     match EConstr.kind evd t with
-    | Rel i when i>k0+k -> aux' k (mkRel (i-k))
-    | Var id -> aux' k t
+    | Rel i when i>k0+k -> aux' k (RelAlias (i-k))
+    | Var id -> aux' k (VarAlias id)
     | _ -> map_with_binders evd succ aux k t
   and aux' k t =
     try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
@@ -1113,22 +1173,24 @@ let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
   | _ -> (* We don't try to be more clever *) true
 
 let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
-  let t' = expansion_of_var evd aliases t in
-  if t' != t then
+  match to_alias evd t with
+  | Some t ->
+    let expanded, t' = expansion_of_var evd aliases t in
+    if expanded then
     (* t is a local definition, we keep it only if appears in the list *)
     (* of let-in variables effectively occurring on the right-hand side, *)
     (* which is the only reason to keep it when inverting arguments *)
-    match EConstr.kind evd t with
-    | Var id -> Id.Set.mem id let_ids
-    | Rel n -> Int.Set.mem n let_rels
-    | _ -> assert false
-  else
+      match t with
+      | VarAlias id -> Id.Set.mem id let_ids
+      | RelAlias n -> Int.Set.mem n let_rels
+    else begin match t with
+    | VarAlias id -> Id.Set.mem id fv_ids
+    | RelAlias n -> n <= k || Int.Set.mem n fv_rels
+    end
+  | None ->
     (* t is an instance for a proper variable; we filter it along *)
     (* the free variables allowed to occur *)
-    match EConstr.kind evd t with
-    | Var id -> Id.Set.mem id fv_ids
-    | Rel n -> n <= k || Int.Set.mem n fv_rels
-    | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
+    (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * EConstr.constr
 
@@ -1380,12 +1442,12 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | (id,p)::_::_ ->
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
-      let ty = lazy (Retyping.get_type_of env !evdref t) in
+      let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
       let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
       evdref := evd;
       c
     with
-      | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
+      | Not_found -> raise (NotInvertibleUsingOurAlgorithm (of_alias t))
       | NotUniqueInType sols ->
           if not !progress then
             raise (NotEnoughInformationToProgress sols);
@@ -1396,14 +1458,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in
           let ts = expansions_of_var evd aliases t in
-          let test c = isEvar evd c || List.mem_f (EConstr.eq_constr evd) c ts in
+          let test c = isEvar evd c || List.exists (is_alias evd c) ts in
           let filter = restrict_upon_filter evd evk test argsv' in
           let filter = closure_of_filter evd evk' filter in
           let candidates = extract_candidates sols in
           let evd = match candidates with
           | NoUpdate ->
             let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in
-            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t) evd
+            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',of_alias t) evd
           | UpdateWith _ ->
             restrict_evar evd evk' filter candidates
           in
@@ -1415,15 +1477,15 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     | Rel i when i>k ->
         let open Context.Rel.Declaration in
         (match Environ.lookup_rel (i-k) env' with
-        | LocalAssum _ -> project_variable (mkRel (i-k))
+        | LocalAssum _ -> project_variable (RelAlias (i-k))
         | LocalDef (_,b,_) ->
-          try project_variable (mkRel (i-k))
+          try project_variable (RelAlias (i-k))
           with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i (EConstr.of_constr b)))
     | Var id ->
         (match Environ.lookup_named id env' with
-        | LocalAssum _ -> project_variable t
+        | LocalAssum _ -> project_variable (VarAlias id)
         | LocalDef (_,b,_) ->
-          try project_variable t
+          try project_variable (VarAlias id)
           with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b))
     | LetIn (na,b,u,c) ->
         imitate envk (subst1 b c)
-- 
cgit v1.2.3


From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:20:25 +0200
Subject: Actually exporting delayed universes in the EConstr implementation.

For now we only normalize sorts, and we leave instances for the next
commit.
---
 pretyping/evarsolve.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4d78d2eb0f..77086d046c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -50,6 +50,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   let modified = ref false in
   (* direction: true for fresh universes lower than the existing ones *)
   let refresh_sort status ~direction s =
+    let s = ESorts.kind !evdref s in
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
       if direction then set_leq_sort env !evdref s' s
@@ -59,7 +60,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   in
   let rec refresh ~onlyalg status ~direction t =
     match EConstr.kind !evdref t with
-    | Sort (Type u as s) ->
+    | Sort s ->
+      begin match ESorts.kind !evdref s with
+      | Type u ->
        (match Univ.universe_level u with
 	| None -> refresh_sort status ~direction s
 	| Some l ->
@@ -71,10 +74,12 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       if onlyalg && alg then
 	         (evdref := Evd.make_flexible_variable !evdref false l; t)
 	       else t))
-    | Sort (Prop Pos as s) when refreshset && not direction ->
+      | Prop Pos when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
           only refreshing when we want higher universes. *)
        refresh_sort status ~direction s
+      | _ -> t
+      end
     | Prod (na,u,v) -> 
       mkProd (na, u, refresh ~onlyalg status ~direction v)
     | _ -> t
-- 
cgit v1.2.3