diff options
| author | Hugo Herbelin | 2014-12-24 09:43:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-30 15:57:45 +0100 |
| commit | ee0aeee014f1111781c0e616c3f72243a03df1ea (patch) | |
| tree | cf467ba336c0d73117a3b7b81e54ad6bbd2ddc52 /dev | |
| parent | e1644336b746797bc929e908df87c6391669005d (diff) | |
Compatibility ocaml 3.12.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ee33995cef..33660e495c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -118,13 +118,13 @@ let ppunbound_ltac_var_map l = ppidmap (fun _ arg -> open Glob_term -let rec pr_closure {idents;typed;untyped} = +let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++ str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++ str"untyped=" ++ pr_closed_glob_constr_idmap untyped ++ str"}") and pr_closed_glob_constr_idmap x = pridmap (fun _ -> pr_closed_glob_constr) x -and pr_closed_glob_constr {closure;term} = +and pr_closed_glob_constr {closure=closure;term=term} = pr_closure closure ++ pr_lglob_constr term let ppclosure x = pp (pr_closure x) |