diff options
Diffstat (limited to 'test-suite/bugs/closed/4882.v')
-rw-r--r-- | test-suite/bugs/closed/4882.v | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v deleted file mode 100644 index 8c26af70..00000000 --- a/test-suite/bugs/closed/4882.v +++ /dev/null @@ -1,50 +0,0 @@ - -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. |