X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=177471c7403a4d9eb2da538289f76e5e718f0681;hb=d3d4ea54cb895a1adc6cb327df42e1394b3f2bea;hp=c2d0d15e171586b339f2fa32cd695cac1d063c54;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index c2d0d15e1..177471c74 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/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