From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- plugins/firstorder/g_ground.ml4 | 2 -- 1 file changed, 2 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 4a38c48d..034dc3c2 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -134,8 +134,6 @@ TACTIC EXTEND firstorder | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> [ gen_ground_tac true (Option.map eval_tactic t) l l' ] -| [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) [] [] ] END TACTIC EXTEND gintuition -- cgit v1.2.3