diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-26 04:30:07 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-26 04:33:51 +0100 |
| commit | 3cc45d57f6001d8c377825b9b940bc51fb3a96f7 (patch) | |
| tree | ffd95829dd19c019811e82f6c849213920849ff3 /dev/top_printers.ml | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
[api] Remove aliases of `Evar.t`
There don't really bring anything, we also correct some minor nits
with the printing function.
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4e7b94e41..832040ad2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -18,7 +18,6 @@ open Univ open Environ open Printer open Constr -open Evd open Goptions open Genarg open Clenv @@ -62,7 +61,7 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) (* term printers *) let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma let rawdebug = ref false -let ppevar evk = pp (str (Evd.string_of_existential evk)) +let ppevar evk = pp (Evar.print evk) let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) @@ -263,7 +262,7 @@ let constr_display csr = "LetIn("^(name_display na)^","^(term_display b)^"," ^(term_display t)^","^(term_display c)^")" | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" - | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")" + | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")" | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")" | Ind ((sp,i),u) -> "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")" |