diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/output | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Inductive.out | 3 | ||||
-rw-r--r-- | test-suite/output/Inductive.v | 3 | ||||
-rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
-rw-r--r-- | test-suite/output/PrintAssumptions.out | 7 | ||||
-rw-r--r-- | test-suite/output/PrintAssumptions.v | 16 | ||||
-rw-r--r-- | test-suite/output/PrintModule.out | 4 | ||||
-rw-r--r-- | test-suite/output/PrintModule.v | 34 | ||||
-rw-r--r-- | test-suite/output/inference.out | 4 | ||||
-rw-r--r-- | test-suite/output/ltac.out | 2 | ||||
-rw-r--r-- | test-suite/output/ltac.v | 17 |
10 files changed, 85 insertions, 9 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out new file mode 100644 index 00000000..e912003f --- /dev/null +++ b/test-suite/output/Inductive.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Last occurrence of "list'" must have "A" as 1st argument in + "A -> list' A -> list' (A * A)%type". diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v new file mode 100644 index 00000000..8db8956e --- /dev/null +++ b/test-suite/output/Inductive.v @@ -0,0 +1,3 @@ +Fail Inductive list' (A:Set) : Set := +| nil' : list' A +| cons' : A -> list' A -> list' (A*A). diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 6efd671a..b1558dab 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -70,7 +70,7 @@ FST (0; 1) : Z Nil : forall A : Type, list A -NIL:list nat +NIL : list nat : list nat (false && I 3)%bool /\ I 6 : Prop @@ -78,7 +78,7 @@ NIL:list nat : Z * Z * Z * (Z * Z * Z) [|0 * (1, 2, 3); (4, 5, 6) * false|] : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) -fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z +fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z : (Z -> Z -> Z -> Z) -> Z Init.Nat.add : nat -> nat -> nat diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 08df9150..66458543 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -2,11 +2,6 @@ Axioms: foo : nat Axioms: foo : nat -Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZAdd -Fetching opaque proofs from disk for Coq.Arith.PeanoNat -Fetching opaque proofs from disk for Coq.Classes.Morphisms -Fetching opaque proofs from disk for Coq.Init.Logic -Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZBase Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g @@ -21,3 +16,5 @@ extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Closed under the global context Closed under the global context +Axioms: +M.foo : False diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index f23bc498..c2003816 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -94,3 +94,19 @@ Proof (false_positive.add_comm 5). Print Assumptions comm_plus5. (* Should answer : Closed under the global context *) + +(** Print Assumption and Include *) + +Module INCLUDE. + +Module M. +Axiom foo : False. +End M. + +Module N. +Include M. +End N. + +Print Assumptions N.foo. + +End INCLUDE. diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out new file mode 100644 index 00000000..db464fd0 --- /dev/null +++ b/test-suite/output/PrintModule.out @@ -0,0 +1,4 @@ +Module N : S with Definition T := nat := M + +Module N : S with Module T := K := M + diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v new file mode 100644 index 00000000..999d9a98 --- /dev/null +++ b/test-suite/output/PrintModule.v @@ -0,0 +1,34 @@ +Module FOO. + +Module M. + Definition T := nat. +End M. + +Module Type S. + Parameter T : Set. +End S. + +Module N : S with Definition T := nat := M. + +Print Module N. + +End FOO. + +Module BAR. + +Module K. End K. +Module Type KS. End KS. + +Module M. + Module T := K. +End M. + +Module Type S. + Declare Module T : KS. +End S. + +Module N : S with Module T := K := M. + +Print Module N. + +End BAR. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index b1952aec..f2d14477 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,12 +6,12 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n in ?y ?y0:T n +fun n : nat => let x := A n in ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat x := A n : T n |- ?T0 -> T n] ?y0 : [n : nat x := A n : T n |- ?T0] -fun n : nat => ?y ?y0:T n +fun n : nat => ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat |- ?T0 -> T n] diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out new file mode 100644 index 00000000..d003c70d --- /dev/null +++ b/test-suite/output/ltac.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +Error: Ltac variable y depends on pattern variable name z which is not bound in current context. diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v new file mode 100644 index 00000000..7e2610c7 --- /dev/null +++ b/test-suite/output/ltac.v @@ -0,0 +1,17 @@ +(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *) +Goal True. +Fail let T := constr:((fun a b : nat => a+b) 1 1) in + lazymatch T with + | (fun x z => ?y) 1 1 + => pose ((fun x _ => y) 1 1) + end. +Abort. + +(* This should not raise a warning (see #4317) *) +Goal True. +assert (H:= eq_refl ((fun x => x) 1)). +let HT := type of H in +lazymatch goal with +| H1 : HT |- _ => idtac +end. +Abort. |