diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 1 | ||||
| -rw-r--r-- | plugins/firstorder/ground.ml | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b81010c7bd..3c6ab47e9b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Formula diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index d462013353..09147d606c 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -37,7 +37,7 @@ let ground_tac solver startseq = let () = if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then - let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in + let gl = { Evd.it = Proofview.Goal.goal gl; sigma = project gl } in Feedback.msg_debug (Printer.pr_goal gl) in tclORELSE (axiom_tac seq.gl seq) |