Correction d'une incohérence de typage des inductifs polymorphes: les

contraintes bornant par le haut le type de l'inductif (ce qui peut
arriver quand l'inductif est argument d'une constante) étaient
oubliées : on pouvait se retrouver avec des inductifs dont le type des
constructeurs, une fois instancié par des paramètres) n'était plus
typable (seul leur réduit, après expansion des constantes, était
typable). [kernel, test-suite]

+ Affichage des inductifs (via Print) en prenant la forme utilisateur des
  constructeurs.
+ Correction warning dans compilation gallina.ml.



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

5 files changed, 18 insertions, 3 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index cd9e2e81f4..5786e67d53 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -254,10 +254,13 @@ let typecheck_inductive env mie =
     array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
       let sign, s = dest_arity env full_arity in
       let status,cst = match s with
-      | Type _ when ar_level <> None (* Explicitly polymorphic *) ->
+      | Type u when ar_level <> None (* Explicitly polymorphic *) 
+            && no_upper_constraints u cst ->
 	  (* The polymorphic level is a function of the level of the *)
 	  (* conclusions of the parameters *)
-	  Inr (param_ccls, lev), cst
+          (* We enforce [u >= lev] in case [lev] has a strict upper *)
+          (* constraints over [u] *)
+	  Inr (param_ccls, lev), enforce_geq u lev cst
       | Type u (* Not an explicit occurrence of Type *) ->
 	  Inl (info,full_arity,s), enforce_geq u lev cst
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8ff8ddb85e..918a32c956 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -228,7 +228,9 @@ let arities_of_specif kn (mib,mip) =
 let arities_of_constructors ind specif = 
   arities_of_specif (fst ind) specif
 
-
+let type_of_constructors ind (mib,mip) =
+  let specif = mip.mind_user_lc in
+  Array.map (constructor_instantiate (fst ind) mib) specif
 
 (************************************************************************)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e63c7772c3..118d19830e 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -47,6 +47,9 @@ val type_of_constructor : constructor -> mind_specif -> types
 (* Return constructor types in normal form *)
 val arities_of_constructors : inductive -> mind_specif -> types array
 
+(* Return constructor types in user form *)
+val type_of_constructors : inductive -> mind_specif -> types array
+
 (* Transforms inductive specification into types (in nf) *)
 val arities_of_specif : mutual_inductive -> mind_specif -> types array 
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 001ee3ea8a..a681210acf 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -550,6 +550,11 @@ let subst_large_constraint u u' v =
 let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
 
+let no_upper_constraints u cst =
+  match u with
+  | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
+  | Max _ -> anomaly "no_upper_constraints"
+
 (* Pretty-printing *)
 
 let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1ce5329ab9..225dce9a6c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -76,6 +76,8 @@ val subst_large_constraint : universe -> universe -> universe -> universe
 val subst_large_constraints : 
   (universe * universe) list -> universe -> universe
 
+val no_upper_constraints : universe -> constraints -> bool
+
 (*s Pretty-printing of universes. *)
 
 val pr_uni : universe -> Pp.std_ppcmds