diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 04:44:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-09 02:54:02 +0100 |
| commit | d00472c59d15259b486868c5ccdb50b6e602a548 (patch) | |
| tree | 008d862e4308ac8ed94cfbcd94ac26c739b89642 /pretyping/reductionops.ml | |
| parent | fa20a54d9fbe0f3872614a592fcef7ef56b05e49 (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 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a57ee6e292..f8e8fa9eb9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -203,6 +203,7 @@ end (** Machinery about stack of unfolded constants *) module Cst_stack = struct open EConstr + (** constant * params * args - constant applied to params = term in head applied to args @@ -1342,7 +1343,7 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = - (** FIXME *) + (* FIXME *) try let ans = match pb with | Reduction.CUMUL -> @@ -1632,7 +1633,7 @@ let meta_reducible_instance evd b = in let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = - let u = whd_betaiota Evd.empty u (** FIXME *) in + let u = whd_betaiota Evd.empty u (* FIXME *) in match EConstr.kind evd u with | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in |