fixing the semantics of subst

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index fd6e7c59f35d8e2b1b4798eac51bf7d445427cf9..8760f36ef46f998bb61ca9a11e4c466308eb99d5 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -191,7 +191,9 @@ 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 _ -> 
+      let msg = lazy "rewrite: nothing to rewrite" in
+      raise (PET.Fail msg)
  in
   ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
   
@@ -364,16 +366,20 @@ let transitivity_tac ~term =
 
 (* FG: subst tactic *********************************************************)
 
+(* 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 msg0 = lazy "Subst: not found in context"
 let msg1 = lazy "Subst: not a simple equality"
 let msg2 = lazy "Subst: recursive equation" 
 
 let subst_tac ~hyp =
    let hole = C.Implicit (Some `Hole) in
-   let map self = function
-      | Some (C.Name s, _) when s <> self -> Some (s, hole)
-      | _                                 -> None
-   in
    let subst_tac status =
       let (proof, goal) = status in
       let (_, metasenv, _, _) = proof in
@@ -390,27 +396,27 @@ let subst_tac ~hyp =
            when LO.is_eq_URI uri -> `RightToLeft, i, t
         | _ -> raise (PET.Fail msg1)
       in    
+      let rewrite pattern =
+         try_tactic ~tactic:(rewrite_tac ~direction ~pattern what)         
+      in
       let var = match PEH.get_name context i with
          | Some name -> name
         | None      -> raise (PET.Fail msg0)   
       in
       if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
-      let pattern = None, PEH.list_rev_map_filter (map hyp) context, Some hole in
-      let start = rewrite_tac ~direction ~pattern what in
-      let continuation = PESR.clear ~hyps:[hyp; var] in
-      let tac = T.then_ ~start ~continuation in
-      PET.apply_tactic tac status
+      let map self = function
+         | Some (C.Name s, _) when s <> self -> 
+            Some (rewrite (None, [(s, hole)], None))
+         | _                                 -> None
+      in
+      let rew_hips = PEH.list_rev_map_filter (map hyp) context in
+      let rew_concl = rewrite (None, [], Some hole) in
+      let clear = PESR.clear ~hyps:[hyp; var] in
+      let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
+      PET.apply_tactic (T.seq ~tactics) 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