aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-10 15:16:11 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-10 15:16:11 +0000
commit43582a9c7ac7e5f2311c8ce52d8107553b2c9673 (patch)
tree53a12a10bb3054c0a6967bc87a8eac3ed2f38e18 /theories/Sorting
parent899d186714a2bcb2d51902c918d0cb20d1815288 (diff)
Better treatment of error messages in rewrite (avoid use of Errors.print).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15583 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sorting')
0 files changed, 0 insertions, 0 deletions