aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-17 11:26:31 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-17 11:26:31 +0100
commit35b88621408d13ae8e2a0247daa01d95d749161c (patch)
tree4ca59470b5003953be82b96539925309a3312a37 /proofs
parent9d2767d3b960a4790d01150941667e0dc62857fc (diff)
Moving printing code for red_expr and may_eval to Pptactic.
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions