diff options
author | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-10-30 22:31:27 +0100 |
---|---|---|
committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:35 +0100 |
commit | 2656c62e9be7a856f12c0da0740869d193273c4d (patch) | |
tree | 96792a9ccb608e795857f784bc6373eebfd4635c /plugins/micromega/Env.v | |
parent | 0aa24d51d2606549da87ed42085f612f2dbb1428 (diff) |
Ppannotation: New.
Define the annotations stored in semi-structured pretty-prints.
Ppconstrsig: New.
Contains the signature of a pretty-printer for ppconstr.
Ppconstr: Export a new rich pretty-printer for constr_expr and co.
Diffstat (limited to 'plugins/micromega/Env.v')
0 files changed, 0 insertions, 0 deletions