aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-12 22:27:49 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-12 22:27:49 +0000
commitbef7efb2c9c398e7f9fd7e38ece6f5a3c99461f3 (patch)
tree539618ba7dfd91d45c462acf072ca88c7b717fb9 /tactics/equality.ml
parent9d3bc8da6655f0a2d207014a38a0c7a1cf8a1788 (diff)
Removed what looks like a (very old) useless f.o. unification pass
made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
0 files changed, 0 insertions, 0 deletions