aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check_stat.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-28 00:02:32 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-28 00:05:53 +0200
commite5fe4569f3eaeaa4e1ce377989e19f1f2c176da9 (patch)
tree3edd23e7326b0240feb82c24393e617ba684342c /checker/check_stat.ml
parentcd139311ecd872301077b9db2df812a828ce2e77 (diff)
An example for cd139311e, showing a consequence of not converting
constants up to their canonical name (taken from Daniel's formalization of Puiseux theorem).
Diffstat (limited to 'checker/check_stat.ml')
0 files changed, 0 insertions, 0 deletions