diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-06 16:43:51 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-06 16:43:51 +0000 |
| commit | 723c344d3e4cf7fdc2e4854ea7d55d140570424d (patch) | |
| tree | 41ae18d8e43aa80007d361e83414d3b043f693ee /library/global.ml | |
| parent | 826913ee19c25cfe445f574080524662bdba1597 (diff) | |
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
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/library/global.ml b/library/global.ml index 7b69ca0a8..6a2dfe145 100644 --- a/library/global.ml +++ b/library/global.ml @@ -33,21 +33,23 @@ let named_context () = named_context !global_env let push_named_def idc = global_env := push_named_def idc !global_env let push_named_assum idc = global_env := push_named_assum idc !global_env -let add_constant sp ce = global_env := add_constant sp ce !global_env let add_parameter sp c = global_env := add_parameter sp c !global_env +let add_constant sp ce = global_env := add_constant sp ce !global_env +let add_discharged_constant sp r = + global_env := add_discharged_constant sp r !global_env let add_mind sp mie = global_env := add_mind sp mie !global_env let add_constraints c = global_env := add_constraints c !global_env let pop_named_decls ids = global_env := pop_named_decls ids !global_env let lookup_named id = lookup_named id !global_env -(* -let lookup_rel n = lookup_rel n !global_env -*) let lookup_constant sp = lookup_constant sp !global_env let lookup_mind sp = lookup_mind sp !global_env let lookup_mind_specif c = lookup_mind_specif c !global_env +let set_opaque sp = set_opaque !global_env sp +let set_transparent sp = set_transparent !global_env sp + let export s = export !global_env s let import cenv = global_env := import cenv !global_env |