From 605d0e3e79fe1f654150c5ba14a1cbe3b5a0d78a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 13:16:45 +0100
Subject: [ssr] under(one-liner version): Do nf_betaiota in the last goal

As a result, the following:

  under i: eq_bigr by rewrite adnnC.  (* ensure 1 Under subogal is created *)
  under i: eq_big by [rewrite adnnC | rewrite addnC].  (* 2 Under subgoals *)

amounts to:

  under i: eq_bigr; [rewrite adnnC; over | cbv beta iota].
  under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | cbv beta iota].
---
 plugins/ssr/ssrfwd.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 491d6cfb33..be2732513f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -425,11 +425,13 @@ let undertac ist varnames ((dir,mult),_ as rule) hint =
     if hint = nohint then
       Proofview.tclUNIT ()
     else
+      let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
       Proofview.tclDISPATCH
         ((List.map (function None -> Proofview.V82.tactic overtac
                            | Some e -> ssrevaltac ist e <*>
                                          Proofview.V82.tactic overtac)
-            (if hint = nullhint then [None] else snd hint)) @ [Proofview.tclUNIT ()])
+            (if hint = nullhint then [None] else snd hint))
+         @ [betaiota])
   in
   (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
      intro_lock varnames <*> undertacs)
-- 
cgit v1.2.3