Coercions are now propagated under let...ins.

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index 5727dae676ac51a9f0f545a11c834aa99ba0d384..e0f920fff9e93bdecc4aa93873f6a50b2217d8f8 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -572,6 +572,7 @@ and try_coercions status
               cl, left_p, leftno, rno
           | _ -> raise exn
         in
+        (*{{{*) pp (lazy "CASE");
         let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
           match t,n with
           | _,0 ->
@@ -802,6 +803,17 @@ and try_coercions status
         let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) 
         in
         metasenv, subst, t, expty (*}}}*)
+    | _,_,NCic.LetIn(name,ty,t,bo) -> 
+        pp (lazy "LETIN");
+        let context_bo = (name, NCic.Def (t,ty)) :: context in
+        let metasenv, subst, bo2, _ = 
+          try_coercions status ~localise metasenv subst context_bo
+           bo orig_t (NCicSubstitution.lift status 1 infty)
+           (NCicSubstitution.lift status 1 expty) perform_unification exc
+        in
+        let coerced = NCic.LetIn (name,ty,t,bo2) in
+        pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
+        metasenv, subst, coerced, expty
     | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> 
         let rec mk_fresh_name ctx firstch n =
           let candidate = (String.make 1 firstch) ^ (string_of_int n) in