Put the "exact" family of tactic in the monad.

10 files changed, 17 insertions, 20 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 98b77ab35..3849a8440 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -39,7 +39,7 @@ TACTIC EXTEND cut
 END
 
 TACTIC EXTEND exact_no_check
-  [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
 END
 
 TACTIC EXTEND vm_cast_no_check
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5e0153fce..7acdff9ac 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
-        Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma)
+        Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
       end }
       end
   | TacApply (a,ev,cb,cl) ->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f19cdd2cc..d05e9484a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -58,7 +58,7 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) exact_no_check
+  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
@@ -151,7 +151,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [pf_constr_of_global id exact_no_check;
+            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
 	     tclTHENLIST
 	       [pf_constr_of_global id (fun idc -> generalize [d idc]);
 		clear_global id;
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 2f3a3e551..73dc13e72 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -316,7 +316,7 @@ let rtauto_tac gls=
     if !check then
       Proofview.V82.of_tactic (Tactics.exact_check term) gls
     else
-      Tactics.exact_no_check term gls in
+      Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
   let tac_end_time = System.get_time () in
   let _ =
     if !check then msg_info (str "Proof term type-checking is on");
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 485559898..cfbcc4750 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -164,7 +164,7 @@ let e_give_exact flags poly (c,clenv) gl =
     else c, gl
   in
   let t1 = pf_unsafe_type_of gl c in
-    tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
+  Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6bbd9b2e8..f0f408c24 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -33,7 +33,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t2 = Tacmach.New.pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
-     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 33eb80c28..d59c2fba4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -84,7 +84,7 @@ let general_decompose recognizer c =
          (onLastHypId
 	    (ifOnHyp recognizer (general_decompose_aux recognizer)
 	      (fun id -> clear [id])));
-       Proofview.V82.tactic (exact_no_check c) ]
+       exact_no_check c ]
   end }
 
 let head_in indl t gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index eecc2b787..572d4b7ab 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1582,7 +1582,7 @@ let substClause l2r c cls =
   Proofview.Goal.enter { enter = begin fun gl ->
   let eq = pf_apply get_type_of gl c in
   tclTHENS (cutSubstClause l2r eq cls)
-    [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
+    [Proofview.tclUNIT (); exact_no_check c]
   end }
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 01af30049..6bf5831f7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1833,7 +1833,7 @@ let cut_and_apply c =
 (* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *)
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
-let new_exact_no_check c =
+let exact_no_check c =
   Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
 
 let exact_check c =
@@ -1845,13 +1845,11 @@ let exact_check c =
   let sigma = Sigma.to_evar_map sigma in
   let sigma, ct = Typing.type_of env sigma c in
   let tac =
-      Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
+      Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
   in
   Sigma.Unsafe.of_pair (tac, sigma)
   end }
 
-let exact_no_check = Tacmach.refine_no_check
-
 let vm_cast_no_check c gl =
   let concl = Tacmach.pf_concl gl in
   Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
@@ -2626,8 +2624,7 @@ let forward b usetac ipat c =
       Proofview.Goal.enter { enter = begin fun gl ->
       let t = Tacmach.New.pf_unsafe_type_of gl c in
       let hd = head_ident c in
-      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
-	(Proofview.V82.tactic (exact_no_check c))
+      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }
   | Some tac ->
       if b then
@@ -2820,14 +2817,14 @@ let specialize (c,lbind) =
         (Proofview.Unsafe.tclEVARS sigma)
 	(Tacticals.New.tclTHENFIRST
 	   (assert_before_replacing id typ)
-	   (new_exact_no_check term))
+	   (exact_no_check term))
   | _ ->
       (* To deprecate in favor of generalize? *)
       Tacticals.New.tclTHEN
         (Proofview.Unsafe.tclEVARS sigma)
 	(Tacticals.New.tclTHENLAST
            (cut typ)
-           (new_exact_no_check term))
+           (exact_no_check term))
   end }
 
 (*****************************)
@@ -3652,7 +3649,7 @@ let specialize_eqs id gl =
   let ty' = Evarutil.nf_evar !evars ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
-	(exact_no_check ((* refresh_universes_strict *) acc')) gl
+	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
     else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
 
 
@@ -4798,7 +4795,7 @@ let abstract_subproof id gk tac =
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
-    new_exact_no_check (applist (lem, args))
+    exact_no_check (applist (lem, args))
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
   Sigma.Unsafe.of_pair (tac, evd)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 47ff197a0..2ffedf81a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -114,7 +114,7 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic
 (** {6 Exact tactics. } *)
 
 val assumption       : unit Proofview.tactic
-val exact_no_check   : constr -> tactic
+val exact_no_check   : constr -> unit Proofview.tactic
 val vm_cast_no_check : constr -> tactic
 val native_cast_no_check : constr -> tactic
 val exact_check      : constr -> unit Proofview.tactic