aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorbertot2001-04-07 08:43:02 +0000
committerbertot2001-04-07 08:43:02 +0000
commit2ec0991f0fef6b529a0d90d64f06aff1c8db91ab (patch)
treed27d471e35a635a8d783b496b557b30b75dd9784 /kernel/type_errors.mli
parentad228a6815329a1331d26caca7f6eaae0ddbd52b (diff)
Two constants had been given in the wrong package (Logic_type instead of
the correct Logic_Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1554 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions