diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-30 18:58:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-30 18:58:57 +0100 |
| commit | d5d15af811a487e65f8c10dfb68d5608f3722f8a (patch) | |
| tree | c4b715bff21c6bb78f950b0452bfcc2945b33062 /dev/db | |
| parent | a01a60b366307da3eca63c9937984db6f273dc41 (diff) | |
Adding printing of ltac envs to debugger.
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -39,3 +39,4 @@ install_printer Top_printers.prsubst install_printer Top_printers.prdelta install_printer Top_printers.ppfconstr install_printer Top_printers.ppgenarginfo +install_printer Top_printers.ppist |