diff options
| author | herbelin | 2000-07-24 13:39:23 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-24 13:39:23 +0000 |
| commit | 3afaf3dde673d77cacaabc354f008dfbe49a7cee (patch) | |
| tree | 4264164faf763ab8d18274cd5aeffe5a1de21728 /library/global.ml | |
| parent | 83f038e61a4424fcf71aada9f97c91165b73aef8 (diff) | |
Passage à des contextes de vars et de rels pouvant contenir des déclarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index cf3d88ca93..a37863a78f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -30,8 +30,12 @@ let universes () = universes !global_env let context () = context !global_env let var_context () = var_context !global_env -let push_var idc = global_env := push_var idc !global_env -let push_rel nac = global_env := push_rel nac !global_env +let push_var_def idc = global_env := push_var_def idc !global_env +let push_var_decl idc = global_env := push_var_decl idc !global_env +(* +let push_rel_def nac = global_env := push_rel nac !global_env +let push_rel_decl nac = global_env := push_rel nac !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_mind sp mie = global_env := add_mind sp mie !global_env @@ -40,7 +44,9 @@ let add_constraints c = global_env := add_constraints c !global_env let pop_vars ids = global_env := pop_vars ids !global_env let lookup_var id = lookup_var 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 |