diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-08 00:58:56 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-08 01:44:10 +0200 |
commit | b5420538da04984ca42eb4284a9be27f3b5ba021 (patch) | |
tree | aef40fc7c5b541e47a15e62488ca617b96012f78 /plugins/cc/ccalgo.ml | |
parent | 1f6a31d138bcfcf341f28772de7c5e08906167c5 (diff) |
Fixing printing of toplevel values.
This is not perfect yet, in particular the whole precedence system is a real
mess, as there is a real need for tidying up the Pptactic implementation.
Nonetheless, printing toplevel values is only used for debugging purposes, where
an ugly display is better than none at all.
Diffstat (limited to 'plugins/cc/ccalgo.ml')
0 files changed, 0 insertions, 0 deletions