diff options
| author | Maxime Dénès | 2017-04-24 14:36:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-24 14:36:45 +0200 |
| commit | 83d30f7aa8be369a8caf7c130d5dfa4962470eda (patch) | |
| tree | 2919bee50a58ec3810950be43cdb18d96830c0c8 /test-suite | |
| parent | ecff95e24e69a8761f7aa154312fdcc01f99766b (diff) | |
| parent | 6c683786c8100259e8c78b710e4a75974ae00eba (diff) | |
Merge PR#565: 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 81fda176ec..7446c17d98 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 2a0f0b407c..82096f29bf 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. |