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.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 'library/global.mli')
| -rw-r--r-- | library/global.mli | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/library/global.mli b/library/global.mli index af6ec6ae9..6842a44eb 100644 --- a/library/global.mli +++ b/library/global.mli @@ -63,18 +63,13 @@ val set_engagement : engagement -> unit (* [start_*] functions return the [module_path] valid for components of the started module / module type *) -val start_module : - identifier -> (mod_bound_id * module_type_entry) list -> module_path +val start_module : identifier -> module_path +val end_module : identifier -> module_type_entry option -> module_path -val end_module : - identifier -> module_type_entry option -> module_path +val add_module_parameter : mod_bound_id -> module_type_entry -> unit -val start_modtype : - identifier -> (mod_bound_id * module_type_entry) list - -> module_path - -val end_modtype : - identifier -> kernel_name +val start_modtype : identifier -> module_path +val end_modtype : identifier -> kernel_name (* Queries *) |