diff options
| author | Emilio Jesus Gallego Arias | 2017-12-29 20:20:38 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-26 16:33:48 +0200 |
| commit | 7628af7af9ff20d2a894673f66c3753e214623f1 (patch) | |
| tree | bb4c10fea3e44e6949a00d591234cecfc3f345ee /pretyping/inductiveops.ml | |
| parent | f49928874b51458fb67e89618bb350ae2f3529e4 (diff) | |
[print] Restrict use of "debug" Termops printer.
The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.
We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b040e63cd2..0fa573b9a6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches = not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ print_constr_env env sigma (mkInd ind)) + str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in |