From 286abd141d415a621cc8ea98055d8dc744c8b752 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Dec 2013 15:52:50 -0500
Subject: 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.

---
 kernel/inductive.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 497c064172..05b0248b9e 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
-- 
cgit v1.2.3