diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-15 10:03:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-15 10:03:21 +0000 |
| commit | 1cb6d3b235b03ccba046dee70b22d9f2e8dd8192 (patch) | |
| tree | 63019a4a21d95cb99dddcce7456e4f59d235771d /kernel/inductive.mli | |
| parent | ded45010b86ccc2203262f13340495b200f742bd (diff) | |
- Fixing bug #2139 (kernel-based test of well-formation of elimination
predicate called from proof refiner was failing because it was not
aware of evars instantiation; I added a nf_evar in 8.2 branch but for
the trunk, I propose to remove the elimination predicate
well-formation test; we therefore assume that tactics build correct
elimination predicates in Case, is it not too much demanding?).
- Seized the opportunity to remove dead kernel code about non dependent
elimination predicates (all predicates are stored dependent by
default since a few years now).
- Anecdotic complement to commit 12229 (removal of obsolete comment).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12241 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index d09cdbdb7..f877b5391 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -65,6 +65,10 @@ val type_case_branches : env -> inductive * constr list -> unsafe_judgment -> constr -> types array * types * constraints +val build_branches_type : + inductive -> mutual_inductive_body * one_inductive_body -> + constr list -> constr -> types array + (* Return the arity of an inductive type *) val mind_arity : one_inductive_body -> rel_context * sorts_family |