aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-28 09:52:18 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-28 09:52:18 +0100
commit5a540c372648493575461a298e04b9fa716661ad (patch)
treea5c6a9b455b93841dc0960b8b0c1e78865c96b1a /dev
parentac006d8c87a7e921ed5a106aeba264bd6c8caa6c (diff)
parent3cc45d57f6001d8c377825b9b940bc51fb3a96f7 (diff)
Merge PR #6248: [api] Remove aliases of `Evar.t`
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml5
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)^")"