diff options
| author | William Lawvere | 2017-07-01 22:10:46 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-07-01 22:10:46 -0700 |
| commit | 80649ebaba75838bfd28ae78822cd2c078da4b23 (patch) | |
| tree | ac29ab5edd3921dbee1c2256737347fd1542dc67 /printing/printer.ml | |
| parent | c2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff) | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 3c31dd96bf..3b0b6d5d23 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -17,7 +17,6 @@ open Nametab open Evd open Proof_type open Refiner -open Pfedit open Constrextern open Ppconstr open Declarations @@ -262,6 +261,14 @@ let pr_universe_ctx sigma c = else mt() +let pr_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + else + mt() + (**********************************************************************) (* Global references *) @@ -812,7 +819,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = end let pr_nth_open_subgoal n = - let pf = get_pftreestate () in + let pf = Proof_global.give_me_the_proof () in let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in pr_subgoal n sigma gls @@ -992,6 +999,11 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) +let pr_cumulative poly cum = + if poly then + if cum then str "Cumulative " else str "NonCumulative " + else mt () + let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then |