diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-09 15:01:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-09 15:01:54 +0000 |
| commit | 1e4c9c6dd74162c5fd75de59f1cab117e458e8de (patch) | |
| tree | 77dc73065ba7879147af5372482a745f7ce07cae /library/global.ml | |
| parent | 984e59594c751b842a26d251ed312819e6e9641c (diff) | |
Mécanisme pour faire remonter les contraintes de typage sur les variables de section au niveau du discharge, sans avoir à garder tout l'environnement de la section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index ea5506969..9dc5cdcd7 100644 --- a/library/global.ml +++ b/library/global.ml @@ -39,8 +39,13 @@ let universes () = universes !global_env let context () = 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_named_def idc = + let d, env = check_and_push_named_def idc !global_env in + global_env := env; d + +let push_named_assum idc = + let d, env = check_and_push_named_assum idc !global_env in + global_env := env; d let add_parameter sp c l = global_env := add_parameter sp c l !global_env let add_constant sp ce l = global_env := add_constant sp ce l !global_env |