X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=b8cdc08ea1b3af2a0288ef6239f3718ad4aed5ea;hb=750d027aedc76aac9def8885dc2bdb6ccdc049d9;hp=68b47341c05caff79f8972eb645c16c8fef30d73;hpb=1acfe506c30e7fcc9d6e427d2523130c371a1159;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 68b47341c..b8cdc08ea 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/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