From 6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 12:56:47 +0200
Subject: Deprecate Global.universes_of_global (replaced by environ version)

---
 engine/univNames.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/univNames.ml b/engine/univNames.ml
index e89dcedb9c..a71f9c5736 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -86,7 +86,7 @@ let register_universe_binders ref ubinders =
       part of the code that depends on the internal representation of names in
       abstract contexts, but removing it requires quite a rework of the
       callers. *)
-  let univs = AUContext.instance (Global.universes_of_global ref) in
+  let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
   let map lvl =
     try LMap.find lvl revmap
-- 
cgit v1.2.3


From 72de7e057505c45cdbf75234a9ea90465d0e19ec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:15:06 +0200
Subject: Simplify fresh_foo_instance functions and pretyping of univ instance

---
 engine/evd.ml      |  2 +-
 engine/univGen.ml  | 87 ++++++++++++++++--------------------------------------
 engine/univGen.mli |  4 +--
 3 files changed, 28 insertions(+), 65 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..eafdc4cb46 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -818,7 +818,7 @@ let fresh_constructor_instance ?loc env evd c =
   with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b07d4848ff..64789cb808 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -11,7 +11,6 @@
 open Sorts
 open Names
 open Constr
-open Environ
 open Univ
 
 (* Generator of levels *)
@@ -50,21 +49,20 @@ let fresh_instance ctx =
   let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
   in !ctx', inst
 
-let existing_instance ctx inst =
+let existing_instance ?loc ctx inst =
   let () =
     let len1 = Array.length (Instance.to_array inst)
     and len2 = AUContext.size ctx in
       if not (len1 == len2) then
-        CErrors.user_err ~hdr:"Universes"
-          Pp.(str "Polymorphic constant expected " ++ int len2 ++
-              str" levels but was given " ++ int len1)
+        CErrors.user_err ?loc ~hdr:"Universes"
+          Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
       else ()
   in LSet.empty, inst
 
-let fresh_instance_from ctx inst =
+let fresh_instance_from ?loc ctx inst =
   let ctx', inst =
     match inst with
-    | Some inst -> existing_instance ctx inst
+    | Some inst -> existing_instance ?loc ctx inst
     | None -> fresh_instance ctx
   in
   let constraints = AUContext.instantiate inst ctx in
@@ -72,63 +70,28 @@ let fresh_instance_from ctx inst =
 
 (** Fresh universe polymorphic construction *)
 
-let fresh_constant_instance env c inst =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_const auctx ->
-    let inst, ctx =
-      fresh_instance_from auctx inst
-    in
-    ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst =
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    ((ind,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind uactx ->
-    let inst, ctx = (fresh_instance_from uactx) inst in
-     ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx =
-      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
-    in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst =
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = fresh_instance_from auctx  inst in
-        (((ind,i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
-    (((ind,i),inst), ctx)
-
 open Globnames
 
-let fresh_global_instance ?names env gr =
-  match gr with
-  | VarRef id -> mkVar id, ContextSet.empty
-  | ConstRef sp ->
-     let c, ctx = fresh_constant_instance env sp names in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = fresh_constructor_instance env sp names in
-       mkConstructU c, ctx
-  | IndRef sp ->
-     let c, ctx = fresh_inductive_instance env sp names in
-       mkIndU c, ctx
-
-let fresh_constant_instance env sp =
-  fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp =
-  fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp =
-  fresh_constructor_instance env sp None
+let fresh_global_instance ?loc ?names env gr =
+  let auctx = Environ.universes_of_global env gr in
+  let u, ctx = fresh_instance_from ?loc auctx names in
+  u, ctx
+
+let fresh_constant_instance env c =
+  let u, ctx = fresh_global_instance env (ConstRef c) in
+  (c, u), ctx
+
+let fresh_inductive_instance env ind =
+  let u, ctx = fresh_global_instance env (IndRef ind) in
+  (ind, u), ctx
+
+let fresh_constructor_instance env c =
+  let u, ctx = fresh_global_instance env (ConstructRef c) in
+  (c, u), ctx
+
+let fresh_global_instance ?loc ?names env gr =
+  let u, ctx = fresh_global_instance ?loc ?names env gr in
+  mkRef (gr, u), ctx
 
 let constr_of_global gr =
   let c, ctx = fresh_global_instance (Global.env ()) gr in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 439424934c..4cfbb94775 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -36,7 +36,7 @@ val new_sort_in_family : Sorts.family -> Sorts.t
 val fresh_instance_from_context : AUContext.t ->
   Instance.t constrained
 
-val fresh_instance_from : AUContext.t -> Instance.t option ->
+val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
 
 val fresh_sort_in_family : Sorts.family ->
@@ -48,7 +48,7 @@ val fresh_inductive_instance : env -> inductive ->
 val fresh_constructor_instance : env -> constructor ->
   pconstructor in_universe_context_set
 
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
   constr in_universe_context_set
 
 val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
-- 
cgit v1.2.3


From 5993c266300cca1c7ca6e8b2b8e3f77f745ca9f9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:27:27 +0200
Subject: Simplify vars_of_global usage

---
 engine/eConstr.ml  |  7 +++++++
 engine/eConstr.mli |  2 ++
 engine/evarutil.ml |  2 +-
 engine/termops.ml  | 19 +++++++------------
 engine/termops.mli |  2 ++
 5 files changed, 19 insertions(+), 13 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8ab3ce821e..cefffb315e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -166,6 +166,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)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..e27eecc24f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -180,6 +180,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
 val decompose_app : Evd.evar_map -> t -> t * t list
 
 (** Pops lambda abstractions until there are no more, skipping casts. *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 13356627f0..f9d9ce3569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -549,7 +549,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
             if Id.Set.mem id' ids then
               raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
           in
-          Id.Set.iter check (Environ.vars_of_global env c)
+          Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
         in
         c
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 1244074d50..ee0c3d210e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -912,9 +912,9 @@ let occur_in_global env id constr =
 
 let occur_var env sigma id c =
   let rec occur_rec c =
-    match EConstr.kind sigma c with
-    | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
-    | _ -> EConstr.iter sigma occur_rec c
+    match EConstr.destRef sigma c with
+    | gr, _ -> occur_in_global env id gr
+    | exception DestKO -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
@@ -961,9 +961,7 @@ let collect_vars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
-let vars_of_global_reference env gr =
-  let c, _ = Global.constr_of_global_in_context env gr in
-  vars_of_global env c
+let vars_of_global_reference = vars_of_global
 
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
@@ -1458,12 +1456,9 @@ let clear_named_body id env =
 
 let global_vars_set env sigma constr =
   let rec filtrec acc c =
-    let acc = match EConstr.kind sigma c with
-    | Var _ | Const _ | Ind _ | Construct _ ->
-      Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
-    | _ -> acc
-    in
-    EConstr.fold sigma filtrec acc c
+    match EConstr.destRef sigma c with
+    | gr, _ -> Id.Set.union (vars_of_global env gr) acc
+    | exception DestKO -> EConstr.fold sigma filtrec acc c
   in
   filtrec Id.Set.empty constr
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 64e3977d68..f7b9469ae8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -118,7 +118,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
+
 val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
+[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
 
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
-- 
cgit v1.2.3


From 5bf063c15468bb81f0f48b583f600250cd829aee Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:37:46 +0200
Subject: UnivGen.constr_of_glob_univ -> Constr.mkRef

---
 engine/eConstr.ml  | 6 ++++++
 engine/eConstr.mli | 2 ++
 engine/univGen.ml  | 7 +------
 engine/univGen.mli | 1 +
 4 files changed, 10 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index cefffb315e..3385b78958 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -74,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
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e27eecc24f..1edc0ee12b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> t -> t
 
+val mkRef : GlobRef.t * EInstance.t -> t
+
 val applist : t * t list -> t
 
 val mkProd_or_LetIn : rel_declaration -> t -> t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 64789cb808..4cdcfd9730 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -105,12 +105,7 @@ let constr_of_global gr =
               str " would forget universes.")
     else c
 
-let constr_of_global_univ (gr,u) =
-  match gr with
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConstU (sp,u)
-  | ConstructRef sp -> mkConstructU (sp,u)
-  | IndRef sp -> mkIndU (sp,u)
+let constr_of_global_univ = mkRef
 
 let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 4cfbb94775..82ec9f3e64 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -63,6 +63,7 @@ val fresh_universe_context_set_instance : ContextSet.t ->
 val global_of_constr : constr -> GlobRef.t puniverses
 
 val constr_of_global_univ : GlobRef.t puniverses -> constr
+[@@ocaml.deprecated "Use [Constr.mkRef]"]
 
 val extend_context : 'a in_universe_context_set -> ContextSet.t ->
   'a in_universe_context_set
-- 
cgit v1.2.3


From 5b49e4d674ee2b41206da2d59dc23e4ae2adf388 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:49:35 +0200
Subject: Simplify UnivGen.type_of_reference

---
 engine/univGen.ml | 58 +++++++++++++++----------------------------------------
 1 file changed, 16 insertions(+), 42 deletions(-)

(limited to 'engine')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 4cdcfd9730..73dd96a540 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -124,52 +124,26 @@ open Declarations
 let type_of_reference env r =
   match r with
   | VarRef id -> Environ.named_type id env, ContextSet.empty
+
   | ConstRef c ->
      let cb = Environ.lookup_constant c env in
      let ty = cb.const_type in
-     begin
-       match cb.const_universes with
-       | Monomorphic_const _ -> ty, ContextSet.empty
-       | Polymorphic_const auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-         Vars.subst_instance_constr inst ty, ctx
-     end
+     let auctx = Declareops.constant_polymorphic_context cb in
+     let inst, ctx = fresh_instance_from auctx None in
+     Vars.subst_instance_constr inst ty, ctx
+
   | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
-         ty, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx  None in
-         let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx =
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
-         in
-         let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-     end
-
-  | ConstructRef cstr ->
-    let (mib,oib as specif) =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
-    in
-    begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-         Inductive.type_of_constructor (cstr,inst) specif, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx =
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
-         in
-         Inductive.type_of_constructor (cstr,inst) specif, ctx
-     end
+    let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
+    let auctx = Declareops.inductive_polymorphic_context mib in
+    let inst, ctx = fresh_instance_from auctx None in
+    let ty = Inductive.type_of_inductive env (specif, inst) in
+    ty, ctx
+
+  | ConstructRef (ind,_ as cstr) ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let auctx = Declareops.inductive_polymorphic_context mib in
+    let inst, ctx = fresh_instance_from auctx None in
+    Inductive.type_of_constructor (cstr,inst) specif, ctx
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
-- 
cgit v1.2.3


From e3615bc48819361891a8d768f5e13eac57a945d0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:51:29 +0200
Subject: Deprecate univ-dropping UnivGen.new_sort_in_family

---
 engine/univGen.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine')

diff --git a/engine/univGen.mli b/engine/univGen.mli
index 82ec9f3e64..78a4dd5500 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -29,6 +29,7 @@ val new_Type_sort : unit -> Sorts.t
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
 val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
 
 (** Build a fresh instance for a given context, its associated substitution and
     the instantiated constraints. *)
-- 
cgit v1.2.3


From bab144fed76c452c49c95c87682d442df68b82f2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:55:56 +0200
Subject: Clean UnivGen.fresh_instance API

---
 engine/univGen.ml  | 46 +++++++++++++++-------------------------------
 engine/univGen.mli |  3 +--
 2 files changed, 16 insertions(+), 33 deletions(-)

(limited to 'engine')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 73dd96a540..443ef22844 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -31,42 +31,26 @@ let new_univ dp = Univ.Universe.make (new_univ_level dp)
 let new_Type dp = mkType (new_univ dp)
 let new_Type_sort dp = Type (new_univ dp)
 
-let fresh_universe_instance ctx =
-  let init _ = new_univ_level () in
-  Instance.of_array (Array.init (AUContext.size ctx) init)
-
-let fresh_instance_from_context ctx =
-  let inst = fresh_universe_instance ctx in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, constraints
-
-let fresh_instance ctx =
-  let ctx' = ref LSet.empty in
-  let init _ =
-    let u = new_univ_level () in
-    ctx' := LSet.add u !ctx'; u
-  in
-  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
-  in !ctx', inst
+let fresh_instance auctx =
+  let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+  let ctx = Array.fold_right LSet.add inst LSet.empty in
+  let inst = Instance.of_array inst in
+  inst, (ctx, AUContext.instantiate inst auctx)
 
-let existing_instance ?loc ctx inst =
+let existing_instance ?loc auctx inst =
   let () =
     let len1 = Array.length (Instance.to_array inst)
-    and len2 = AUContext.size ctx in
+    and len2 = AUContext.size auctx in
       if not (len1 == len2) then
         CErrors.user_err ?loc ~hdr:"Universes"
           Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
       else ()
-  in LSet.empty, inst
-
-let fresh_instance_from ?loc ctx inst =
-  let ctx', inst =
-    match inst with
-    | Some inst -> existing_instance ?loc ctx inst
-    | None -> fresh_instance ctx
   in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, (ctx', constraints)
+  inst, (LSet.empty, AUContext.instantiate inst auctx)
+
+let fresh_instance_from ?loc ctx = function
+  | Some inst -> existing_instance ?loc ctx inst
+  | None -> fresh_instance ctx
 
 (** Fresh universe polymorphic construction *)
 
@@ -129,20 +113,20 @@ let type_of_reference env r =
      let cb = Environ.lookup_constant c env in
      let ty = cb.const_type in
      let auctx = Declareops.constant_polymorphic_context cb in
-     let inst, ctx = fresh_instance_from auctx None in
+     let inst, ctx = fresh_instance auctx in
      Vars.subst_instance_constr inst ty, ctx
 
   | IndRef ind ->
     let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
     let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance_from auctx None in
+    let inst, ctx = fresh_instance auctx in
     let ty = Inductive.type_of_inductive env (specif, inst) in
     ty, ctx
 
   | ConstructRef (ind,_ as cstr) ->
     let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
     let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance_from auctx None in
+    let inst, ctx = fresh_instance auctx in
     Inductive.type_of_constructor (cstr,inst) specif, ctx
 
 let type_of_global t = type_of_reference (Global.env ()) t
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 78a4dd5500..cc3803f393 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -34,8 +34,7 @@ val new_sort_in_family : Sorts.family -> Sorts.t
 (** Build a fresh instance for a given context, its associated substitution and
     the instantiated constraints. *)
 
-val fresh_instance_from_context : AUContext.t ->
-  Instance.t constrained
+val fresh_instance : AUContext.t -> Instance.t in_universe_context_set
 
 val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
-- 
cgit v1.2.3


From da049e138e2b1acf9cdd40d3dbac4508f76f21cb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:08:08 +0200
Subject: Deprecate UnivGen.new_{univ,Type,Type_sort}

They are impractical since we need to get the level out to register it
afterwards.
---
 engine/univGen.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'engine')

diff --git a/engine/univGen.mli b/engine/univGen.mli
index cc3803f393..136c04f969 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -23,9 +23,13 @@ val set_remote_new_univ_id : universe_id RemoteCounter.installer
 
 val new_univ_id : unit -> universe_id
 val new_univ_level : unit -> Level.t
+
 val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
 val new_Type : unit -> types
+[@@ocaml.deprecated "Use [new_univ_level]"]
 val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
 val new_sort_in_family : Sorts.family -> Sorts.t
-- 
cgit v1.2.3


From e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:11:22 +0200
Subject: UnivGen.extend_context -> Univ.extend_in_context_set

Such a basic function can live in Univ rather than the higher level UnivGen.
---
 engine/univGen.ml  | 3 +--
 engine/univGen.mli | 1 +
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 443ef22844..23ab30eb75 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -141,8 +141,7 @@ let fresh_sort_in_family = function
 let new_sort_in_family sf =
   fst (fresh_sort_in_family sf)
 
-let extend_context (a, ctx) (ctx') =
-  (a, ContextSet.union ctx ctx')
+let extend_context = Univ.extend_in_context_set
 
 let new_global_univ () =
   let u = fresh_level () in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 136c04f969..c2e9d0c696 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -71,6 +71,7 @@ val constr_of_global_univ : GlobRef.t puniverses -> constr
 
 val extend_context : 'a in_universe_context_set -> ContextSet.t ->
   'a in_universe_context_set
+[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
 
 (** Create a fresh global in the global environment, without side effects.
     BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
-- 
cgit v1.2.3


From 44ecd58e9ab5fb0f2c45e9eec76440f84995825c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:20:51 +0200
Subject: {Univops -> Vars}.universes_of_constr

It's basically an occur check so it makes sense to put it in vars
---
 engine/univops.ml  | 14 +-------------
 engine/univops.mli |  1 +
 2 files changed, 2 insertions(+), 13 deletions(-)

(limited to 'engine')

diff --git a/engine/univops.ml b/engine/univops.ml
index 7f9672f828..c933641865 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -9,20 +9,8 @@
 (************************************************************************)
 
 open Univ
-open Constr
 
-let universes_of_constr c =
-  let rec aux s c =
-    match kind c with
-    | Const (c, u) ->
-          LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-          LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) ->
-      let u = Sorts.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
+let universes_of_constr = Vars.universes_of_constr
 
 let restrict_universe_context (univs, csts) keep =
   let removed = LSet.diff univs keep in
diff --git a/engine/univops.mli b/engine/univops.mli
index 57a53597b9..0ed06bb204 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -13,6 +13,7 @@ open Univ
 
 (** Return the set of all universes appearing in [constr]. *)
 val universes_of_constr : constr -> LSet.t
+[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
 (** [restrict_universe_context (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
-- 
cgit v1.2.3


From 6aa0aa37e19457a8c0c3ad36f7bbead058442344 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:41:31 +0200
Subject: {Univops->UState}.restrict_universe_context

Thus the adhoc univops can be removed at the end of the deprecation period.

Should we keep exposing restrict_universe_context or make people go
through restrict?

restrict_universe_context is used directly only by newring, where it's
a choice between

    let univs = UState.restrict_universe_context univs vars in

and

    let univs = UState.(context_set (restrict (of_context_set univs) vars)) in
---
 engine/engine.mllib |  2 +-
 engine/uState.ml    | 15 ++++++++++++++-
 engine/uState.mli   | 11 +++++++++++
 engine/univops.ml   | 14 +-------------
 engine/univops.mli  |  5 +----
 5 files changed, 28 insertions(+), 19 deletions(-)

(limited to 'engine')

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 37e83b6238..bb43808542 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,8 +4,8 @@ UnivSubst
 UnivProblem
 UnivMinim
 Universes
-Univops
 UState
+Univops
 Nameops
 Evar_kinds
 Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index 29cb3c9bcc..aa7ec63a6f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -406,12 +406,25 @@ let check_univ_decl ~poly uctx decl =
       (Univ.ContextSet.constraints uctx.uctx_local);
   ctx
 
+let restrict_universe_context (univs, csts) keep =
+  let open Univ in
+  let removed = LSet.diff univs keep in
+  if LSet.is_empty removed then univs, csts
+  else
+  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+  let g = UGraph.empty_universes in
+  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.merge_constraints csts g in
+  let allkept = LSet.diff allunivs removed in
+  let csts = UGraph.constraints_for ~kept:allkept g in
+  (LSet.inter univs keep, csts)
+
 let restrict ctx vars =
   let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
   let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
-  let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
+  let uctx' = restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
 let demote_seff_univs entry uctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index f833508ebf..8053a7bf83 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,6 +13,7 @@
     primitives when needed. *)
 
 open Names
+open Univ
 
 exception UniversesDiffer
 
@@ -91,6 +92,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 (** {5 Unification} *)
 
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+
+(** [restrict uctx ctx] restricts the local universes of [uctx] to
+   [ctx] extended by local named universes and side effect universes
+   (from [demote_seff_univs]). Transitive constraints between retained
+   universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
 val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
diff --git a/engine/univops.ml b/engine/univops.ml
index c933641865..53c42023ad 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -8,18 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Univ
-
 let universes_of_constr = Vars.universes_of_constr
 
-let restrict_universe_context (univs, csts) keep =
-  let removed = LSet.diff univs keep in
-  if LSet.is_empty removed then univs, csts
-  else
-  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
-  let g = UGraph.empty_universes in
-  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
-  let g = UGraph.merge_constraints csts g in
-  let allkept = LSet.diff allunivs removed in
-  let csts = UGraph.constraints_for ~kept:allkept g in
-  (LSet.inter univs keep, csts)
+let restrict_universe_context = UState.restrict_universe_context
diff --git a/engine/univops.mli b/engine/univops.mli
index 0ed06bb204..597d2d6785 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,8 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
-   the universes in [keep]. The constraints [csts] are adjusted so
-   that transitive constraints between remaining universes (those in
-   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
-- 
cgit v1.2.3