diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-15 22:10:08 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 13:32:33 +0200 |
| commit | 6c683786c8100259e8c78b710e4a75974ae00eba (patch) | |
| tree | 0a0dc4c63582c9ba1c64cf9c783da53fca8006af /test-suite | |
| parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) | |
Remove VernacError
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Search.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 10 |
2 files changed, 17 insertions, 1 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 81fda176e..7446c17d9 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -98,6 +98,14 @@ h: n <> newdef n h': newdef n <> n h: n <> newdef n h: n <> newdef n +h: n <> newdef n +h': newdef n <> n +The command has indeed failed with message: +No such goal. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. h: P n h': ~ P n h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2a0f0b407..82096f29b 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. - intros n h h'. + cut False. + intros _ n h h'. Search n. (* search hypothesis *) Search newdef. (* search hypothesis *) Search ( _ <> newdef _). (* search hypothesis, pattern *) Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) + + 1:Search newdef. + 2:Search newdef. + + Fail 3:Search newdef. + Fail 1-2:Search newdef. + Fail all:Search newdef. Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. |