From a1fd5fb489237a1300adb242e2c9b6c74c82981b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 12 Apr 2017 14:16:04 +0200
Subject: Porting the firstorder plugin to the new tactic API.

---
 plugins/firstorder/ground.ml | 38 +++++++++++++++++++++++---------------
 1 file changed, 23 insertions(+), 15 deletions(-)

(limited to 'plugins/firstorder/ground.ml')

diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d6cd7e2a0..ab1dd07c1 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -12,8 +12,9 @@ open Sequent
 open Rules
 open Instances
 open Term
-open Tacmach
-open Tacticals
+open Tacmach.New
+open Tacticals.New
+open Proofview.Notations
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
@@ -29,18 +30,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 { 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 { enter = begin fun gl ->
+    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
+        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
@@ -60,7 +67,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
@@ -80,7 +87,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
@@ -119,7 +126,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 }
-- 
cgit v1.2.3