From dc8750d166cffd846619d2de20e02a4e31c6357f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 18:10:36 +0200
Subject: Put the "exact_constr" tactic in the monad.

---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0e5cef828b..23755dac1d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -504,7 +504,7 @@ let vernac_end_proof ?proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-  let status = by (Tactics.New.exact_proof c) in
+  let status = by (Tactics.exact_proof c) in
   save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Pp.feedback Feedback.AddedAxiom
 
-- 
cgit v1.2.3