Add [Polymorphic] flag for defs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 22 insertions, 17 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 02330339d..8c52655ff 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -143,6 +143,6 @@ let cook_constant env r =
 	let t = mkArity (ctx,Type s.poly_level) in
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
 	let j = make_judge (constr_of_def body) typ in
-	Typeops.make_polymorphic_if_constant_for_ind env j
+	Typeops.make_polymorphic env j
   in
   (body, typ, cb.const_constraints)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 28f11c9af..32dfaae8f 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -55,9 +55,10 @@ type mutual_inductive_entry = {
 (*s Constants (Definition/Axiom) *)
 
 type definition_entry = {
-  const_entry_body   : constr;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
+  const_entry_body        : constr;
+  const_entry_type        : types option;
+  const_entry_polymorphic : bool;
+  const_entry_opaque      : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 08740afae..5d9569de4 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -51,9 +51,10 @@ type mutual_inductive_entry = {
 (** {6 Constants (Definition/Axiom) } *)
 
 type definition_entry = {
-  const_entry_body   : constr;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
+  const_entry_body        : constr;
+  const_entry_type        : types option;
+  const_entry_polymorphic : bool;
+  const_entry_opaque      : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8146ea7c1..9a73abfad 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -26,14 +26,17 @@ open Type_errors
 open Indtypes
 open Typeops
 
-let constrain_type env j cst1 = function
-  | None ->
-      make_polymorphic_if_constant_for_ind env j, cst1
+let constrain_type env j cst1 poly = function
+  | None -> make_polymorphic env j, cst1
   | Some t ->
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-      assert (t = tj.utj_val);
-      NonPolymorphicType t, union_constraints (union_constraints cst1 cst2) cst3
+	assert (t = tj.utj_val);
+	let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
+	  if poly then 
+	    make_polymorphic env { j with uj_type = tj.utj_val }, cstrs
+	  else
+	    NonPolymorphicType t, cstrs
 
 let local_constrain_type env j cst1 = function
   | None ->
@@ -92,7 +95,8 @@ let infer_declaration env dcl =
   match dcl with
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
-      let (typ,cst) = constrain_type env j cst c.const_entry_type in
+      let (typ,cst) = constrain_type env j cst 
+	c.const_entry_polymorphic c.const_entry_type 
       let def =
 	if c.const_entry_opaque
 	then OpaqueDef (Declarations.opaque_from_val j.uj_val)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 85e8e6c88..b7a8b7d4e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -130,10 +130,10 @@ let extract_context_levels env =
   List.fold_left
     (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
 
-let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
+let make_polymorphic env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
-  | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
+  | Sort (Type u) ->
       let param_ccls = extract_context_levels env params in
       let s = { poly_param_levels = param_ccls; poly_level = u} in
       PolymorphicArity (params,s)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index c1c805f38..af46b9875 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -101,6 +101,5 @@ val type_of_constant_knowing_parameters :
   env -> constant_type -> constr array -> types
 
 (** Make a type polymorphic if an arity *)
-val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
-  constant_type
+val make_polymorphic : env -> unsafe_judgment -> constant_type