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 /kernel/reduction.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 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index de926bd1d6..9960513294 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -66,6 +66,9 @@ val default_conv_leq : types conversion_function (* Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr +(* Builds an application node, reducing the [n] first beta-zeta redexes. *) +val betazeta_appvect : int -> constr -> constr array -> constr + (* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types |