diff options
| author | Hugo Herbelin | 2020-11-10 15:14:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 13:57:15 +0100 |
| commit | eae015fa8aadab229a056eb869e2b926fa6c9dc2 (patch) | |
| tree | d005144ea8d3250b78a1de8563f58e833146ec0e /test-suite | |
| parent | 89a4b7e7dd82bd46db2d00b6e48b8989d3a5372b (diff) | |
Avoid exposing an internal names when "intros _ H" fails.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Tactics.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Tactics.v | 8 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 70427220ed..3f07261ca6 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -7,3 +7,5 @@ H is already used. The command has indeed failed with message: H is already used. a +The command has indeed failed with message: +This variable is used in hypothesis H. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 96b6d652c9..8526e43a23 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -30,3 +30,11 @@ Goal True. assert_succeeds should_not_loop. assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) Abort. + +Module IntroWildcard. + +Theorem foo : { p:nat*nat & p = (0,0) } -> True. +Fail intros ((n,_),H). +Abort. + +End IntroWildcard. |