Removing a few suspicious functions from the kernel.

These functions were messing with the deferred universe constraints in an
error-prone way, and were only used for printing as of today. We inline
the one used by the printer instead.

6 files changed, 25 insertions, 48 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 72b490768..4ec8d43e7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -67,37 +67,6 @@ let type_of_constant cb =
       if t' == t then x else RegularArity t'
   | TemplateArity _ as x -> x
 
-let constraints_of_constant otab cb =
-  match cb.const_universes with
-  | Polymorphic_const ctx -> 
-    Univ.UContext.constraints (Univ.instantiate_univ_context ctx)
-  | Monomorphic_const ctx -> 
-    Univ.Constraint.union 
-      (Univ.UContext.constraints ctx)
-      (match cb.const_body with
-       | Undef _ -> Univ.empty_constraint
-       | Def c -> Univ.empty_constraint
-       | OpaqueDef o ->
-         Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
-
-let universes_of_constant otab cb = 
-  match cb.const_body with
-  | Undef _ | Def _ ->
-    begin
-      match cb.const_universes with
-      | Monomorphic_const ctx -> ctx
-      | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
-    end
-  | OpaqueDef o -> 
-    let body_uctxs = Opaqueproof.force_constraints otab o in
-    match cb.const_universes with
-    | Monomorphic_const ctx ->
-      let uctxs = Univ.ContextSet.of_context ctx in
-      Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
-    | Polymorphic_const ctx ->
-      assert(Univ.ContextSet.is_empty body_uctxs);
-      Univ.instantiate_univ_context ctx
-
 let universes_of_polymorphic_constant otab cb = 
   match cb.const_universes with
   | Monomorphic_const _ -> Univ.UContext.empty
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 811a28aa6..7db2050b7 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -39,10 +39,6 @@ val constant_is_polymorphic : constant_body -> bool
 val body_of_constant :
   Opaqueproof.opaquetab -> constant_body -> Term.constr option
 val type_of_constant : constant_body -> constant_type
-val constraints_of_constant :
-  Opaqueproof.opaquetab -> constant_body -> Univ.constraints
-val universes_of_constant :
-  Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
 
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1bd9d6e49..d3fb4ef58 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -368,8 +368,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let u1 = inductive_polymorphic_instance mind1 in
       let arity1,cst1 = constrained_type_of_inductive env 
 	((mind1,mind1.mind_packets.(i)),u1) in
-      let cst2 =
-        Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in 
+      let cst2 = assert false in
+(*       let cst2 = *)
+(*         Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in  *)
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, arity1, typ2) in
@@ -384,8 +385,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
       let u1 = inductive_polymorphic_instance mind1 in
       let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let cst2 =
-        Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
+      let cst2 = assert false in
+(*       let cst2 = *)
+(*         Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in *)
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, ty1, ty2) in
diff --git a/library/global.ml b/library/global.ml
index 6d80012f4..7289cc757 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -124,10 +124,6 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 let opaque_tables () = Environ.opaque_tables (env ())
 let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
 let body_of_constant cst = body_of_constant_body (lookup_constant cst)
-let constraints_of_constant_body cb =
-  Declareops.constraints_of_constant (opaque_tables ()) cb
-let universes_of_constant_body cb =
-  Declareops.universes_of_constant (opaque_tables ()) cb
 
 (** Operations on kernel names *)
 
diff --git a/library/global.mli b/library/global.mli
index a4a38ce84..048ea4d87 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -91,10 +91,6 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive
 val opaque_tables : unit -> Opaqueproof.opaquetab
 val body_of_constant : constant -> Term.constr option
 val body_of_constant_body : Declarations.constant_body -> Term.constr option
-val constraints_of_constant_body :
-  Declarations.constant_body -> Univ.constraints
-val universes_of_constant_body :
-  Declarations.constant_body -> Univ.universe_context
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 6d2bf6b73..51e557f2e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -511,7 +511,25 @@ let print_constant with_values sep sp =
   let val_0 = Global.body_of_constant_body cb in
   let typ = Declareops.type_of_constant cb in
   let typ = ungeneralized_type_of_constant_type typ in
-  let univs = Global.universes_of_constant_body cb in
+  let univs =
+    let otab = Global.opaque_tables () in
+    match cb.const_body with
+    | Undef _ | Def _ ->
+      begin
+        match cb.const_universes with
+        | Monomorphic_const ctx -> ctx
+        | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+      end
+    | OpaqueDef o ->
+      let body_uctxs = Opaqueproof.force_constraints otab o in
+      match cb.const_universes with
+      | Monomorphic_const ctx ->
+        let uctxs = Univ.ContextSet.of_context ctx in
+        Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+      | Polymorphic_const ctx ->
+        assert(Univ.ContextSet.is_empty body_uctxs);
+        Univ.instantiate_univ_context ctx
+  in
   let ctx =
     Evd.evar_universe_context_of_binders
       (Universes.universe_binders_of_global (ConstRef sp))