diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-04 10:28:55 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-04 10:28:55 +0000 |
| commit | 7cffdbf4f4106950ba958d6f45fc16106069c9f7 (patch) | |
| tree | 572ff87d59b89a1eea82ff4909b7c985d98254bb /library | |
| parent | 408a1d674962625dfa90d45bc17f319d3e43c7ff (diff) | |
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 11 | ||||
| -rw-r--r-- | library/declare.mli | 4 |
2 files changed, 10 insertions, 5 deletions
diff --git a/library/declare.ml b/library/declare.ml index 4c68617c2..f86edc915 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 78f19e68f..38a14c010 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 |