index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
/
closed
/
bug_6951.v
blob: 419f8d7c4eaf586ebb690c0287f734f4571f8760 (
plain
)
1
2
Record
float2
:
Set
:=
Float2
{
Fnum
:
unit
}.
Scheme
Equality
for
float2
.