Correction trou de typage des éliminations d'inductifs introduit dans commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou

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

2 files changed, 82 insertions, 12 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 103a5982ef..d47a796ef1 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -116,8 +116,6 @@ let is_info_type env t =
 
 let is_small infos = List.for_all (fun (logic,small) -> small) infos
 let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
-let is_logic_arity infos =
-  List.for_all (fun (logic,small) -> logic || small) infos
 
 (* An inductive definition is a "unit" if it has only one constructor
    and that all arguments expected by this constructor are 
@@ -505,19 +503,29 @@ let is_recursive = Rtree.is_infinite
   array_exists one_is_rec
 *)
 
+(* Allowed eliminations *)
+
 let all_sorts = [InProp;InSet;InType]
-let impredicative_sorts = [InProp;InSet]
+let small_sorts = [InProp;InSet]
 let logical_sorts = [InProp]
 
-let allowed_sorts env issmall isunit = function
+let allowed_sorts issmall isunit = function
+  (* Type: all elimination allowed *)
   | Type _ -> all_sorts
-  | Prop Pos -> 
-      if issmall then all_sorts
-      else impredicative_sorts
-  | Prop Null -> 
-(* 29/1/02: added InType which is derivable when the type is unit and small *)
-      if isunit then all_sorts
-      else logical_sorts
+
+  (* Small Set is predicative: all elimination allowed *)
+  | Prop Pos when issmall -> all_sorts
+
+  (* Large Set is necessarily impredicative: forbids large elimination *)
+  | Prop Pos -> small_sorts
+
+  (* Unitary/empty Prop: elimination to all sorts are realizable *)
+  (* unless the type is large. If it is large, forbids large elimination *)
+  (* which otherwise allows to simulate the inconsistent system Type:Type *)
+  | Prop Null when isunit -> if issmall then all_sorts else small_sorts
+
+  (* Other propositions: elimination only to Prop *)
+  | Prop Null -> logical_sorts
 
 let fold_inductive_blocks f =
   Array.fold_left (fun acc (_,ar,_,_,_,lc) -> f (Array.fold_left f acc lc) ar)
@@ -547,7 +555,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	splayed_lc in
     (* Elimination sorts *)
     let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
-    let kelim = allowed_sorts env issmall isunit ar_sort in
+    let kelim = allowed_sorts issmall isunit ar_sort in
     let nconst, nblock = ref 0, ref 0 in 
     let transf num =
       let arity = List.length (dest_subterms recarg).(num) in
diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
new file mode 100644
index 0000000000..6866f19ae4
--- /dev/null
+++ b/test-suite/failure/Uminus.v
@@ -0,0 +1,62 @@
+(* Check that the encoding of system U- fails *)
+
+Inductive prop : Prop := down : Prop -> prop.
+
+Definition up (p:prop) : Prop := let (A) := p in A.
+
+Lemma p2p1 : forall A:Prop, up (down A) -> A.
+Proof.
+exact (fun A x => x).
+Qed.
+
+Lemma p2p2 : forall A:Prop, A -> up (down A).
+Proof.
+exact (fun A x => x).
+Qed.
+
+(** Hurkens' paradox *)
+
+Definition V := forall A:Prop, ((A -> prop) -> A -> prop) -> A -> prop.
+Definition U := V -> prop.
+Definition sb (z:V) : V := fun A r a => r (z A r) a.
+Definition le (i:U -> prop) (x:U) : prop :=
+  x (fun A r a => i (fun v => sb v A r a)).
+Definition induct (i:U -> prop) : Prop :=
+  forall x:U, up (le i x) -> up (i x).
+Definition WF : U := fun z => down (induct (z U le)).
+Definition I (x:U) : Prop :=
+  (forall i:U -> prop, up (le i x) -> up (i (fun v => sb v U le x))) -> False.
+
+Lemma Omega : forall i:U -> prop, induct i -> up (i WF).
+Proof.
+intros i y.
+apply y.
+unfold le, WF, induct in |- *.
+intros x H0.
+apply y.
+exact H0.
+Qed.
+
+Lemma lemma1 : induct (fun u => down (I u)).
+Proof.
+unfold induct in |- *.
+intros x p.
+intro q.
+apply (q (fun u => down (I u)) p).
+intro i.
+apply q with (i := fun y => i (fun v:V => sb v U le y)).
+Qed.
+
+Lemma lemma2 : (forall i:U -> prop, induct i -> up (i WF)) -> False.
+Proof.
+intro x.
+apply (x (fun u => down (I u)) lemma1).
+intros i H0.
+apply (x (fun y => i (fun v => sb v U le y))).
+apply H0.
+Qed.
+
+Theorem paradox : False.
+Proof.
+exact (lemma2 Omega).
+Qed.