From 15b6c9b6fa268a9af6dd4f05961e469545e92a6f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 24 Feb 2014 20:46:32 +0100
Subject: Lazyconstr -> Opaqueproof

Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
---
 dev/printers.mllib  | 2 +-
 dev/top_printers.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index aedd09560d..6415a1a781 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -58,7 +58,7 @@ Copcodes
 Cemitcodes
 Nativevalues
 Future
-Lazyconstr
+Opaqueproof
 Declareops
 Retroknowledge
 Conv_oracle
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 82155a3058..eefd07e605 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -58,7 +58,7 @@ let ppevar evk = pp (str (Evd.string_of_existential evk))
 let ppconstr x = pp (Termops.print_constr x)
 let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
-let ppsconstr x = ppconstr (Lazyconstr.force x)
+let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
-- 
cgit v1.2.3