diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-04 21:09:49 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-04 21:09:49 +0200 |
commit | d862b659457b12437d4fa348c3c4dc3dd08d8065 (patch) | |
tree | fc4c5009977361e932043cdfff9b4ff434cc1ba0 /test-suite | |
parent | b0ed0c2c1c7ca8fc434ecadd3a9ed906e6e428c2 (diff) | |
parent | 2eecd666a45a79241f0aadb9493ae8ef9cc9795e (diff) |
Merge PR #7229: Deprecate implicit tactic solving.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/4882.v | 50 | ||||
-rw-r--r-- | test-suite/success/ImplicitTactic.v | 16 |
2 files changed, 0 insertions, 66 deletions
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v deleted file mode 100644 index 8c26af708..000000000 --- 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. diff --git a/test-suite/success/ImplicitTactic.v b/test-suite/success/ImplicitTactic.v deleted file mode 100644 index d8fa3043d..000000000 --- a/test-suite/success/ImplicitTactic.v +++ /dev/null @@ -1,16 +0,0 @@ -(* A Wiedijk-Cruz-Filipe style tactic for solving implicit arguments *) - -(* Declare a term expression with a hole *) -Parameter quo : nat -> forall n:nat, n<>0 -> nat. -Notation "x / y" := (quo x y _) : nat_scope. - -(* Declare the tactic for resolving implicit arguments still - unresolved after type-checking; it must complete the subgoal to - succeed *) -Declare Implicit Tactic assumption. - -Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. -intros. -(* Here, assumption is used to solve the implicit argument of quo *) -exists (n / d). - |