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/indtypes.ml | 20 +-------------------
 1 file changed, 1 insertion(+), 19 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f79d16c02f..6e87a04446 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -431,24 +431,6 @@ if Int.equal nmr 0 then 0 else
           | _ -> k)
   in find 0 (n-1) (lpar,List.rev hyps)
 
-let lambda_implicit_lift n a =
-  let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in
-  let implicit_sort = mkType (Universe.make level) in
-  let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
-  iterate lambda_implicit n (lift n a)
-
-(* This removes global parameters of the inductive types in lc (for
-   nested inductive types only ) *)
-let abstract_mind_lc env ntyps npars lc =
-  if Int.equal npars 0 then
-    lc
-  else
-    let make_abs =
-      List.init ntyps
-	(function i -> lambda_implicit_lift npars (mkRel (i+1)))
-    in
-    Array.map (substl make_abs) lc
-
 (* [env] is the typing environment
    [n] is the dB of the last inductive type
    [ntypes] is the number of inductive types in the definition
@@ -538,7 +520,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
       let auxntyp = mib.mind_ntypes in
 	if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
 	(* The nested inductive type with parameters removed *)
-	let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
+	let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in
 	  (* Extends the environment with a variable corresponding to
 	     the inductive def *)
 	let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in
-- 
cgit v1.2.3