diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2013-12-26 15:52:50 -0500 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-07-22 17:34:57 -0400 |
| commit | 286abd141d415a621cc8ea98055d8dc744c8b752 (patch) | |
| tree | e3811f8c42d965af5870b412b0499cb0ff89c3cd /kernel/inductive.mli | |
| parent | 9b272a861bc3263c69b699cd2ac40ab2606543fa (diff) | |
Refining match subterm and commutative cut rules. The parameters that are
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 497c06417..05b0248b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -135,3 +135,6 @@ type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec +val lambda_implicit_lift : int -> Constr.constr -> Term.constr + +val abstract_mind_lc : int -> Int.t -> Constr.constr array -> Constr.constr array |