- doubleTypeInference: we check for unreferenced letins in the inferred type also...

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

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index f6dd83be313c55c94bb961ba1262a03d00a81e59..65d5f1edf14911a93c66c81fdba2cdaf25d71809 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -195,29 +195,29 @@ 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 get_clears c p xtypes = 
    let meta = C.Implicit None in
@@ -270,7 +270,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 +282,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