Two bugs fixed in the apply tactic:

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c43034f93dfd7f672ade503c0723e9474bd021ea..97f40205201446fdf82cebd6ad5a67278edec6c7 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -223,9 +223,9 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
+let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
-   saturate_term newmeta' metasenv' context termty in
+   saturate_term newmeta' metasenv' context termty goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
   in
@@ -234,6 +234,11 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
   in
   subst,newmetasenv',t
 
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+    Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+  | _ -> 0
+
 let apply_tac_verbose ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
@@ -278,18 +283,17 @@ let apply_tac_verbose ~term (proof, goal) =
    let termty,_ = 
      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
    let termty =
-     CicSubstitution.subst_vars exp_named_subst_diff termty
-   in
-(*CSC: this code is suspect and/or bugged: we try first without reduction
-  and then using whd. However, the saturate_term always tries with full
-  reduction without delta. *)
+     CicSubstitution.subst_vars exp_named_subst_diff termty in
+   let goal_arity = count_prods context ty in
    let subst,newmetasenv',t = 
-    try
+    let rec add_one_argument n =
+     try
       new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
-        termty
-    with CicUnification.UnificationFailure _ ->
-      new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
-        (CicReduction.whd context termty)
+        termty n
+     with CicUnification.UnificationFailure _ when n > 0 ->
+      add_one_argument (n - 1)
+    in
+     add_one_argument goal_arity
    in
    let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
    let apply_subst = CicMetaSubst.apply_subst subst in
@@ -457,7 +461,7 @@ let elim_tac ~term =
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let (termty,metasenv',arguments,fresh_meta) =
      ProofEngineHelpers.saturate_term
-      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty in
+      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
     let term = if arguments = [] then term else Cic.Appl (term::arguments) in
     let uri,exp_named_subst,typeno,args =
      match termty with