the refiner was not checking that the resulting type

of an application was the expected one in case
the application is ((lambda...) ?...) when ?...
resolves to the empty ? vector.

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 757041451bbe7978aeb30d0dcdaf88cdf35663d8..037c5c6e2ce6b80f23e4bbacfe2f0471162e1b8b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -12,7 +12,7 @@
 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
 
 let debug s = prerr_endline (Lazy.force s);;
-(* let debug _ = ();; *)
+let debug _ = ();;
 
 module COT : Set.OrderedType 
 with type t = string * NCic.term * int * int  * NCic.term *

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 5a6f1028fdf9a4ad177a2483961a090096f8a697..c4534e8daf6f466430f1144abf40ed28ed3c691a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -109,7 +109,7 @@ let rec typeof rdb
        | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
        | C.Appl _ when skip_appl -> metasenv, subst, t, expty
        | _ ->
-          pp (lazy (
+          pp (lazy ("forcing infty=expty: "^
           (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
           (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
            try 
@@ -126,7 +126,7 @@ let rec typeof rdb
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " expty= " ^
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
        match expty with None -> "None" | Some e -> 
        NCicPp.ppterm ~metasenv ~subst ~context e));
     let metasenv, subst, t, infty = 
@@ -332,7 +332,7 @@ let rec typeof rdb
                 NCicTypeChecker.type_of_branch 
                   ~subst context leftno outtype cons ty_cons in
               pp (lazy ("TYPEOFBRANCH: " ^
-               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
                NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
               let metasenv, subst, p, _ = 
                 typeof_aux metasenv subst context (Some ty_branch) p in
@@ -344,7 +344,7 @@ let rec typeof rdb
       metasenv, subst, C.Match (r, outtype, term, pl),resty
     | C.Match _ -> assert false
     in
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty true true metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
@@ -467,7 +467,9 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
        " of type " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_he
        ^ " to type " ^ match expty with None -> "None" | Some x -> 
        NCicPp.ppterm ~metasenv ~subst ~context x));
-      force_ty true false metasenv subst context orig_t res ty_he expty
+     (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
+      * the application may also be a lambda! *)
+     force_ty false false metasenv subst context orig_t res ty_he expty
   | NCic.Implicit `Vector::tl ->
       let has_some_more_pis x =
         match NCicReduction.whd ~subst context x with

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index caa069a0d839697cdbfc36e8a0c155bccfed1b3c..152c729d0d0f50ffdcc3d28c0f85c98aa1a32bd3 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -435,12 +435,8 @@ let letin_tac ~where ~what:(_,_,w) name =
 ;;
 
 let apply_tac (s,n,t) = 
-  let t = 
-    match t with
-    | Ast.AttributedTerm (_,Ast.Binder _) | Ast.Binder _ -> t
-    | _ -> Ast.Appl [t; Ast.Implicit `Vector]
-  in
-    exact_tac (s,n,t)
+  let t = Ast.Appl [t; Ast.Implicit `Vector] in
+  exact_tac (s,n,t)
 ;;
 
 type indtyinfo = {