From ad55bb9bc450fbccc969bca52602a6572217d565 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 20 Jul 2007 14:48:36 +0000
Subject: [PATCH] acic_procedural: bug fix:                  sometimes whd is
 not enough, we need normalize ...

---
 components/acic_procedural/proceduralClassify.ml | 2 +-
 components/tactics/proofEngineHelpers.ml         | 7 +++++++
 components/tactics/proofEngineHelpers.mli        | 4 ++++
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml
index 489feb4b6..4c0014d2e 100644
--- a/components/acic_procedural/proceduralClassify.ml
+++ b/components/acic_procedural/proceduralClassify.ml
@@ -78,7 +78,7 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_whd (c, t) in
+   let vs, h = PEH.split_with_normalize (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 85dba95ea..ec2e1919c 100644
--- 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 = 
diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index 1eeb0aca3..39fb69b0d 100644
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -121,6 +121,10 @@ val get_rel: Cic.context -> string -> Cic.term option
    t and t_i is the premise of t accessed by Rel i in t_0. 
    Performes a whd on the conclusion before giving up.
    Each t_i is returned with a context c_i in wich it is typed
+   split_with_normalize (c, t) normalizes t before operating the split
+   whd is useless here
 *)
 val split_with_whd: Cic.context * Cic.term -> 
                     (Cic.context * Cic.term) list * int
+val split_with_normalize: Cic.context * Cic.term -> 
+                          (Cic.context * Cic.term) list * int
-- 
2.39.2