diff options
| author | vsiles | 2008-03-18 09:06:14 +0000 |
|---|---|---|
| committer | vsiles | 2008-03-18 09:06:14 +0000 |
| commit | 99541c1123793d1c6352d1326c40426024b55948 (patch) | |
| tree | 21f66eb771dd0a55b96fcad17eed87a2ac9a8e61 /dev/include | |
| parent | 405a876ec06bc92168c2323b44a621734dff4901 (diff) | |
* Small change in the make_eq_decidability call : the functions does not (yet)
work on mutual inductive types so if we can't compute it, we discard it but
keep the boolean equality declaration which is ok even on mutuals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10688 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions