aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-07 20:55:31 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-07 20:55:31 +0000
commit8e4b7319caa0754401c8b868e9ce9490a867d7f1 (patch)
treeefbb3e085ff7f28dc8310bc906189846f69cf32d /kernel/vconv.ml
parenta5808860fbabd1239d1116c2f4413d56ff99620f (diff)
Reverted commit r13893 about propagation of more informative
unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/vconv.ml')
0 files changed, 0 insertions, 0 deletions