diff options
author | 2001-08-10 14:42:22 +0000 | |
---|---|---|
committer | 2001-08-10 14:42:22 +0000 | |
commit | 8e92ee787e7d1fd48cae1eccf67a9b05e739743e (patch) | |
tree | b33191fbaba0cad4b14a96cf5d7786dd2c07c3d7 /toplevel/coqtop.ml | |
parent | c0a3b41ad2f2afba3f060e0d4001bd7aceea0831 (diff) |
Parsing
- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
lieu de string)
Table des noms qualifiés
- Remplacement de la table de visibilité par une table qui ne cache
plus les noms de modules et sections mais seulement les noms des
constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
module A déjà existant : seuls les noms de constructions de l'ancien
A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
constantes définies à l'intérieur de sections et simplification
connexes (suppression de END-SECTION, une seule table de noms qui ne
survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
Require and co, tests de cohérence; pour être cohérent avec la non
survie des tables de noms à la sortie des section, les require à
l'intérieur d'une section eux aussi sont refaits à la fermeture de la
section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r-- | toplevel/coqtop.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a88223925..7d293aed9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -12,6 +12,7 @@ open Pp open Util open System open Options +open Names open States open Toplevel open Coqinit @@ -44,10 +45,10 @@ let outputstate = ref "" let set_outputstate s = outputstate:=s let outputstate () = if !outputstate <> "" then extern_state !outputstate -let set_include d p = push_include (d,Names.dirpath_of_string p) -let set_rec_include d p = push_rec_include (d,Names.dirpath_of_string p) -let set_default_include d = set_include d Nametab.default_root -let set_default_rec_include d = set_rec_include d Nametab.default_root +let set_include d p = push_include (d,p) +let set_rec_include d p = push_rec_include (d,p) +let set_default_include d = set_include d Nametab.default_root_prefix +let set_default_rec_include d = set_rec_include d Nametab.default_root_prefix let load_vernacular_list = ref ([] : string list) let add_load_vernacular s = @@ -60,15 +61,15 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter - (fun s -> Library.load_module (Filename.basename s) (Some s)) - (List.rev !load_vernacular_obj) + List.iter Library.read_module_from_file (List.rev !load_vernacular_obj) let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = List.iter - (fun s -> Library.require_module None (Filename.basename s) (Some s) false) + (fun s -> + let qid = Nametab.make_qualid [] (id_of_string (Filename.basename s)) in + Library.require_module None qid (Some s) false) (List.rev !require_list) (* Re-exec Coq in bytecode or native code if necessary. [s] is either @@ -110,7 +111,7 @@ let parse_args () = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p; parse rem + | "-R" :: d :: p :: rem ->set_rec_include d (dirpath_of_string p);parse rem | "-R" :: ([] | [_]) -> usage () | "-q" :: rem -> no_load_rc (); parse rem |