diff options
| author | herbelin | 2009-08-11 15:15:46 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-11 15:15:46 +0000 |
| commit | a07e31a2693bde01d3dca59364693096d550561a (patch) | |
| tree | 322e0acb77a7dfc1a2276b88a73357ffc09a08a7 /pretyping/inductiveops.mli | |
| parent | 9cfe880e1f5f9dddd63aa269a2fb159665c2d182 (diff) | |
Ensures that let-in's in arities of inductive types work well. Maybe not
very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 357fb09082..cc1bb7f418 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -58,7 +58,7 @@ val mis_nf_constructor_type : val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array -(* Return number of expected parameters and of expected real arguments *) +(* Return the lengths of parameters signature and real arguments signature *) val inductive_nargs : env -> inductive -> int * int val mis_constructor_nargs_env : env -> constructor -> int |