aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretype_errors.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-23 20:38:44 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-25 13:20:54 +0200
commitb39465da31bfd488dfad4ea4627186f9a1843e56 (patch)
treeecb154c909121d3e2eccf5885bd4b22d817a8866 /pretyping/pretype_errors.mli
parent9973cd2ca529076388710e90f2c46180581397cf (diff)
VarInstance are also goals.
Diffstat (limited to 'pretyping/pretype_errors.mli')
0 files changed, 0 insertions, 0 deletions