diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/univers.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/univers.v')
-rw-r--r-- | test-suite/success/univers.v | 60 |
1 files changed, 39 insertions, 21 deletions
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index a619b8da..87edc4de 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -1,40 +1,58 @@ (* This requires cumulativity *) Definition Type2 := Type. -Definition Type1 := Type : Type2. +Definition Type1 : Type2 := Type. -Lemma lem1 : (True->Type1)->Type2. -Intro H. -Apply H. -Exact I. +Lemma lem1 : (True -> Type1) -> Type2. +intro H. +apply H. +exact I. Qed. -Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). -Auto. +Lemma lem2 : + forall (A : Type) (P : A -> Type) (x : A), + (forall y : A, x = y -> P y) -> P x. +auto. Qed. -Lemma lem3 : (P:Prop)P. -Intro P ; Pattern P. -Apply lem2. +Lemma lem3 : forall P : Prop, P. +intro P; pattern P in |- *. +apply lem2. Abort. (* Check managing of universe constraints in inversion *) (* Bug report #855 *) -Inductive dep_eq : (X:Type) X -> X -> Prop := - | intro_eq : (X:Type) (f:X)(dep_eq X f f) - | intro_feq : (A:Type) (B:A->Type) - let T = (x:A)(B x) in - (f, g:T) (x:A) - (dep_eq (B x) (f x) (g x)) -> - (dep_eq T f g). +Inductive dep_eq : forall X : Type, X -> X -> Prop := + | intro_eq : forall (X : Type) (f : X), dep_eq X f f + | intro_feq : + forall (A : Type) (B : A -> Type), + let T := forall x : A, B x in + forall (f g : T) (x : A), dep_eq (B x) (f x) (g x) -> dep_eq T f g. Require Import Relations. -Theorem dep_eq_trans : (X:Type) (transitive X (dep_eq X)). +Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X). Proof. - Unfold transitive. - Intros X f g h H1 H2. - Inversion H1. + unfold transitive in |- *. + intros X f g h H1 H2. + inversion H1. Abort. + +(* Submitted by Bas Spitters (bug report #935) *) + +(* This is a problem with the status of the type in LetIn: is it a + user-provided one or an inferred one? At the current time, the + kernel type-check the type in LetIn, which means that it must be + considered as user-provided when calling the kernel. However, in + practice it is inferred so that a universe refresh is needed to set + its status as "user-provided". + + Especially, universe refreshing was not done for "set/pose" *) + +Lemma ind_unsec : forall Q : nat -> Type, True. +intro. +set (C := forall m, Q m -> Q m). +exact I. +Qed. |