elim tactic: it needs two arguments, a term as well as a pattern

[helm.git] / components / acic_procedural / proceduralPreprocess.ml

diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml
index dcd4cb58b20588734b9a40c5ee5ca27d2db0a1ba..d3e655da70ea6ee20f54674c8782bb5f0deed028 100644 (file)
--- a/components/acic_procedural/proceduralPreprocess.ml
+++ b/components/acic_procedural/proceduralPreprocess.ml
@@ -30,26 +30,17 @@ module Un   = CicUniv
 module I    = CicInspect
 module E    = CicEnvironment
 module S    = CicSubstitution
-module Rd   = CicReduction
 module TC   = CicTypeChecker 
 module Rf   = CicRefine
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
+module PEH  = ProofEngineHelpers
 
 (* helper functions *********************************************************)
 
 let identity x = x
 
 let comp f g x = f (g x)
-   
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (Rd.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
 
 let get_type c t =
    try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
@@ -67,9 +58,9 @@ let refine c t =
       raise e
 
 let get_tail c t =
-   match split c t with
-      | hd :: _, _ -> hd
-      | _          -> assert false
+   match PEH.split_with_whd (c, t) with
+      | (_, hd) :: _, _ -> hd
+      | _               -> assert false
 
 let is_proof c t =
    match get_tail c (get_type c (get_type c t)) with
@@ -159,8 +150,8 @@ let eta_expand g tys t =
    let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
    let arg i = C.Rel (succ i) in
    let rec aux i f a = function
-      | []       -> f, a 
-      | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
+      | []            -> f, a 
+      | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
    in
    let n = List.length tys in
    let absts, args = aux 0 identity [] tys in
@@ -174,7 +165,7 @@ let get_tys c decurry =
    let rec aux n = function
 (*      | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *)
       | t                 ->
-         let tys, _ = split c (get_type c t) in
+         let tys, _ = PEH.split_with_whd (c, get_type c t) in
          let _, tys = HEL.split_nth n (List.rev tys) in
         let tys, _ = HEL.split_nth decurry tys in
          tys
@@ -251,7 +242,7 @@ and pp_appl g ht es c t = function
       pp_proof g ht es c x
 
 and pp_atomic g ht es c t =
-   let _, premsno = split c (get_type c t) in
+   let _, premsno = PEH.split_with_whd (c, get_type c t) in
    g t true premsno
 
 and pp_mutcase g ht es c uri tyno outty arg cases =
@@ -265,14 +256,14 @@ and pp_mutcase g ht es c uri tyno outty arg cases =
       I.S.mem tyno (I.get_mutinds_of_uri uri t) 
    in
    let map2 case (_, cty) = 
-      let map (h, case, k) premise = 
+      let map (h, case, k) (_, premise) = 
          if h > 0 then pred h, case, k else
         if is_recursive premise then 
            0, add_abst k case, k + 2 
         else
            0, case, succ k
       in
-      let premises, _ = split c cty in
+      let premises, _ = PEH.split_with_whd (c, cty) in
       let _, lifted_case, _ =
          List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
       in