diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-18 14:58:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-18 14:58:14 +0000 |
| commit | b4b1a1498463e8f9f32b88979781d281869fb0d4 (patch) | |
| tree | e14164db85a56486314607ceb57999a861182e09 /library/global.ml | |
| parent | bedaec8452d0600ede52efeeac016c9d323c66de (diff) | |
Renommage canonique :
declaration = definition | assumption
mode de reference = named | rel
Ex:
push_named_decl : named_declaration -> env -> env
lookup_named : identifier -> safe_environment -> constr option * typed_type
add_named_assum : identifier * typed_type -> named_context -> named_context
add_named_def : identifier*constr*typed_type -> named_context -> named_context
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@724 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/library/global.ml b/library/global.ml index 96fb689a3..52ea32986 100644 --- a/library/global.ml +++ b/library/global.ml @@ -28,22 +28,19 @@ let _ = let universes () = universes !global_env let context () = context !global_env -let var_context () = var_context !global_env +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 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 let add_constraints c = global_env := add_constraints c !global_env -let pop_vars ids = global_env := pop_vars ids !global_env +let pop_named_decls ids = global_env := pop_named_decls ids !global_env -let lookup_var id = lookup_var id !global_env +let lookup_named id = lookup_named id !global_env (* let lookup_rel n = lookup_rel n !global_env *) |