Merge PR #853: Clean 'with Definition' implementation.

7 files changed, 32 insertions, 80 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9a75b1993..1337036b8 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 d698d88b4..7350724b8 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/mod_typing.ml b/kernel/mod_typing.ml
index f53ef6f56..71c037008 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,16 +72,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
-      let uctx = (* Context of the spec *)
+      let c', univs, ctx' =
         match cb.const_universes with
-        | Monomorphic_const _ -> uctx
-        | Polymorphic_const auctx ->
-	  Univ.instantiate_univ_context auctx
-      in
-      let c', univs, ctx' = 
-	if not (Declareops.constant_is_polymorphic cb) then
-	  let env' = Environ.push_context ~strict:true uctx env' in
+        | Monomorphic_const _ ->
+          (** We do not add the deferred constraints of the body in the
+              environment, because they do not appear in the type of the
+              definition. Any inconsistency will be raised at a later stage
+              when joining the environment. *)
 	  let env' = Environ.push_context ~strict:true ctx env' in
 	  let c',cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
@@ -94,7 +91,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	       let c' = Mod_subst.force_constr cs in
 	         c, Reduction.infer_conv env' (Environ.universes env') c c'
 	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
-	else
+        | Polymorphic_const uctx ->
+          let uctx = Univ.instantiate_univ_context uctx in
 	  let cus, ccst = Univ.UContext.dest uctx in
 	  let newus, cst = Univ.UContext.dest ctx in
 	  let () =
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 44a1e6191..6f128d5d3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -358,38 +358,17 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	      let c2 = Mod_subst.force_constr lc2 in
 	      check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
    | IndType ((kn,i),mind1) ->
-       ignore (CErrors.user_err Pp.(str @@
+       CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
-       "name."));
-      let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
-      if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
-      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 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
-       check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2
-   | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (CErrors.user_err Pp.(str @@
+       "name.")
+   | IndConstr (((kn,i),j),mind1) ->
+      CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-       "name."));
-      let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
-      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 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
-       check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2
+       "name.")
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module msb1 in
diff --git a/library/global.ml b/library/global.ml
index dd7f23378..8b59c84dd 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 c7ccabe1a..754fa1516 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 faa69f41e..15c0f80b9 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))