aboutsummaryrefslogtreecommitdiff
path: root/engine/ftactic.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-12-06 04:44:27 +0100
committerEmilio Jesus Gallego Arias2018-12-09 02:54:02 +0100
commitd00472c59d15259b486868c5ccdb50b6e602a548 (patch)
tree008d862e4308ac8ed94cfbcd94ac26c739b89642 /engine/ftactic.ml
parentfa20a54d9fbe0f3872614a592fcef7ef56b05e49 (diff)
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
Diffstat (limited to 'engine/ftactic.ml')
-rw-r--r--engine/ftactic.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index b371884ba4..ac0344148a 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,8 +29,8 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
| Depends l ->
let f arg = f arg >>= function
| Uniform x ->
- (** We dispatch the uniform result on each goal under focus, as we know
- that the [m] argument was actually dependent. *)
+ (* We dispatch the uniform result on each goal under focus, as we know
+ that the [m] argument was actually dependent. *)
Proofview.Goal.goals >>= fun goals ->
let ans = List.map (fun g -> (g,x)) goals in
Proofview.tclUNIT ans