aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authormsozeau2008-02-09 10:59:29 +0000
committermsozeau2008-02-09 10:59:29 +0000
commit667de252676eb051fc4e056234f505ebafc335ca (patch)
tree6d1470c9f35ff2e13d0de3b24a5ed4e75d97e168 /dev
parent009fc6e9d0c92852f3a02ff66876875b9384d41a (diff)
Fix the clrewrite tactic, change Relations.v to work on relations in Prop
only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions