From 0daae2bd1ab518d8fcb6d59a5616786ade94d1e5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Dec 2017 16:26:24 +0100 Subject: Deprecate implicit tactic solving. --- test-suite/success/ImplicitTactic.v | 16 ---------------- 1 file changed, 16 deletions(-) delete mode 100644 test-suite/success/ImplicitTactic.v (limited to 'test-suite/success') 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). - -- cgit v1.2.3