Lazyconstr -> Opaqueproof

Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 6e656fad9..6c0f1b060 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,11 +80,11 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	  let cst = cb.const_constraints +++ cst1 +++ cst2 in
 	  j.uj_val, cst
 	| Def cs ->
-	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
+	  let cst1 = Reduction.conv env' c (Mod_subst.force_constr cs) in
 	  let cst = cb.const_constraints +++ cst1 in
           c, cst
       in
-      let def = Def (Lazyconstr.from_val c') in
+      let def = Def (Mod_subst.from_val c') in
       let cb' =
 	{ cb with
 	  const_body = def;