Procedural: clear tactics added

[helm.git] / components / acic_procedural / proceduralConversion.ml

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index 68b47341c05caff79f8972eb645c16c8fef30d73..b8cdc08ea1b3af2a0288ef6239f3718ad4aed5ea 100644 (file)
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -145,44 +145,48 @@ let mk_pattern psno predicate =
    let body = generalize psno predicate in
    clear_absts 0 psno body
 
-let get_clears c p xet = 
+let get_clears c p xtypes = 
    let meta = C.Implicit None in
-   let rec aux c names p et = function
+   let rec aux c names p it et = function
       | []                                                -> 
          List.rev c, List.rev names         
       | Some (C.Name name as n, C.Decl v) as hd :: tl     ->
          let hd, names, v = 
-           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
               Some (C.Anonymous, C.Decl v), name :: names, meta 
            else 
               hd, names, v
         in
         let p = C.Lambda (n, v, p) in
+        let it = C.Prod (n, v, it) in
         let et = C.Prod (n, v, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
          let hd, names, v = 
-           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
               Some (C.Anonymous, C.Def (v, x)), name :: names, meta
            else 
               hd, names, v
         in
         let p = C.LetIn (n, v, p) in
+        let it = C.LetIn (n, v, it) in
         let et = C.LetIn (n, v, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
         let p = C.Lambda (n, meta, p) in
+        let it = C.Lambda (n, meta, it) in
         let et = C.Lambda (n, meta, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
         let p = C.LetIn (n, meta, p) in
+        let it = C.LetIn (n, meta, it) in
         let et = C.LetIn (n, meta, et) in
-        aux (hd :: c) names p et tl
+        aux (hd :: c) names p it et tl
       | None :: tl                                        -> assert false
    in
-   match xet with 
-      | Some et -> aux [] [] p et c
-      | None    -> c, []
+   match xtypes with 
+      | Some (it, et) -> aux [] [] p it et c
+      | None          -> c, []
 
 let clear c hyp =
    let rec aux c = function