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 /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 2bbda279bd..83f1f8d8e9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -605,12 +605,12 @@ let print_evar_constraints gl sigma = let t1 = Evarutil.nf_evar sigma t1 and t2 = Evarutil.nf_evar sigma t2 in let env = - (** We currently allow evar instances to refer to anonymous de Bruijn - indices, so we protect the error printing code in this case by giving - names to every de Bruijn variable in the rel_context of the conversion - problem. MS: we should rather stop depending on anonymous variables, they - can be used to indicate independency. Also, this depends on a strategy for - naming/renaming *) + (* We currently allow evar instances to refer to anonymous de Bruijn + indices, so we protect the error printing code in this case by giving + names to every de Bruijn variable in the rel_context of the conversion + problem. MS: we should rather stop depending on anonymous variables, they + can be used to indicate independency. Also, this depends on a strategy for + naming/renaming *) Namegen.make_all_name_different env sigma in str" " ++ hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ @@ -686,7 +686,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | None -> GoalMap.empty in - (** Printing functions for the extra informations. *) + (* Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a | b::l -> Pp.int a ++ str"-" ++ print_stack b l @@ -753,7 +753,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | None -> () in - (** Main function *) + (* Main function *) match goals with | [] -> begin |