ssr: rewrite Ssripats and Ssrview in the tactic monad

Ssripats and Ssrview are now written in the Tactic Monad.
Ssripats implements the => tactical.
Ssrview implements the application of forward views.

The code is, according to my tests, 100% backward compatible.
The code is much more documented than before.
Moreover the "ist" (ltac context) used to interpret views is the correct
one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC
EXTEND execution time).  Some of the code not touched by this commit
still uses the incorrect ist, so its visibility in TACTIC EXTEND
can't be removed yet.

The main changes in the code are:
- intro patterns are implemented using a state machine (a goal comes
  with a state). Ssrcommon.MakeState provides an easy way for a tactic
  to enrich the goal with with data of interest, such as the set of
  hyps to be cleared.  This cleans up the old implementation that, in
  order to thread the state, that to redefine a bunch of tclSTUFF
- the interpretation of (multiple) forward views uses the state to
  accumulate intermediate results
- the bottom of Sscommon collects a bunch of utilities written in the
  tactic monad. Most of them are the rewriting of already existing
  utilities.  When possible the old version was removed.

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 11ebe4337..18ada1c5d 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -617,20 +617,20 @@ let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
 
 let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
-  let interp_rpattern ist gl gc =
-    try interp_rpattern ist gl gc
+  let interp_rpattern gl gc =
+    try interp_rpattern gl gc
     with _ when snd mult = May -> fail := true; project gl, T mkProp in
   let interp gc gl =
     try interp_term ist gl gc
     with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
   let rwtac gl = 
-    let rx = Option.map (interp_rpattern ist gl) grx in
+    let rx = Option.map (interp_rpattern gl) grx in
     let t = interp gt gl in
     (match kind with
     | RWred sim -> simplintac occ rx sim
     | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt
     | RWeq -> rwrxtac occ rx dir t) gl in
-  let ctac = cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
+  let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
   if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl
 
 (** Rewrite argument sequence *)