diff options
| author | Hugo Herbelin | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:22:00 +0200 |
| commit | 50374354b7ced786d68d45884295a4c770642123 (patch) | |
| tree | 9c11b0cd9502e95ec6e296a5b1a50386dcca2eca /test-suite | |
| parent | 34237bb07fa8663d3d9e8ca4f9459f46841fd43d (diff) | |
Cleaning the use of pstate and evar_map in Search.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Search.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 9 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index a527b5e9f8..43f4ed13d9 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -285,3 +285,5 @@ h: P n h': ~ P n h: P n h: P n +a: A +b: A diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 82096f29bf..08245a4a91 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -35,3 +35,12 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False. Abort. +Module M. +Section S. +Variable A:Type. +Variable a:A. +Theorem Thm (b:A) : True. +Search A. (* Test search in hypotheses *) +Abort. +End S. +End M. |