diff options
| author | sacerdot | 2005-01-13 14:28:56 +0000 |
|---|---|---|
| committer | sacerdot | 2005-01-13 14:28:56 +0000 |
| commit | 0224b036502016e9bd4e8b683af458248fdac4a9 (patch) | |
| tree | 6edb63dd6839906dc95c1c1c5ef29a25e1c67673 /translate | |
| parent | 204ca2560751eaa0fc00f6d5235fc81236855f1b (diff) | |
Construct "T with (Definition|Module) id := c" generalized to
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 4b47b8d0aa..f052310b70 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -36,6 +36,18 @@ let pr_lident (b,_ as loc,id) = pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) else pr_id id +let string_of_fqid fqid = + String.concat "." (List.map string_of_id fqid) + +let pr_fqid fqid = str (string_of_fqid fqid) + +let pr_lfqid (_,_ as loc,fqid) = + if loc <> dummy_loc then + let (b,_) = unloc loc in + pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) + else + pr_fqid fqid + let pr_lname = function (loc,Name id) -> pr_lident (loc,id) | lna -> pr_located pr_name lna @@ -229,9 +241,9 @@ let pr_hints local db h pr_c pr_pat = let pr_with_declaration pr_c = function | CWith_Definition (id,c) -> let p = pr_c c in - str"Definition" ++ spc() ++ pr_lident id ++ str" := " ++ p + str"Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p | CWith_Module (id,qid) -> - str"Module" ++ spc() ++ pr_lident id ++ str" := " ++ + str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid let rec pr_module_type pr_c = function |