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.

3 files changed, 6 insertions, 39 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