diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-28 09:52:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-28 09:52:18 +0100 |
| commit | 5a540c372648493575461a298e04b9fa716661ad (patch) | |
| tree | a5c6a9b455b93841dc0960b8b0c1e78865c96b1a /dev | |
| parent | ac006d8c87a7e921ed5a106aeba264bd6c8caa6c (diff) | |
| parent | 3cc45d57f6001d8c377825b9b940bc51fb3a96f7 (diff) | |
Merge PR #6248: [api] Remove aliases of `Evar.t`
Diffstat (limited to 'dev')
| -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)^")" |