From 7cffdbf4f4106950ba958d6f45fc16106069c9f7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 4 Dec 2000 10:28:55 +0000
Subject: caractere opaque des constantes repris en compte

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1045 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml  | 11 +++++++----
 library/declare.mli |  4 +++-
 2 files changed, 10 insertions(+), 5 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 4c68617c24..f86edc915d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -114,7 +114,9 @@ type constant_declaration_type =
   | ConstantEntry  of constant_entry
   | ConstantRecipe of Cooking.recipe
 
-type constant_declaration = constant_declaration_type * strength
+type opacity = bool
+
+type constant_declaration = constant_declaration_type * strength * opacity
 
 let csttab = ref (Spmap.empty : strength Spmap.t)
 
@@ -124,7 +126,7 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.init_function = (fun () -> csttab := Spmap.empty);
 	    Summary.survive_section = false }
 
-let cache_constant (sp,(cdt,stre)) =
+let cache_constant (sp,(cdt,stre,op)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
@@ -133,9 +135,10 @@ let cache_constant (sp,(cdt,stre)) =
     | ConstantRecipe r -> Global.add_discharged_constant sp r
   end;
   Nametab.push sp (ConstRef sp);
+  if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
-let load_constant (sp,(ce,stre)) =
+let load_constant (sp,(ce,stre,op)) =
   csttab := Spmap.add sp stre !csttab
 
 let open_constant (sp,_) = ()
@@ -437,7 +440,7 @@ let declare_eliminations sp i =
   let declare na c =
     declare_constant (id_of_string na)
       (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
-       NeverDischarge);
+       NeverDischarge,false);
     if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
diff --git a/library/declare.mli b/library/declare.mli
index 78f19e68f8..38a14c0107 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,7 +34,9 @@ type constant_declaration_type =
   | ConstantEntry  of constant_entry
   | ConstantRecipe of Cooking.recipe
 
-type constant_declaration = constant_declaration_type * strength
+type opacity = bool
+
+type constant_declaration = constant_declaration_type * strength * opacity
 
 val declare_constant : identifier -> constant_declaration -> unit
 
-- 
cgit v1.2.3