diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-26 19:00:46 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-11 14:58:25 +0100 |
| commit | 34f63d7d890921cce37f4d48f48cdb020f2ac988 (patch) | |
| tree | 68c9756827be70d060f6ec597b21492117da1249 /printing/prettyp.ml | |
| parent | a77f3a3e076e273af35ad520cae2eef0e3552811 (diff) | |
[proof] Embed evar_map in RefinerError exception.
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1eb2c31c8..647111bbe 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -903,18 +903,16 @@ let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path ((i,j),p) = - let sigma, env = Pfedit.get_current_context () in +let print_path env sigma ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) +let print_graph env sigma = + prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) @@ -929,7 +927,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between env sigma cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -940,7 +938,7 @@ let print_path_between cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path env sigma ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl |