1 files changed, 134 insertions, 323 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bd47a04f1e..96f1ce5e60 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -13,132 +13,24 @@ open Util
 open Names
 open Constr
 open Context
-open Evd
-
-module API :
-sig
-module ESorts :
-sig
-type t
-val make : Sorts.t -> t
-val kind : Evd.evar_map -> t -> Sorts.t
-val unsafe_to_sorts : t -> Sorts.t
-end
-module EInstance :
-sig
-type t
-val make : Univ.Instance.t -> t
-val kind : Evd.evar_map -> t -> Univ.Instance.t
-val empty : t
-val is_empty : t -> bool
-val unsafe_to_instance : t -> Univ.Instance.t
-end
-type t
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
-val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
-val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
-val of_constr : Constr.t -> t
-val to_constr : evar_map -> t -> Constr.t
-val unsafe_to_constr : t -> Constr.t
-val unsafe_eq : (t, Constr.t) eq
-val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
-val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
-val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
-val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
-val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
-end =
-struct
 
-module ESorts =
-struct
-  type t = Sorts.t
-  let make s = s
-  let kind sigma = function
-  | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u)
-  | s -> s
-  let unsafe_to_sorts s = s
-end
+module ESorts = struct
+  include Evd.MiniEConstr.ESorts
 
-module EInstance =
-struct
-  type t = Univ.Instance.t
-  let make i = i
-  let kind sigma i =
-    if Univ.Instance.is_empty i then i
-    else Evd.normalize_universe_instance sigma i
-  let empty = Univ.Instance.empty
-  let is_empty = Univ.Instance.is_empty
-  let unsafe_to_instance t = t
+  let equal sigma s1 s2 =
+    Sorts.equal (kind sigma s1) (kind sigma s2)
 end
 
-type t = Constr.t
-
-let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
-  with NotInstantiatedEvar | Not_found -> None
-
-let rec whd_evar sigma c =
-  match Constr.kind c with
-  | Evar ev ->
-    begin match safe_evar_value sigma ev with
-    | Some c -> whd_evar sigma c
-    | None -> c
-    end
-  | App (f, args) when isEvar f ->
-    (** Enforce smart constructor invariant on applications *)
-    let ev = destEvar f in
-    begin match safe_evar_value sigma ev with
-    | None -> c
-    | Some f -> whd_evar sigma (mkApp (f, args))
-    end
-  | Cast (c0, k, t) when isEvar c0 ->
-    (** Enforce smart constructor invariant on casts. *)
-    let ev = destEvar c0 in
-    begin match safe_evar_value sigma ev with
-    | None -> c
-    | Some c -> whd_evar sigma (mkCast (c, k, t))
-    end
-  | _ -> c
-
-let kind sigma c = Constr.kind (whd_evar sigma c)
-let kind_upto = kind
-let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
-let of_kind = Constr.of_kind
-let of_constr c = c
-let unsafe_to_constr c = c
-let unsafe_eq = Refl
-
-let rec to_constr sigma c = match Constr.kind c with
-| Evar ev ->
-  begin match safe_evar_value sigma ev with
-  | Some c -> to_constr sigma c
-  | None -> Constr.map (fun c -> to_constr sigma c) c
-  end
-| Sort (Sorts.Type u) ->
-  let u' = Evd.normalize_universe sigma u in
-  if u' == u then c else mkSort (Sorts.sort_of_univ u')
-| Const (c', u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkConstU (c', u')
-| Ind (i, u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkIndU (i, u')
-| Construct (co, u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkConstructU (co, u')
-| _ -> Constr.map (fun c -> to_constr sigma c) c
-
-let of_named_decl d = d
-let unsafe_to_named_decl d = d
-let of_rel_decl d = d
-let unsafe_to_rel_decl d = d
-let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
+module EInstance = struct
+  include Evd.MiniEConstr.EInstance
 
+  let equal sigma i1 i2 =
+    Univ.Instance.equal (kind sigma i1) (kind sigma i2)
 end
 
-include API
+include (Evd.MiniEConstr : module type of Evd.MiniEConstr
+         with module ESorts := ESorts
+          and module EInstance := EInstance)
 
 type types = t
 type constr = t
@@ -182,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
 
+let mkRef (gr,u) = let open GlobRef in match gr with
+  | ConstRef c -> mkConstU (c,u)
+  | IndRef ind -> mkIndU (ind,u)
+  | ConstructRef c -> mkConstructU (c,u)
+  | VarRef x -> mkVar x
+
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 
 let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
@@ -201,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false
 let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false
 let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
 let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
+
+let rec isType sigma c = match kind sigma c with
+  | Sort s -> (match ESorts.kind sigma s with
+      | Sorts.Type _ -> true
+      | _ -> false )
+  | Cast (c,_,_) -> isType sigma c
+  | _ -> false
+
 let isVarId sigma id c =
   match kind sigma c with Var id' -> Id.equal id id' | _ -> false
 let isRelN sigma n c =
@@ -274,6 +180,13 @@ let destProj sigma c = match kind sigma c with
 | Proj (p, c) -> (p, c)
 | _ -> raise DestKO
 
+let destRef sigma c = let open GlobRef in match kind sigma c with
+  | Var x -> VarRef x, EInstance.empty
+  | Const (c,u) -> ConstRef c, u
+  | Ind (ind,u) -> IndRef ind, u
+  | Construct (c,u) -> ConstructRef c, u
+  | _ -> raise DestKO
+
 let decompose_app sigma c =
   match kind sigma c with
     | App (f,cl) -> (f, Array.to_list cl)
@@ -381,131 +294,35 @@ let decompose_prod_n_assum sigma n c =
   in
   prodec_rec Context.Rel.empty n c
 
-let existential_type sigma (evk, args) =
-  of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args))
+let existential_type = Evd.existential_type
 
-let map sigma f c = match kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (b,k,t) ->
-      let b' = f b in
-      let t' = f t in
-      if b'==b && t' == t then c
-      else mkCast (b', k, t')
-  | Prod (na,t,b) ->
-      let b' = f b in
-      let t' = f t in
-      if b'==b && t' == t then c
-      else mkProd (na, t', b')
-  | Lambda (na,t,b) ->
-      let b' = f b in
-      let t' = f t in
-      if b'==b && t' == t then c
-      else mkLambda (na, t', b')
-  | LetIn (na,b,t,k) ->
-      let b' = f b in
-      let t' = f t in
-      let k' = f k in
-      if b'==b && t' == t && k'==k then c
-      else mkLetIn (na, b', t', k')
-  | App (b,l) ->
-      let b' = f b in
-      let l' = Array.smartmap f l in
-      if b'==b && l'==l then c
-      else mkApp (b', l')
-  | Proj (p,t) ->
-      let t' = f t in
-      if t' == t then c
-      else mkProj (p, t')
-  | Evar (e,l) ->
-      let l' = Array.smartmap f l in
-      if l'==l then c
-      else mkEvar (e, l')
-  | Case (ci,p,b,bl) ->
-      let b' = f b in
-      let p' = f p in
-      let bl' = Array.smartmap f bl in
-      if b'==b && p'==p && bl'==bl then c
-      else mkCase (ci, p', b', bl')
-  | Fix (ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
-      if tl'==tl && bl'==bl then c
-      else mkFix (ln,(lna,tl',bl'))
-  | CoFix(ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
-      if tl'==tl && bl'==bl then c
-      else mkCoFix (ln,(lna,tl',bl'))
-
-let map_with_binders sigma g f l c0 = match kind sigma c0 with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c0
-  | Cast (c, k, t) ->
-    let c' = f l c in
-    let t' = f l t in
-    if c' == c && t' == t then c0
-    else mkCast (c', k, t')
-  | Prod (na, t, c) ->
-    let t' = f l t in
-    let c' = f (g l) c in
-    if t' == t && c' == c then c0
-    else mkProd (na, t', c')
-  | Lambda (na, t, c) ->
-    let t' = f l t in
-    let c' = f (g l) c in
-    if t' == t && c' == c then c0
-    else mkLambda (na, t', c')
-  | LetIn (na, b, t, c) ->
-    let b' = f l b in
-    let t' = f l t in
-    let c' = f (g l) c in
-    if b' == b && t' == t && c' == c then c0
-    else mkLetIn (na, b', t', c')
-  | App (c, al) ->
-    let c' = f l c in
-    let al' = CArray.Fun1.smartmap f l al in
-    if c' == c && al' == al then c0
-    else mkApp (c', al')
-  | Proj (p, t) ->
-    let t' = f l t in
-    if t' == t then c0
-    else mkProj (p, t')
-  | Evar (e, al) ->
-    let al' = CArray.Fun1.smartmap f l al in
-    if al' == al then c0
-    else mkEvar (e, al')
-  | Case (ci, p, c, bl) ->
-    let p' = f l p in
-    let c' = f l c in
-    let bl' = CArray.Fun1.smartmap f l bl in
-    if p' == p && c' == c && bl' == bl then c0
-    else mkCase (ci, p', c', bl')
-  | Fix (ln, (lna, tl, bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
-    let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
-    if tl' == tl && bl' == bl then c0
-    else mkFix (ln,(lna,tl',bl'))
-  | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = CArray.Fun1.smartmap f l tl in
-    let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
-    mkCoFix (ln,(lna,tl',bl'))
-
-let iter sigma f c = match kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
-  | Cast (c,_,t) -> f c; f t
-  | Prod (_,t,c) -> f t; f c
-  | Lambda (_,t,c) -> f t; f c
-  | LetIn (_,b,t,c) -> f b; f t; f c
-  | App (c,l) -> f c; Array.iter f l
-  | Proj (p,c) -> f c
-  | Evar (_,l) -> Array.iter f l
-  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
-  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
-  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
+
+let map_under_context f n c =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map_under_context f n (unsafe_to_constr c))
+let map_branches f ci br =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
+let map_return_predicate f ci p =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+
+let map_user_view sigma f c =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c)))
+
+let map sigma f c =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map f (unsafe_to_constr (whd_evar sigma c)))
+
+let map_with_binders sigma g f l c =
+  let f l c = unsafe_to_constr (f l (of_constr c)) in
+  of_constr (Constr.map_with_binders g f l (unsafe_to_constr (whd_evar sigma c)))
+
+let iter sigma f c =
+  let f c = f (of_constr c) in
+  Constr.iter f (unsafe_to_constr (whd_evar sigma c))
 
 let iter_with_full_binders sigma g f n c =
   let open Context.Rel.Declaration in
@@ -516,83 +333,76 @@ let iter_with_full_binders sigma g f n c =
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
-  | App (c,l) -> f n c; CArray.Fun1.iter f n l
-  | Evar (_,l) -> CArray.Fun1.iter f n l
-  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | App (c,l) -> f n c; Array.Fun1.iter f n l
+  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i t)) n) n lna tl in
     Array.iter (f n') bl
   | CoFix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in
     Array.iter (f n') bl
 
 let iter_with_binders sigma g f n c =
-  iter_with_full_binders sigma (fun _ acc -> g acc) f n c
+  let f l c = f l (of_constr c) in
+  Constr.iter_with_binders g f n (unsafe_to_constr (whd_evar sigma c))
 
-let fold sigma f acc c = match kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> acc
-  | Cast (c,_,t) -> f (f acc c) t
-  | Prod (_,t,c) -> f (f acc t) c
-  | Lambda (_,t,c) -> f (f acc t) c
-  | LetIn (_,b,t,c) -> f (f (f acc b) t) c
-  | App (c,l) -> Array.fold_left f (f acc c) l
-  | Proj (p,c) -> f acc c
-  | Evar (_,l) -> Array.fold_left f acc l
-  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
-  | CoFix (_,(lna,tl,bl)) ->
-    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+let fold sigma f acc c =
+  let f acc c = f acc (of_constr c) in
+  Constr.fold f acc (unsafe_to_constr (whd_evar sigma c))
 
 let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
   (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
 
 let eq_constr sigma c1 c2 =
-  let kind c = kind_upto sigma c in
+  let kind c = kind sigma c in
+  let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
   let rec eq_constr nargs c1 c2 =
-    compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2
+    compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
   in
-  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 c1 c2
 
 let eq_constr_nounivs sigma c1 c2 =
-  let kind c = kind_upto sigma c in
+  let kind c = kind sigma c in
   let rec eq_constr nargs c1 c2 =
     compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
   in
-  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 c1 c2
 
 let compare_constr sigma cmp c1 c2 =
-  let kind c = kind_upto sigma c in
-  let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
-  compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  let kind c = kind sigma c in
+  let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
+  let cmp nargs c1 c2 = cmp c1 c2 in
+  compare_gen kind eq_inst eq_sorts cmp 0 c1 c2
 
 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
-  let open Universes in
+  let open UnivProblem in
   if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
   else
     CArray.fold_left3
       (fun cstrs v u u' ->
          let open Univ.Variance in
          match v with
-         | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs
+         | Irrelevant -> Set.add (UWeak (u,u')) cstrs
          | Covariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
            (match cv_pb with
-            | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs
-            | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs)
+            | Reduction.CONV -> Set.add (UEq (u,u')) cstrs
+            | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs)
          | Invariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
-           Constraints.add (UEq (u,u')) cstrs)
+           Set.add (UEq (u,u')) cstrs)
       cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
-  let open Universes in
+  let open UnivProblem in
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
@@ -605,7 +415,7 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
     compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
-  let open Universes in
+  let open UnivProblem in
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     cstrs
@@ -616,15 +426,16 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
     else
-      Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs))
+      Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
         cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
 
 let eq_universes env sigma cstrs cv_pb ref nargs l l' =
-  if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true)
+  if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
   else
-    let l = Evd.normalize_universe_instance sigma l
-    and l' = Evd.normalize_universe_instance sigma l' in
-    let open Universes in
+    let l = EInstance.kind sigma l
+    and l' = EInstance.kind sigma l' in
+    let open GlobRef in
+    let open UnivProblem in
     match ref with
     | VarRef _ -> assert false (* variables don't have instances *)
     | ConstRef _ ->
@@ -639,28 +450,28 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
       true
 
 let test_constr_universes env sigma leq m n =
-  let open Universes in
-  let kind c = kind_upto sigma c in
-  if m == n then Some Constraints.empty
+  let open UnivProblem in
+  let kind c = kind sigma c in
+  if m == n then Some Set.empty
   else
-    let cstrs = ref Constraints.empty in
+    let cstrs = ref Set.empty in
     let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
     let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
     and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
     let eq_sorts s1 s2 =
-      let s1 = ESorts.kind sigma (ESorts.make s1) in
-      let s2 = ESorts.kind sigma (ESorts.make s2) in
+      let s1 = ESorts.kind sigma s1 in
+      let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
-      else (cstrs := Constraints.add 
+      else (cstrs := Set.add
               (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	    true)
     in
     let leq_sorts s1 s2 = 
-      let s1 = ESorts.kind sigma (ESorts.make s1) in
-      let s2 = ESorts.kind sigma (ESorts.make s2) in
+      let s1 = ESorts.kind sigma s1 in
+      let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
       else 
-	(cstrs := Constraints.add 
+        (cstrs := Set.add
            (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
@@ -678,63 +489,53 @@ let test_constr_universes env sigma leq m n =
     if res then Some !cstrs else None
 
 let eq_constr_universes env sigma m n =
-  test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+  test_constr_universes env sigma false m n
 let leq_constr_universes env sigma m n =
-  test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+  test_constr_universes env sigma true m n
 
 let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
-  let kind c = kind_upto sigma c in
-  match kind_upto sigma m, kind_upto sigma n with
+  let kind c = kind sigma c in
+  match kind m, kind n with
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
-      (match kind_upto sigma f with
+      (match kind f with
       | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
-          let pb = Environ.lookup_projection p env in
-          let npars = pb.Declarations.proj_npars in
-	  if Array.length args == npars + 1 then
+          let npars = Projection.npars p in
+          if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
 	  else false
       | _ -> false)
   | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
-  let open Universes in
-  if m == n then Some Constraints.empty
+  let open UnivProblem in
+  if m == n then Some Set.empty
   else 
-    let cstrs = ref Constraints.empty in
+    let cstrs = ref Set.empty in
     let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
     let eq_sorts s1 s2 =
+      let s1 = ESorts.kind sigma s1 in
+      let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
       else
-	(cstrs := Constraints.add 
+        (cstrs := Set.add
            (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
     in
-    let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
+    let res = eq_constr' 0 m n in
     if res then Some !cstrs else None
 
-let universes_of_constr env sigma c =
+let universes_of_constr sigma c =
   let open Univ in
-  let open Declarations in
   let rec aux s c =
     match kind sigma c with
     | Const (c, u) ->
-      begin match (Environ.lookup_constant c env).const_universes with
-        | Polymorphic_const _ ->
           LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
-        | Monomorphic_const (univs, _) ->
-          LSet.union s univs
-      end
     | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-      begin match (Environ.lookup_mind mind env).mind_universes with
-        | Cumulative_ind _ | Polymorphic_ind _ ->
           LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
-        | Monomorphic_ind (univs,_) ->
-          LSet.union s univs
-      end
     | Sort u ->
        let sort = ESorts.kind sigma u in
        if Sorts.is_small sort then s
@@ -743,7 +544,7 @@ let universes_of_constr env sigma c =
          LSet.fold LSet.add (Universe.levels u) s
     | Evar (k, args) ->
        let concl = Evd.evar_concl (Evd.find sigma k) in
-       fold sigma aux (aux s (of_constr concl)) c
+       fold sigma aux (aux s concl) c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
@@ -786,7 +587,7 @@ let to_rel_decl = unsafe_to_rel_decl
 type substl = t list
 
 (** Operations that commute with evar-normalization *)
-let lift n c = of_constr (Vars.lift n (to_constr c))
+let lift = lift
 let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
 
 let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c))
@@ -901,9 +702,13 @@ let named_context e = cast_named_context (sym unsafe_eq) (named_context e)
 let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e)
 let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
 
+let of_existential : Constr.existential -> existential =
+  let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+  gen unsafe_eq
+
 let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
-let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e)
 
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
@@ -916,7 +721,7 @@ let map_rel_context_in_env f env sign =
 
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
-  evd, of_constr t
+  evd, t
 
 let is_global sigma gr c =
   Globnames.is_global gr (to_constr sigma c)
@@ -926,7 +731,13 @@ struct
 let to_sorts = ESorts.unsafe_to_sorts
 let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
+let to_constr_array = unsafe_to_constr_array
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
+let to_named_context =
+  let gen : type a b. (a, b) eq -> (a,a) Context.Named.pt -> (b,b) Context.Named.pt
+    = fun Refl x -> x
+  in
+  gen unsafe_eq
 let eq = unsafe_eq
 end