diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-01 17:52:44 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 18:35:12 +0100 |
commit | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (patch) | |
tree | 94afab156f907e5576091fdebe4b227346440dba /dev | |
parent | 6b99de706e37c75407373e756e24f2256b848815 (diff) |
Introducing a new EConstr.t type to perform the nf_evar operation on demand.
Diffstat (limited to 'dev')
-rw-r--r-- | dev/db | 1 | ||||
-rw-r--r-- | dev/top_printers.ml | 1 |
2 files changed, 2 insertions, 0 deletions
@@ -28,6 +28,7 @@ install_printer Top_printers.pppattern install_printer Top_printers.ppglob_constr install_printer Top_printers.ppconstr +install_printer Top_printers.ppeconstr install_printer Top_printers.ppuni install_printer Top_printers.ppuniverses install_printer Top_printers.ppconstraints diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b552d9994..b7736f498 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -71,6 +71,7 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) let ppconstr x = pp (Termops.print_constr x) +let ppeconstr x = pp (Termops.print_constr (EConstr.Unsafe.to_constr x)) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr |