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/evarsolve.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/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4692fe0057..4c4a236620 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -80,7 +80,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if v' == v then t else mkProd (na, u, v') | _ -> t in - (** Refresh the types of evars under template polymorphic references *) + (* Refresh the types of evars under template polymorphic references *) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> @@ -1385,7 +1385,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = let occur_evar_upto_types sigma n c = let c = EConstr.Unsafe.to_constr c in let seen = ref Evar.Set.empty in - (** FIXME: Is that supposed to be evar-insensitive? *) + (* FIXME: Is that supposed to be evar-insensitive? *) let rec occur_rec c = match Constr.kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> @@ -1581,7 +1581,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = Id.Set.subset (collect_vars evd rhs) !names in let body = - if fast rhs then nf_evar evd rhs (** FIXME? *) + if fast rhs then nf_evar evd rhs (* FIXME? *) else let t' = imitate (env,0) rhs in if !progress then |