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 /checker/mod_checking.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 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index b83fe831bb..086dd17e39 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -10,10 +10,10 @@ open Environ let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); - (** Locally set the oracle for further typechecking *) + (* Locally set the oracle for further typechecking *) let oracle = env.env_typing_flags.conv_oracle in let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in - (** [env'] contains De Bruijn universe variables *) + (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env @@ -40,7 +40,7 @@ let check_constant_declaration env kn cb = if poly then add_constant kn cb env else add_constant kn cb env' in - (** Reset the value of the oracle *) + (* Reset the value of the oracle *) Environ.set_oracle env oracle (** {6 Checking modules } *) |