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 | |
| 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
| -rw-r--r-- | printing/printer.ml | 7 | ||||
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 2 |
2 files changed, 5 insertions, 4 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 diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ba316ceb64..b8db52735d 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,7 +7,7 @@ bli : Type Axioms: bli : Type Axioms: -@seq relies on definitional UIP. +seq relies on definitional UIP. Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g |