diff options
| author | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
| commit | 6a48e732577b9ab09d458c7526f599d4528fe2fc (patch) | |
| tree | 66cf1df2a49a7ee2470d13dd46b3ee917cdc00e3 /printing | |
| parent | 5ced288419aed8a622ed2c267e35d9a174facafc (diff) | |
| parent | 39a10cba3d610c6f12438084c5de7c1217c8fe94 (diff) | |
Merge PR #8534: Checking if low-level name printers are used on purpose or not
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 67d71332b0..5ca330d377 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -944,9 +944,16 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> + (* FIXME? *) let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in + let safe_pr_inductive env kn = + try pr_inductive env (kn,0) + with Not_found -> + (* FIXME? *) + MutInd.print kn + in let safe_pr_ltype env sigma typ = try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () @@ -961,7 +968,7 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") | Guarded kn -> hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in |