diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-02 17:17:42 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-02 17:17:42 +0000 |
| commit | 12965209478bd99dfbe57f07d5b525e51b903f22 (patch) | |
| tree | 36a7f5e4802cd321caf02fed0be8349100be09fb /parsing/q_coqast.ml4 | |
| parent | 8b26fd6ba739d4f49fae99ed764b086022e44b50 (diff) | |
Modules dans COQ\!\!\!\!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index debe3ba93..6b7eb89a3 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,6 +8,8 @@ (* $Id$ *) +open Names +open Libnames open Q_util let dummy_loc = (0,0) @@ -71,13 +73,13 @@ let rec mlexpr_of_ast = function | Coqast.Num loc i -> <:expr< Coqast.Num loc $int:string_of_int i$ >> | Coqast.Id loc id -> <:expr< Coqast.Id loc $str:id$ >> | Coqast.Str loc str -> <:expr< Coqast.Str loc $str:str$ >> - | Coqast.Path loc qid -> - let l,a = Names.repr_path qid in + | Coqast.Path loc kn -> + let l,a = Libnames.decode_kn kn in let mlexpr_of_modid id = - <:expr< Names.id_of_string $str:Names.string_of_id id$ >> in - let e = List.map mlexpr_of_modid (Names.repr_dirpath l) in + <:expr< Names.id_of_string $str:string_of_id id$ >> in + let e = List.map mlexpr_of_modid (repr_dirpath l) in let e = expr_list_of_var_list e in - <:expr< Coqast.Path loc (Names.make_path (Names.make_dirpath $e$) + <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$) (Names.id_of_string $str:Names.string_of_id a$)) >> | Coqast.Dynamic _ _ -> failwith "Q_Coqast: dynamic: not implemented" @@ -121,8 +123,8 @@ let mlexpr_of_dirpath dir = <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >> let mlexpr_of_qualid qid = - let (dir, id) = Nametab.repr_qualid qid in - <:expr< Nametab.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> + let (dir, id) = repr_qualid qid in + <:expr< make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> let mlexpr_of_reference = function | Tacexpr.RQualid (loc,qid) -> <:expr< Tacexpr.RQualid loc $mlexpr_of_qualid qid$ >> |