improved check in delift for flexible lc entries.

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 7c199f8c07bf0c64ec295392f99083ad81b20db8..56ec069d2c77bb7d30eff3773073908bdc01b6ff 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -114,10 +114,14 @@ let rec typeof rdb
           (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
            try 
              let metasenv, subst =
+    (*D*)inside 'U'; try let rc = 
                NCicUnification.unify rdb metasenv subst context infty expty 
+    (*D*)in outside(); rc with exc -> outside (); raise exc
              in
              metasenv, subst, t, expty
-           with exc -> 
+           with 
+           | NCicUnification.Uncertain _ 
+           | NCicUnification.UnificationFailure _ as exc -> 
              try_coercions rdb ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
@@ -229,8 +233,18 @@ let rec typeof rdb
        let metasenv, subst, t, _ = 
          typeof_aux metasenv subst context (Some ty) t in
        let context1 = (n, C.Def (t,ty)) :: context in
+       let metasenv, subst, expty1 = 
+         match expty with 
+         | None -> metasenv, subst, None 
+         | Some x -> 
+             let m, s, x = 
+               NCicUnification.delift_term_wrt_terms 
+                 rdb metasenv subst context x [t]
+             in
+               m, s, Some x
+       in
        let metasenv, subst, bo, bo_ty = 
-         typeof_aux metasenv subst context1 None bo 
+         typeof_aux metasenv subst context1 expty1 bo 
        in
        let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
@@ -509,11 +523,13 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
           let metasenv,subst, flex_prod, _ =
            typeof rdb ~localise metasenv subst
             context flex_prod None in
+(*
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nOF: " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
+*)
           let metasenv, subst =
              try NCicUnification.unify rdb metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf