aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview_monad.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-22 17:38:06 +0200
committerThéo Zimmermann2019-05-22 17:38:06 +0200
commit049cfe725d334fb863df31ee9e03db4b54a64455 (patch)
tree2149121e604d2b369eb001289bf64adf508afc21 /engine/proofview_monad.ml
parented7d118e8ee9a6725daafde31845981f5da8d2b4 (diff)
parent0001b6d108c2d2c058b0bfca7e0af888c026fe05 (diff)
Merge PR #10203: Fixing typos - Part 1
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: gares Reviewed-by: jfehrle Reviewed-by: vbgl
Diffstat (limited to 'engine/proofview_monad.ml')
-rw-r--r--engine/proofview_monad.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 80eb9d0124..8ed75a8d00 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -252,7 +252,7 @@ module Giveup : Writer with type t = goal list = struct
let put gs = Logical.put (true, gs)
end
-(** Lens and utilies pertaining to the info trace *)
+(** Lens and utilities pertaining to the info trace *)
module InfoL = struct
let recording = Logical.(map (fun {P.trace} -> trace) current)
let if_recording t =