diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
| commit | 4c3301517cf8887b3684fda58e2e4626a072a5fb (patch) | |
| tree | bd1ed746e255a9f25b486711163001b2f45d8017 /kernel/term.mli | |
| parent | a8b034513e0c03ceb7e154949b15f62ac6862f3b (diff) | |
Various fixes:
- Fix a typo in lowercase_utf8
- Fix generation of signatures in subtac_cases not working for dependent
inductive types with dependent indices.
- Fix coercion of inductive types generating ill-typed terms.
- Fix test script using new syntax for Instances.
- Move simpl_existTs to Program.Equality and use it in simpl_depind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
0 files changed, 0 insertions, 0 deletions