acic_procedural: bug fix:

                 sometimes whd is not enough, we need normalize ...

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index 489feb4b66aa54385f1e3f102ecdc5381cb1d9c8..4c0014d2e320e4e214aa511f66f1694ee9b6ac59 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/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/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index 85dba95ea1942859856ce77d0eaf042c25d5ca49..ec2e1919c456bf2f807c865d3f5e5cff8b48d2d1 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/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/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 1eeb0aca3b3356a9168673d20750a35d8d05720e..39fb69b0d1067370a408c62be07cc495331516c1 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/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