Two bugs fixed in the apply tactic:

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index a7c1d39bd1953073fff0228f9556c59210047599..23aa20bfb50cb30d4483e5fd2c04400281ce7934 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -608,17 +608,18 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
  in
   res @ locate_in_term what ~where:ty context
 
-(* saturate_term newmeta metasenv context ty                                  *)
-(* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)
-(* which there is new a META for each hypothesis, a list of arguments for the *)
-(* new applications and the index of the last new META introduced. The nth    *)
-(* argument in the list of arguments is just the nth new META.                *)
-let saturate_term newmeta metasenv context ty =
+(* saturate_term newmeta metasenv context ty goal_arity                       *)
+(* Given a type [ty] (a backbone), it returns its suffix of length            *)
+(* [goal_arity] head and a new metasenv in which there is new a META for each *)
+(* hypothesis, a list of arguments for the new applications and the index of  *)
+(* the last new META introduced. The nth argument in the list of arguments is *)
+(* just the nth new META.                                                     *)
+let saturate_term newmeta metasenv context ty goal_arity =
  let module C = Cic in
  let module S = CicSubstitution in
+ assert (goal_arity >= 0);
   let rec aux newmeta ty =
-   let ty' = ty in
-   match ty' with
+   match ty with
       C.Cast (he,_) -> aux newmeta he
 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
       (* If the expected type is a Type, then also Set is OK ==>
@@ -643,22 +644,31 @@ let saturate_term newmeta metasenv context ty =
          CicMkImplicit.identity_relocation_list_for_metavariable context
        in
         let newargument = C.Meta (newmeta,irl) in
-         let (res,newmetasenv,arguments,lastmeta) =
+         let res,newmetasenv,arguments,lastmeta,prod_no =
           aux (newmeta + 1) (S.subst newargument t)
          in
-         let s' = CicReduction.normalize ~delta:false context s in
-          res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
-          (** NORMALIZE RATIONALE 
-           * we normalize the target only NOW since we may be in this case:
-           * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k  
-           * and we want a mesasenv with ?1:A1 and ?2:A2 and not
-           * ?1, ?2, ?3 (that is the one we whould get if we start from the
-           * beta-normalized A1 -> A2 -> A3 -> P **)
-    | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
+          if prod_no + 1 = goal_arity then
+           let head = CicReduction.normalize ~delta:false context ty in
+            head,[],[],newmeta,goal_arity + 1
+          else
+           (** NORMALIZE RATIONALE 
+            * we normalize the target only NOW since we may be in this case:
+            * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k  
+            * and we want a mesasenv with ?1:A1 and ?2:A2 and not
+            * ?1, ?2, ?3 (that is the one we whould get if we start from the
+            * beta-normalized A1 -> A2 -> A3 -> P **)
+           let s' = CicReduction.normalize ~delta:false context s in
+            res,(newmeta,context,s')::newmetasenv,newargument::arguments,
+             lastmeta,prod_no + 1
+    | t ->
+       let head = CicReduction.normalize ~delta:false context t in
+        match CicReduction.whd context head with
+           C.Prod _ as head' -> aux newmeta head'
+         | _ -> head,[],[],newmeta,0
   in
    (* WARNING: here we are using the invariant that above the most *)
    (* recente new_meta() there are no used metas.                  *)
-   let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
+   let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in
     res,metasenv @ newmetasenv,arguments,lastmeta
 
 let lookup_type metasenv context hyp =