diff options
| -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 |