diff options
| author | Pierre-Marie Pédrot | 2018-11-19 08:12:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 733cb74a2038ff92156b7209713fc2ea741ccca6 (patch) | |
| tree | ee664936850ce6160d9e3fc3219b9dba7b7ea096 /printing | |
| parent | ad5aea737ecc639c31dda84322b3550a4d380b47 (diff) | |
Rename TranspState into TransparentState.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 4 | ||||
| -rw-r--r-- | printing/printer.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index b7c53c5513..dfe987a671 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -446,8 +446,8 @@ 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 ts = - hv 0 (str"VARIABLES: " ++ pr_idpred ts.TranspState.tr_var ++ fnl () ++ - str"CONSTANTS: " ++ pr_cpred ts.TranspState.tr_cst ++ fnl ()) + 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 fb4e790c10..cfa1caef00 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -134,7 +134,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 : TranspState.t -> Pp.t +val pr_transparent_state : TransparentState.t -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) |