diff options
author | 2001-12-13 09:03:13 +0000 | |
---|---|---|
committer | 2001-12-13 09:03:13 +0000 | |
commit | 78d1c75322684eaa7e0ef753ee56d9c6140ec830 (patch) | |
tree | 3ec7474493dc988732fdc9fe9d637b8de8279798 /contrib/correctness/prename.ml | |
parent | f813d54ada801c2162491267c3b236ad181ee5a3 (diff) |
compat ocaml 3.03
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/prename.ml')
-rw-r--r-- | contrib/correctness/prename.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml index 122ff16ab..aa068f19c 100644 --- a/contrib/correctness/prename.ml +++ b/contrib/correctness/prename.ml @@ -111,8 +111,8 @@ let var_at_date r d id = find (until d r) id with Not_found -> raise (UserError ("Renamings.var_at_date", - hOV 0 [< 'sTR"Variable "; pr_id id; 'sTR" is unknown"; 'sPC; - 'sTR"at date "; 'sTR d >])) + hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++ + str"at date " ++ str d))) let vars_at_date r d ids = let r' = until d r in List.map (fun id -> id,find r' id) ids @@ -125,15 +125,15 @@ open Util open Himsg let pp r = - hOV 2 (prlist_with_sep (fun () -> [< 'fNL >]) + hov 2 (prlist_with_sep (fun () -> (fnl ())) (fun (d,l) -> - [< 'sTR d; 'sTR": "; - prlist_with_sep (fun () -> [< 'sPC >]) + (str d ++ str": " ++ + prlist_with_sep (fun () -> (spc ())) (fun (id,id') -> - [< 'sTR"("; pr_id id; 'sTR","; pr_id id'; 'sTR")" >]) - l >]) + (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")")) + l)) r.levels) let ppr e = - pP (pp e) + Pp.pp (pp e) |