diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-29 12:30:25 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-29 12:30:25 +0000 |
commit | 73798a12d39b03e1823b93c1364a86d14e2eec0a (patch) | |
tree | 1095b79d71bdacfcf2acc311b9e4a3aa98f64d4c /interp/constrextern.mli | |
parent | ea24960e35ee39f8ed719583886f7b56587a879c (diff) |
Fix eauto still using delta when it shouldn't (should make CoRN compile
in reasonable time), add (unfinished) documentation on type classes.
Put some classes into Prop explicitely as singleton inductive types are
no longer in Prop by default even if all the arguments are (is that
really what we want? roconnor says no).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.mli')
0 files changed, 0 insertions, 0 deletions