aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authormsozeau2008-03-18 11:22:13 +0000
committermsozeau2008-03-18 11:22:13 +0000
commitd4685a5bdaf15c31ddc616777b05280ec7570d08 (patch)
tree1349f628eb8cb3dcfbaf9d5d78bce185f10a8f39 /dev
parent99541c1123793d1c6352d1326c40426024b55948 (diff)
Correct implementation of normalization of signatures using setoid
rewriting, in some sense bootstrapping the system. Remove redundant morphisms for now to test for completeness (small performance penalty). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10689 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions