diff options
| author | Gaëtan Gilbert | 2020-07-20 10:46:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-20 10:46:17 +0200 |
| commit | d6aff7758936e4028614a1ac7e1dfbc5c7f82076 (patch) | |
| tree | c4439ad667aab9dd6418af1ab81c8b31f97670f6 /printing | |
| parent | e9061bb414dfebad5bdf2efe634030563f8a2381 (diff) | |
| parent | a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e (diff) | |
Merge PR #12684: Do not print constructor and inductive types as terms when asked to be printed as themselves
Reviewed-by: SkySkimmer
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index f8413f3588..c5cb6ffad8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -257,11 +257,12 @@ let pr_puniverses f env sigma (c,u) = then f env c ++ pr_universe_instance sigma u else f env c -let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) -let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind) -let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr) + +let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) +let pr_inductive env ind = pr_global_env (Termops.vars_of_env env) (GlobRef.IndRef ind) +let pr_constructor env cstr = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstructRef cstr) let pr_pconstant = pr_puniverses pr_constant let pr_pinductive = pr_puniverses pr_inductive |