diff options
author | 2016-07-04 16:17:41 +0200 | |
---|---|---|
committer | 2016-07-04 16:17:41 +0200 | |
commit | c78b84425be7535e46c63e80200c07a1921e67bd (patch) | |
tree | 0ea661c36ca1da6966b12b1d6c3389c9c020ffc5 /test-suite/bugs/closed/4882.v | |
parent | 9468bcd39808f4587d3732f46773b1e339b2267c (diff) | |
parent | c22f6694bac3479426cf179839430d9d8675e456 (diff) |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'test-suite/bugs/closed/4882.v')
-rw-r--r-- | test-suite/bugs/closed/4882.v | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v new file mode 100644 index 000000000..8c26af708 --- /dev/null +++ b/test-suite/bugs/closed/4882.v @@ -0,0 +1,50 @@ + +Definition Foo {T}{a : T} : T := a. + +Module A. + + Declare Implicit Tactic eauto. + + Goal forall A (x : A), A. + intros. + apply Foo. (* Check defined evars are normalized *) + (* Qed. *) + Abort. + +End A. + +Module B. + + Definition Foo {T}{a : T} : T := a. + + Declare Implicit Tactic eassumption. + + Goal forall A (x : A), A. + intros. + apply Foo. + (* Qed. *) + Abort. + +End B. + +Module C. + + Declare Implicit Tactic first [exact True|assumption]. + + Goal forall (x : True), True. + intros. + apply (@Foo _ _). + Qed. + +End C. + +Module D. + + Declare Implicit Tactic assumption. + + Goal forall A (x : A), A. + intros. + exact _. + Qed. + +End D. |