- new tactic subst removes simple non recursive equalities from the context

[helm.git] / helm / software / components / tactics / equalityTactics.ml

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index c697acaedaeeb79d08940d912abd3ced915b40d6..fd6e7c59f35d8e2b1b4798eac51bf7d445427cf9 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -191,7 +191,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
     in
      (proof',goals)
   with (* FG: this should be PET.Fail _ *)
-     TC.TypeCheckerFailure _ -> PET.apply_tactic (P.letout_tac ()) status
+     TC.TypeCheckerFailure _ -> PET.apply_tactic P.letout_tac status
  in
   ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
   
@@ -362,7 +362,7 @@ let transitivity_tac ~term =
   ProofEngineTypes.mk_tactic (transitivity_tac ~term)
 ;;
 
-(* FG *)
+(* FG: subst tactic *********************************************************)
 
 let msg0 = lazy "Subst: not found in context"
 let msg1 = lazy "Subst: not a simple equality"
@@ -402,3 +402,26 @@ let subst_tac ~hyp =
       PET.apply_tactic tac status
    in
    PET.mk_tactic subst_tac
+
+(* FG: This should be replaced by T.try_tactic *)
+let try_tactic ~tactic =
+   let try_tactic status =
+      try PET.apply_tactic tactic status with
+         | PET.Fail _ -> PET.apply_tactic T.id_tac status
+   in
+   PET.mk_tactic try_tactic
+
+let subst_tac =
+   let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
+   let map = function
+      | Some (C.Name s, _) -> Some (subst s)
+      | _                  -> None
+   in
+   let subst_tac status =
+      let (proof, goal) = status in
+      let (_, metasenv, _, _) = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      let tactics = PEH.list_rev_map_filter map context in
+      PET.apply_tactic (T.seq ~tactics) status
+   in
+   PET.mk_tactic subst_tac