aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.mli')
-rw-r--r--proofs/proofview.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a32ceb59ec..914af982d6 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -404,7 +404,7 @@ end
(* The [NonLogical] module allows the execution of side effects in tactics
(non-logical side-effects are not discarded at failures). *)
-module NonLogical : module type of Proofview_monad.NonLogical
+module NonLogical : module type of Logic_monad.NonLogical
(* [tclLIFT c] includes the non-logical command [c] in a tactic. *)
val tclLIFT : 'a NonLogical.t -> 'a tactic