aboutsummaryrefslogtreecommitdiffhomepage
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 4472bbcb7..234c3fff9 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -451,7 +451,7 @@ module Refine : sig
end
-(* The [NonLogical] module allows to execute side effects in tactics
+(* The [NonLogical] module allows the execution of side effects in tactics
(non-logical side-effects are not discarded at failures). *)
module NonLogical : sig