aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-19 08:12:28 +0100
committerPierre-Marie Pédrot2018-11-19 13:29:55 +0100
commit733cb74a2038ff92156b7209713fc2ea741ccca6 (patch)
treeee664936850ce6160d9e3fc3219b9dba7b7ea096 /printing/printer.ml
parentad5aea737ecc639c31dda84322b3550a4d380b47 (diff)
Rename TranspState into TransparentState.
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml4
1 files changed, 2 insertions, 2 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