X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=e42ad490eee970aee950dc98be1effcd0f0d99d1;hb=59c1da7b30cc49916a636682556ed1b9532cd146;hp=324141af46b0783c535ab07eab7720dbdb801663;hpb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 324141af4..e42ad490e 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -72,7 +72,7 @@ let lift k n =
       | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
       | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
       | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
-      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t)
+      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k ty, lift_term k s, lift_term (succ k) t)
       | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
       | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
    in
@@ -240,7 +240,7 @@ let clear c hyp =
    aux [] c
 
 let elim_inferred_type context goal arg using cpattern =
-   let metasenv, ugraph = [], Un.empty_ugraph in 
+   let metasenv, ugraph = [], Un.oblivion_ugraph in 
    let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
    let _splits, args_no = PEH.split_with_whd (context, ety) in
    let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim 
@@ -249,3 +249,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