X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=e73ccfe596b0b65936fb71f7699b8f82093f9498;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=f6dd83be313c55c94bb961ba1262a03d00a81e59;hpb=b4fd90e993045c2a71b6fd2479cd515f09d36d06;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index f6dd83be3..e73ccfe59 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -195,29 +195,33 @@ let generalize n =
    in
    gen_term
 
-let convert g ety k predicate =
+let convert g ity k predicate =
    let rec aux = function
-      | C.ALambda (_, _, b, ety), C.ALambda (id, n, u, pred) ->
-         C.ALambda (id, n, aux (b, u), aux (ety, pred))
-      | C.AProd (_, _, b, ety), C.AProd (id, n, u, pred) ->
-         C.AProd (id, n, aux (b, u), aux (ety, pred))
-      | C.ALetIn (_, _, a, b, ety), C.ALetIn (id, n, v, u, pred) ->
-         C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ety, pred))
+      | C.ALambda (_, _, b, ity), C.ALambda (id, n, u, pred) ->
+         C.ALambda (id, n, aux (b, u), aux (ity, pred))
+      | C.AProd (_, _, b, ity), C.AProd (id, n, u, pred) ->
+         C.AProd (id, n, aux (b, u), aux (ity, pred))
+      | C.ALetIn (_, _, a, b, ity), C.ALetIn (id, n, v, u, pred) ->
+         C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ity, pred))
       | C.AAppl (_, bs), C.AAppl (id, us) when List.length bs = List.length us ->
          let map b u = aux (b,u) in
 	 C.AAppl (id, List.map2 map bs us)
-      | C.ACast (_, ety, b), C.ACast (id, pred, u) ->
-         C.ACast (id, aux (ety, pred), aux (b, u))
-      | ety, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) ->
-	 aux (ety, subst 1 v pred) 	 
-      | ety, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) ->
-         aux (ety, C.AAppl (id, subst 1 v pred :: vs))
+      | C.ACast (_, ity, b), C.ACast (id, pred, u) ->
+         C.ACast (id, aux (ity, pred), aux (b, u))
+      | ity, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) ->
+	 aux (ity, subst 1 v pred) 	 
+      | ity, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) ->
+         aux (ity, C.AAppl (id, subst 1 v pred :: vs))
       | _, pred                                                 -> pred
    in
-   g k (aux (ety, predicate))
+   g k (aux (ity, predicate))
 
-let mk_pattern psno ety predicate =
-   clear_absts (convert (generalize psno) ety) psno 0 predicate 
+let mk_pattern psno ity predicate =
+   clear_absts (convert (generalize psno) ity) psno 0 predicate 
+
+let beta v = function
+   | C.ALambda (_, _, _, t) -> subst 1 v t
+   | _                      -> assert false
 
 let get_clears c p xtypes = 
    let meta = C.Implicit None in
@@ -270,7 +274,7 @@ let clear c hyp =
       | entry :: tail -> aux (entry :: c) tail
    in
    aux [] c
-
+(*
 let elim_inferred_type context goal arg using cpattern =
    let metasenv, ugraph = [], Un.default_ugraph in
    let ety = H.get_type "elim_inferred_type" context using in
@@ -282,7 +286,7 @@ let elim_inferred_type context goal arg using cpattern =
    let ty = C.Appl (predicate :: actual_args) in
    let upto = List.length actual_args in
    Rd.head_beta_reduce ~delta:false ~upto ty
-
+*)
 let does_not_occur = function
    | C.AImplicit (_, None) -> true
    | _                     -> false