From c5d686f2abee4f7d6376cfbdbc2d49c42c423c17 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 16 Apr 2006 15:51:02 +0000 Subject: 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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8723 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/global.mli | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'library/global.mli') 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 *) -- cgit v1.2.3