aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2009-04-09 10:13:28 +0000
committerherbelin2009-04-09 10:13:28 +0000
commit16ea6252339bed9901fff48b5883f4d471a88e7a (patch)
tree92278fec909264b6c5eb6160c10d26b9893990d4 /dev
parente2a8e020542e32b51ff5951d40bed3dad68c903d (diff)
Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use
Type instead of sort variables for unknown levels in unification). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12075 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions