From 15b6c9b6fa268a9af6dd4f05961e469545e92a6f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
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.
---
 kernel/kernel.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/kernel.mllib')

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 7d318add5..bcd366f1a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -12,7 +12,7 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
-Lazyconstr
+Opaqueproof
 Declareops
 Retroknowledge
 Conv_oracle
-- 
cgit v1.2.3