diff options
Diffstat (limited to 'test-suite/output/Search.v')
| -rw-r--r-- | test-suite/output/Search.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |