diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-16 15:51:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-16 15:51:02 +0000 |
| commit | c5d686f2abee4f7d6376cfbdbc2d49c42c423c17 (patch) | |
| tree | d1d40416131888f1d8110225f817486dda537ad9 /library/global.ml | |
| parent | a6ef81988e1e4282cb2b7d6bf9a99576e032800d (diff) | |
Nouveau mécanisme pour les modules interactifs : les arguments de
foncteurs sont données un par un ce qui permet de faire les
load_objects correspondants au bon moment (càd juste après l'ajout des
déclarations logiques et avant l'ajout du paramètre suivant). Ceci
clôt le bug #1118 et corrige des erreurs de localisation introduite
par le commit précédent.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8723 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/library/global.ml b/library/global.ml index 6ad414339..19b416519 100644 --- a/library/global.ml +++ b/library/global.ml @@ -73,12 +73,12 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env -let start_module id params = +let start_module id = let l = label_of_id id in - let mp,newenv = start_module l params !global_env in + let mp,newenv = start_module l !global_env in global_env := newenv; mp - + let end_module id mtyo = let l = label_of_id id in let mp,newenv = end_module l mtyo !global_env in @@ -86,9 +86,14 @@ let end_module id mtyo = mp -let start_modtype id params = +let add_module_parameter mbid mte = + let newenv = add_module_parameter mbid mte !global_env in + global_env := newenv + + +let start_modtype id = let l = label_of_id id in - let mp,newenv = start_modtype l params !global_env in + let mp,newenv = start_modtype l !global_env in global_env := newenv; mp |