diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-12 10:43:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-19 17:43:26 +0200 |
| commit | 50dc7d426824b8e02e337682597605f022de2dd9 (patch) | |
| tree | 30b65cf873cf460044839bf3ff2134991faf6227 /test-suite/output/FunExt.out | |
| parent | 978dd21af8467aa483bce551b3d5df8895cfff0f (diff) | |
Adding an "extensionality in H" tactic which applies functional
extensionality in H supposed to be a quantified equality until
giving a bare equality.
Thanks to Jason Gross and Jonathan Leivent for suggestions and
examples.
Diffstat (limited to 'test-suite/output/FunExt.out')
| -rw-r--r-- | test-suite/output/FunExt.out | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out new file mode 100644 index 000000000..b97fe7a88 --- /dev/null +++ b/test-suite/output/FunExt.out @@ -0,0 +1,15 @@ +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not a non-dependent hypothesis. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not a non-dependent hypothesis. +The command has indeed failed with message: +Ltac call to "extensionality" failed. +Tactic failure: Not an extensional equality. |