diff options
author | 2011-07-26 20:30:32 +0000 | |
---|---|---|
committer | 2011-07-26 20:30:32 +0000 | |
commit | 2bc740de1bd1476c39aeedd14a9586b2c426d7d6 (patch) | |
tree | e21dfcd4c26f23cb265663f577fe3c92cd75290b /test-suite | |
parent | 535790b58a83879bdabd61914f68efe8e1ec469a (diff) |
or_introl is now too complicated for basic tests of test-suite/output/PrintInfos.v
This is due to r14296.
existT should do the job.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/PrintInfos.out | 23 | ||||
-rw-r--r-- | test-suite/output/PrintInfos.v | 6 |
2 files changed, 14 insertions, 15 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index d60c8097c..f423f8513 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,17 +1,16 @@ -or_introl : forall A B : Prop, A -> A \/ B +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P Argument A is implicit -Argument scopes are [type_scope type_scope _] -Expands to: Constructor Coq.Init.Logic.or_introl -Inductive or (A B : Prop) : Prop := - or_introl : A -> A \/ B | or_intror : B -> A \/ B - -For or_introl: Argument A is implicit -For or_intror: Argument B is implicit -For or: Argument scopes are [type_scope type_scope] -For or_introl: Argument scopes are [type_scope type_scope _] -For or_intror: Argument scopes are [type_scope type_scope _] -or_introl : forall A B : Prop, A -> A \/ B +Argument scopes are [type_scope _ _ _] +Expands to: Constructor Coq.Init.Specif.existT +Inductive sigT (A : Type) (P : A -> Type) : Type := + existT : forall x : A, P x -> sigT P + +For sigT: Argument A is implicit +For existT: Argument A is implicit +For sigT: Argument scopes are [type_scope type_scope] +For existT: Argument scopes are [type_scope _ _ _] +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index dd9f3c07a..6a89f8809 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -1,6 +1,6 @@ -About or_introl. -Print or_introl. -Print Implicit or_introl. +About existT. +Print existT. +Print Implicit existT. Print eq_refl. About eq_refl. |