apply now tries both to reduce and to not reduce the applied term

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 7eddcd1640c035e9a817e73031bcd3c509bf4d6f..c6dc1bf4a4169b60ed5eb769d2ac4918a82f541c 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -162,7 +162,7 @@ let new_metasenv_for_apply newmeta proof context ty =
  let module C = Cic in
  let module S = CicSubstitution in
   let rec aux newmeta ty =
-   let ty' = CicReduction.whd context ty in 
+   let ty' = (*CicReduction.whd context*) ty in 
    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
@@ -259,6 +259,19 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
+let new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty termty =
+  let (consthead,newmetas,arguments,_) =
+    new_metasenv_for_apply newmeta' proof context termty
+  in
+  let newmetasenv = metasenv'@newmetas in
+  let subst,newmetasenv',_ = 
+    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+  in
+  let t = 
+    if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)
+  in
+  subst,newmetasenv',t
+
 let apply_tac_verbose ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
@@ -300,47 +313,39 @@ let apply_tac_verbose ~term (proof, goal) =
      | _ -> [],newmeta,[],term
    in
    let metasenv' = metasenv@newmetasenvfragment in
-   let termty,_ = (* TASSI:FIXME *)
+   let termty,_ = 
      CicTypeChecker.type_of_aux' metasenv' context term CicUniv.empty_ugraph in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty
    in
-    (* newmeta is the lowest index of the new metas introduced *)
-    let (consthead,newmetas,arguments,_) =
-     new_metasenv_for_apply newmeta' proof context termty
-    in
-     let newmetasenv = metasenv'@newmetas in
-      let subst,newmetasenv',_ = (* TASSI:FIXME *)
-        CicUnification.fo_unif newmetasenv context consthead ty 
-         CicUniv.empty_ugraph
-      in
-       let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
-       let apply_subst = CicMetaSubst.apply_subst subst in
-        let old_uninstantiatedmetas,new_uninstantiatedmetas =
-         (* subst_in doesn't need the context. Hence the underscore. *)
-         let subst_in _ = CicMetaSubst.apply_subst subst in
-          classify_metas newmeta in_subst_domain subst_in newmetasenv'
-        in
-         let bo' =
-          apply_subst
-           (if List.length newmetas = 0 then
-             term'
-            else
-             Cic.Appl (term'::arguments)
-           )
-         in
-         let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
-         let subst_in =
-           (* if we just apply the subtitution, the type is irrelevant:
+   let subst,newmetasenv',t = 
+     try
+       new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
+         termty
+     with CicUnification.UnificationFailure _ -> 
+       new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
+         (CicReduction.whd context termty)
+   in
+   let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
+   let apply_subst = CicMetaSubst.apply_subst subst in
+   let old_uninstantiatedmetas,new_uninstantiatedmetas =
+     (* subst_in doesn't need the context. Hence the underscore. *)
+     let subst_in _ = CicMetaSubst.apply_subst subst in
+     classify_metas newmeta in_subst_domain subst_in newmetasenv'
+   in
+   let bo' = apply_subst t in
+   let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
+   let subst_in =
+     (* if we just apply the subtitution, the type is irrelevant:
              we may use Implicit, since it will be dropped *)
-           CicMetaSubst.apply_subst 
-            ((metano,(context, bo', Cic.Implicit None))::subst)
-         in
-         let (newproof, newmetasenv''') =
-           subst_meta_and_metasenv_in_proof
-             proof metano subst_in newmetasenv''
-         in
-           (subst_in,(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+     CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
+   in
+   let (newproof, newmetasenv''') = 
+     subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
+   in
+     (subst_in,
+       (newproof, 
+          List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)