aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authormsozeau2009-11-15 00:15:42 +0000
committermsozeau2009-11-15 00:15:42 +0000
commit77ba6079eef1099a34bfcff01fe36298392e3fdf (patch)
tree466868e3c5c3ffb57d32083ca2a51067e4926d09 /plugins
parent600e73d2522599fd600ab717410254565d57236b (diff)
Fix [Instance: forall ..., C args := t] declarations to behave as
expected, not introducing the [forall ...] variables to avoid unnecessary eta-expansions. Force to use { } in instance declarations when the class is a record even if it's a singleton. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12524 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions