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 /kernel/safe_typing.mli | |
| 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 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 43755b908..1b4d932b5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -72,17 +72,17 @@ val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) val start_module : - label -> (mod_bound_id * module_type_entry) list - -> safe_environment -> module_path * safe_environment + label -> safe_environment -> module_path * safe_environment val end_module : label -> module_type_entry option -> safe_environment -> module_path * safe_environment +val add_module_parameter : + mod_bound_id -> module_type_entry -> safe_environment -> safe_environment val start_modtype : - label -> (mod_bound_id * module_type_entry) list - -> safe_environment -> module_path * safe_environment + label -> safe_environment -> module_path * safe_environment val end_modtype : label -> safe_environment -> kernel_name * safe_environment |