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 /interp/notation_term.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 'interp/notation_term.ml')
| -rw-r--r-- | interp/notation_term.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5fb0ca1b43..0ef1f267f6 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -20,13 +20,13 @@ open Glob_term as well as non global expressions such as existential variables. *) type notation_constr = - (** Part common to [glob_constr] and [cases_pattern] *) + (* Part common to [glob_constr] and [cases_pattern] *) | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - (** Part only in [glob_constr] *) + (* Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool |