nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 00e6d66f6a..2613199ffd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -310,6 +310,16 @@ let evaluable_constant env k =
   with Not_found -> 
     false
 
+(*s Opaque / Transparent switching *)
+
+let set_opaque env sp =
+  let cb = lookup_constant sp env in
+  cb.const_opaque <- true
+
+let set_transparent env sp =
+  let cb = lookup_constant sp env in
+  cb.const_opaque <- false
+
 (*s Modules (i.e. compiled environments). *)
 
 type compiled_env = {