diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 6 | ||||
| -rw-r--r-- | printing/printer.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 7ce08ed6bc..831008a957 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -456,9 +456,9 @@ let pr_predicate pr_elt (b, elts) = let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) -let pr_transparent_state (ids, csts) = - hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ - str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) +let pr_transparent_state ts = + hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++ + str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ()) (* display complete goal og_s has goal+sigma on the previous proof step for diffs diff --git a/printing/printer.mli b/printing/printer.mli index e50b02b508..785f452a7b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -135,7 +135,7 @@ val pr_context_of : env -> evar_map -> Pp.t val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t val pr_cpred : Cpred.t -> Pp.t val pr_idpred : Id.Pred.t -> Pp.t -val pr_transparent_state : transparent_state -> Pp.t +val pr_transparent_state : TransparentState.t -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) |