aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-24 17:25:27 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-29 21:54:31 +0200
commitec49447d078da25959d617ae23e55a668fdd1646 (patch)
treefa36169808ba6bcd886f9fa6e333a569e218717c /interp/notation.ml
parent7eeda1b1ffd93311965aa431ea64f0fb38e3b34d (diff)
CoqIDE: new message to print AST
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions