acic_procedural: bug fix:

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

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 85dba95ea1942859856ce77d0eaf042c25d5ca49..ec2e1919c456bf2f807c865d3f5e5cff8b48d2d1 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -652,6 +652,13 @@ let split_with_whd (c, t) =
     in
     aux false [] 0 c t
 
+let split_with_normalize (c, t) =
+   let add s v c = Some (s, Cic.Decl v) :: c in
+   let rec aux a n c = function
+      | Cic.Prod (s, v, t)  -> aux ((c, v) :: a) (succ n) (add s v c) t
+      | v                   -> (c, v) :: a, n
+    in
+    aux [] 0 c (CicReduction.normalize c t)
 
   (* menv sorting *)
 module OT =