lambda case fixed, used to not properly use the expected type if it was not a Prod

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index d47767528a79801a84763e2537236d9e7b12bfe7..73634e7e0757e2ac3a477cfb0a1b4b092ab4544c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -101,13 +101,13 @@ let rec typeof hdb
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   ~look_for_coercion metasenv subst context term expty 
 =
-  let force_ty metasenv subst context orig t infty expty =
+  let force_ty skip_lambda metasenv subst context orig t infty expty =
     (*D*)inside 'F'; try let rc = 
     match expty with
     | Some expty ->
        (match t with
-       | C.Implicit _ 
-       | C.Lambda _ -> metasenv, subst, t, expty
+       | C.Implicit _ -> assert false
+       | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
        | _ ->
           pp (lazy (
           (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
@@ -177,14 +177,14 @@ let rec typeof hdb
            context orig_s orig_t (name,s) t (s1,s2)
        in
        metasenv, subst, NCic.Prod(name,s,t), ty
-    | C.Lambda (n,(s as orig_s),t) ->
-       let exp_s, exp_ty_t =
+    | C.Lambda (n,(s as orig_s),t) as orig ->
+       let exp_s, exp_ty_t, force_after =
          match expty with
-         | None -> None, None
+         | None -> None, None, false
          | Some expty -> 
              match NCicReduction.whd ~subst context expty with
-             | C.Prod (_,s,t) -> Some s, Some t
-             | _ -> None, None (** XXX FUNCLASS |-> QUALCOSA *)
+             | C.Prod (_,s,t) -> Some s, Some t, false
+             | _ -> None, None, true 
        in
        let metasenv, subst, s, ty_s = 
          typeof_aux metasenv subst context None s in
@@ -201,11 +201,15 @@ let rec typeof hdb
                exp_s))) exc))
          | None -> (metasenv, subst), None
        in
-       let context = (n,C.Decl s) :: context in
+       let context_for_t = (n,C.Decl s) :: context in
        let metasenv, subst, t, ty_t = 
-         typeof_aux metasenv subst context exp_ty_t t 
+         typeof_aux metasenv subst context_for_t exp_ty_t t 
        in
-       metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
+       if force_after then
+         force_ty false metasenv subst context orig 
+           (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
+       else 
+         metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
     | C.LetIn (n,(ty as orig_ty),t,bo) ->
        let metasenv, subst, ty, ty_ty = 
          typeof_aux metasenv subst context None ty in
@@ -283,7 +287,7 @@ let rec typeof hdb
     in
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
-      force_ty metasenv subst context orig t infty expty
+      force_ty true metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
   in
     typeof_aux metasenv subst context expty term