From c1f12859e933fdbd2ca5e054fc23c01f79f8cc56 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 10 Sep 2009 10:10:10 +0000
Subject: [PATCH] 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.

---
 helm/software/components/ng_refiner/nCicCoercion.ml |  2 +-
 helm/software/components/ng_refiner/nCicRefiner.ml  | 12 +++++++-----
 helm/software/components/ng_tactics/nTactics.ml     |  8 ++------
 3 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 757041451..037c5c6e2 100644
--- 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 5a6f1028f..c4534e8da 100644
--- 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 caa069a0d..152c729d0 100644
--- 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 = {
-- 
2.39.2