ssr: ipats: V82.tactic ~nf_evars:false everywhere

4 files changed, 35 insertions, 29 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index daad730ff..23da1eb69 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -121,13 +121,13 @@ let refine_interp_apply_view dbl ist gl gv =
         else [])
 
 let apply_top_tac =
-  Tacticals.New.tclTHENLIST [
-    Proofview.V82.tactic (introid top_id);
-    Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
-    Tactics.clear [top_id]
+  Tacticals.tclTHENLIST [
+    introid top_id;
+    apply_rconstr (mkRVar top_id);
+    old_cleartac [SsrHyp(None,top_id)]
   ]
 
-let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl ->
+let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
  let _, clr = interp_hyps ist gl gclr in
  let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
  let ggenl, tclGENTAC =
@@ -152,7 +152,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl ->
     let gl = pf_merge_uc_of sigma gl in
     Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
   | _, _ ->
-     let open Proofview.Notations in
-     Proofview.V82.of_tactic (apply_top_tac <*> cleartac clr) gl) gl
+     Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
 )
 
+let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index b3e59f7fc..a5d44d925 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -377,7 +377,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
 let no_intro ?ist what eqid elim_tac is_rec clr = elim_tac
 
 let elimtac x =
-  Proofview.V82.tactic
+  Proofview.V82.tactic ~nf_evars:false
     (ssrelim ~is_case:false [] (`EConstr ([],None,x)) None no_intro)
 let casetac x = ssrelim ~is_case:true [] (`EConstr ([],None,x)) None no_intro
 
@@ -435,6 +435,9 @@ let perform_injection c gl =
   let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in 
   Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl
 
-let ssrscasetac force_inj c = Proofview.V82.tactic (fun gl ->
-  if force_inj || is_injection_case c gl then perform_injection c gl
+let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl ->
+  if is_injection_case c gl then perform_injection c gl
   else casetac c gl)
+
+let ssrscasetac c =
+  Proofview.V82.tactic ~nf_evars:false (fun gl -> casetac c gl)
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index b802486a0..0541a13ed 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -45,6 +45,9 @@ val perform_injection :
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val ssrscasetac :
-  bool ->
+  EConstr.constr ->
+  unit Proofview.tactic
+
+val ssrscase_or_inj_tac :
   EConstr.constr ->
   unit Proofview.tactic
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 77ebe17a4..1a964bd50 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -137,9 +137,9 @@ let tac_case t =
     Ssrcommon.tacTYPEOF t >>= fun ty ->
     Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj ->
     if is_inj then
-      V82.tactic (Ssrelim.perform_injection t)
+      V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)
     else
-      Ssrelim.ssrscasetac false t
+      Ssrelim.ssrscasetac t
 end
 
 (** [=> [: id]] ************************************************************)
@@ -218,7 +218,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
      tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
   | IPatInj ipatss ->
      tclIORPAT (Ssrcommon.tclWITHTOP
-       (fun t -> V82.tactic (Ssrelim.perform_injection t))) ipatss
+       (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t))) ipatss
 
   | IPatAnon Drop -> intro_drop
   | IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -230,15 +230,15 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
   | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
 
   | IPatSimpl (Simpl n) ->
-       V82.tactic (Ssrequality.simpltac (Simpl n))
+       V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
   | IPatSimpl (Cut n) ->
-       V82.tactic (Ssrequality.simpltac (Cut n))
+       V82.tactic ~nf_evars:false (Ssrequality.simpltac (Cut n))
   | IPatSimpl (SimplCut (n,m)) ->
-       V82.tactic (Ssrequality.simpltac (SimplCut (n,m)))
+       V82.tactic ~nf_evars:false (Ssrequality.simpltac (SimplCut (n,m)))
 
   | IPatRewrite (occ,dir) ->
      Ssrcommon.tclWITHTOP
-       (fun x -> V82.tactic (Ssrequality.ipat_rewrite occ dir x))
+       (fun x -> V82.tactic  ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x))
 
   | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids
 
@@ -302,7 +302,7 @@ end
 let with_dgens { dgens; gens; clr } maintac = match gens with
   | [] -> with_defective maintac dgens clr
   | gen :: gens ->
-      V82.tactic (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen
+      V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen
 
 let mkCoqEq env sigma =
   let eq = Coqlib.((build_coq_eq_data ()).eq) in
@@ -326,7 +326,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
          | Term.ProdType (_, src, tgt) -> begin
              match EConstr.kind_of_type sigma src with
              | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
-                V82.tactic Ssrcommon.unprotecttac <*>
+                V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*>
                 Ssrcommon.tclINTRO_ID ipat
              | _ -> Ssrcommon.tclINTRO_ANON <*> intro_eq ()
              end
@@ -380,9 +380,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
     | _ -> tclUNIT () in
   let unprot =
     if eqid <> None && is_rec
-    then V82.tactic Ssrcommon.unprotecttac else tclUNIT () in
+    then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in
   V82.of_tactic begin
-    V82.tactic ssrelim <*>
+    V82.tactic ~nf_evars:false ssrelim <*>
     tclIPAT_EQ (intro_eq <*> unprot) ipats
   end
 
@@ -477,12 +477,12 @@ let ssrelimtac (view, (eqid, (dgens, ipats))) =
     | [v] ->
       Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs ->
       tclDISPATCH (List.map (fun elim ->
-        V82.tactic
+        V82.tactic ~nf_evars:false
           (Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats)))
         cs)
     | [] ->
       tclINDEPENDENT
-        (V82.tactic
+        (V82.tactic ~nf_evars:false
           (Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats)))
     | _ ->
       Ssrcommon.errorstrm
@@ -497,7 +497,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
         Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj ->
         let simple = (eqid = None && deps = [] && occ = None) in
         if simple && inj then
-          V82.tactic (Ssrelim.perform_injection vc) <*>
+          V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*>
           Tactics.clear (List.map Ssrcommon.hyp_id clear) <*>
           tclIPATssr ipats
         else
@@ -506,7 +506,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
             if view <> [] && eqid <> None && deps = []
             then [gen], [], None
             else deps, clear, occ in
-          V82.tactic
+          V82.tactic ~nf_evars:false
             (Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc))
               eqid (elim_intro_tac ipats))
       in
@@ -515,7 +515,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
   in
   with_dgens dgens (ndefectcasetac view eqid ipats)
 
-let ssrscasetoptac = Ssrcommon.tclWITHTOP (Ssrelim.ssrscasetac false)
+let ssrscasetoptac = Ssrcommon.tclWITHTOP Ssrelim.ssrscase_or_inj_tac
 let ssrselimtoptac = Ssrcommon.tclWITHTOP Ssrelim.elimtac
 
 (** [move] **************************************************************)
@@ -555,7 +555,7 @@ let tclIPAT ip =
 
 let ssrmovetac = function
   | _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) ->
-     let gentac = V82.tactic (Ssrcommon.genstac (gens, [])) in
+     let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in
      let conclusion _ t clear ccl =
        Tactics.apply_type ~typecheck:true ccl [t] <*>
        Tactics.clear (List.map Ssrcommon.hyp_id clear) in
@@ -569,7 +569,7 @@ let ssrmovetac = function
     let dgentac = with_dgens dgens eqmovetac in
     dgentac <*> tclIPAT (eqmoveipats pat ipats)
   | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) ->
-    let gentac = V82.tactic (Ssrcommon.genstac (gens, clr)) in
+    let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in
     gentac <*> tclIPAT ipats
   | _, (_, ({ clr }, ipats)) ->
     Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats]