(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

(*#* #stop file *)

      Tactic Definition SubstFwd H y :=
         Repeat (
            Match Context With
               | [ K: ? |- ? ] -> (
                  Match K With
                     | [H] -> Fail 1
                     | _   -> Rewrite H in K
                 )
         ); Try Rewrite H; Clear H y.

      Tactic Definition SubstBack H y :=
         Repeat (
            Match Context With
               | [ K: ? |- ? ] -> (
                  Match K With
                     | [H] -> Fail 1
                     | _   -> Rewrite <- H in K
                  )
         ); Try Rewrite <- H; Clear H y.

      Tactic Definition Subst :=
         Repeat (
            Match Context With
               | [ y: ? |- ? ] -> (
                  Match Context With
                     | [ K: y = ? |- ? ] -> SubstFwd K y
                     | [ K: ? = y |- ? ] -> SubstBack K y
                 )
         ).