diff options
| author | Hugo Herbelin | 2020-07-12 20:37:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-15 21:48:25 +0200 |
| commit | a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e (patch) | |
| tree | 4fccdec595b66741023dc88c040a10446e7031e9 /printing/printer.ml | |
| parent | 33e748514dad9459885006a1523d107d556be22b (diff) | |
Do not print global refs as terms when asked to be printed as themselves.
This was already the case for constant, but not for constructors and
inductive types.
For instance, in message "The constructor @cons (in type list) is
expected to ..." we don't want a @ to be printed.
Diffstat (limited to 'printing/printer.ml')
| -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 |