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

[helm.git] / components / tactics / proofEngineHelpers.ml

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index c2d0d15e171586b339f2fa32cd695cac1d063c54..177471c7403a4d9eb2da538289f76e5e718f0681 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -639,3 +639,12 @@ let get_rel context name =
       | _ :: tl                                 -> aux (succ i) tl
    in
    aux 1 context
+
+let split_with_whd (c, t) =
+   let add s v c = Some (s, Cic.Decl v) :: c in
+   let rec aux whd a n c = function
+      | Cic.Prod (s, v, t)  -> aux false ((c, v) :: a) (succ n) (add s v c) t
+      | v when whd          -> (c, v) :: a, n
+      | v                   -> aux true a n c (CicReduction.whd c v)
+    in
+    aux false [] 0 c t