diff options
Diffstat (limited to 'plugins/firstorder/ground.ml')
| -rw-r--r-- | plugins/firstorder/ground.ml | 50 |
1 files changed, 30 insertions, 20 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 628af4e7..4e3ba573 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -1,18 +1,21 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Ltac_plugin open Formula open Sequent open Rules open Instances -open Term -open Tacmach -open Tacticals +open Constr +open Tacmach.New +open Tacticals.New let update_flags ()= let predref=ref Names.Cpred.empty in @@ -28,18 +31,24 @@ let update_flags ()= CClosure.betaiotazeta (Names.Id.Pred.full,Names.Cpred.complement !predref) -let ground_tac solver startseq gl= +let ground_tac solver startseq = + Proofview.Goal.enter begin fun gl -> update_flags (); - let rec toptac skipped seq gl= - if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Feedback.msg_debug (Printer.pr_goal gl); + let rec toptac skipped seq = + Proofview.Goal.enter begin fun gl -> + let () = + if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 + then + 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) begin try - let (hd,seq1)=take_formula seq - and re_add s=re_add_formula_list skipped s in + let (hd,seq1)=take_formula (project gl) seq + and re_add s=re_add_formula_list (project gl) skipped s in let continue=toptac [] - and backtrack gl=toptac (hd::skipped) seq1 gl in + and backtrack =toptac (hd::skipped) seq1 in match hd.pat with Right rpat-> begin @@ -59,7 +68,7 @@ let ground_tac solver startseq gl= or_tac backtrack continue (re_add seq1) | Rfalse->backtrack | Rexists(i,dom,triv)-> - let (lfp,seq2)=collect_quantified seq in + let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 @@ -79,7 +88,7 @@ let ground_tac solver startseq gl= left_or_tac ind backtrack hd.id continue (re_add seq1) | Lforall (_,_,_)-> - let (lfp,seq2)=collect_quantified seq in + let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 @@ -118,7 +127,8 @@ let ground_tac solver startseq gl= ll_atom_tac typ la_tac hd.id continue (re_add seq1) end with Heap.EmptyHeap->solver - end gl in - let seq, gl' = startseq gl in - wrap (List.length (pf_hyps gl)) true (toptac []) seq gl' - + end + end in + let n = List.length (Proofview.Goal.hyps gl) in + startseq (fun seq -> wrap n true (toptac []) seq) + end |