diff options
| author | Hugo Herbelin | 2015-12-20 01:04:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-18 13:07:22 +0200 |
| commit | 2cb554aa772c5c6d179c6a4611b70d459073a316 (patch) | |
| tree | 4493ad52bb7adf03128de2bba63d46f26a893a77 /test-suite | |
| parent | 403af31e3d0bc571acf0a66907277ad839c94df4 (diff) | |
Exporting a generic argument induction_arg. As a consequence,
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/ltac.out | 5 | ||||
| -rw-r--r-- | test-suite/success/Injection.v | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 21a8cf9ede..21554e9ff8 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -16,9 +16,8 @@ The command has indeed failed with message: In nested Ltac calls to "f2", "f1" and "refine", last call failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: -Ltac call to "h" failed. -Error: Ltac variable x is bound to I which cannot be coerced to -a declared or quantified hypothesis. +In nested Ltac calls to "h" and "injection", last call failed. +Error: No primitive equality found. The command has indeed failed with message: In nested Ltac calls to "h" and "injection", last call failed. Error: No primitive equality found. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 56ed89ed86..c072cc6417 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -124,7 +124,7 @@ intros * [= H]. exact H. Abort. -(* Injection does not projects at positions in Prop... allow it? +(* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. Goal forall p q : True\/True, c _ p = c _ q -> False. |