From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 24 May 2011 21:39:32 +0000 (+0000)
Subject: Coercions are now propagated under let...ins.
X-Git-Tag: make_still_working~2491
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf1817cb5d753cb4c0f14725be867e9f96da84a4;p=helm.git

Coercions are now propagated under let...ins.
---

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index 5727dae67..e0f920fff 100644
--- 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