aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-08-07 12:15:30 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-08-07 12:15:30 +0000
commit2cbf0f8fe0929d36391a8f12e32873eb3a95d7cd (patch)
tree07099379e89777ef6e3934930afb7386284276f9 /test-suite/failure
parentfa87b9196df910caa4cb085f9dee69ca58df0c34 (diff)
Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain some minimal compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure')
0 files changed, 0 insertions, 0 deletions