Writing Tactics.keep in the new monad.

4 files changed, 19 insertions, 13 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index d7344d3558..43fefc4c6c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1435,7 +1435,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 	    (Proofview.V82.of_tactic (apply (mkVar hrec)))
 	    [ tclTHENSEQ
 		[
-		  keep (tcc_hyps@eqs);
+		  (Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
 		  (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
 		  (fun g ->
 		     if is_mes
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ac2255488b..c76c28dbfc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2017,12 +2017,15 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (Elim.h_double_induction h1 h2)
   (* Context management *)
   | TacClear (b,l) ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") begin
-      Proofview.V82.tactic begin fun gl ->
-        let l = interp_hyp_list ist (pf_env gl) (project gl) l in
-        if b then Tactics.keep l gl else Tactics.clear l gl
-      end
+      Proofview.Goal.enter begin fun gl ->
+        let env = Tacmach.New.pf_env gl in
+        let sigma = Proofview.Goal.sigma gl in
+        let l = interp_hyp_list ist env sigma l in
+        if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l)
+        else
+          (* spiwack: until the tactic is in the monad *)
+          let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in
+          Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac
       end
   | TacClearBody l ->
       Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c600a86cb4..e4783707ac 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1833,9 +1833,10 @@ let specialize (c,lbind) g =
 
 (* Keeping only a few hypotheses *)
 
-let keep hyps gl =
-  let env = Global.env() in
-  let ccl = pf_concl gl in
+let keep hyps =
+  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.tclENV >>= fun env ->
+  let ccl = Proofview.Goal.concl gl in
   let cl,_ =
     fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if Id.List.mem hyp hyps
@@ -1843,8 +1844,10 @@ let keep hyps gl =
 	|| occur_var env hyp ccl
       then (clear,decl::keep)
       else (hyp::clear,keep))
-      ~init:([],[]) (pf_env gl)
-  in thin cl gl
+      ~init:([],[]) (Proofview.Goal.env gl)
+  in
+  Proofview.V82.tactic (fun gl -> thin cl gl)
+  end
 
 (************************)
 (* Introduction tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 75b1fe7044..7a6464547c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -165,7 +165,7 @@ val unfold_constr     : global_reference -> tactic
 val clear         : Id.t list -> tactic
 val clear_body    : Id.t list -> unit Proofview.tactic
 val unfold_body   : Id.t -> tactic
-val keep          : Id.t list -> tactic
+val keep          : Id.t list -> unit Proofview.tactic
 val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
 val specialize    : constr with_bindings -> tactic