From bf4fdaa1836a17e4d36d38ba47959d1f50155a7b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 29 May 2018 23:07:02 +0200
Subject: [ssr] under: rewrite takes an optional bool arg

* If this flag under=true: enable flag with_evars of refine_with
  to create evar(s) if the "under lemma" has non-inferable args.

* Backward compatibility of ssr rewrite is kept.

* Fix test-suite/ssr/dependent_type_err.v
---
 plugins/ssr/ssrequality.ml  | 21 ++++++++++-----------
 plugins/ssr/ssrequality.mli |  1 +
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 5abbc214de..ccd0203b17 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -327,7 +327,7 @@ let rule_id = mk_internal_id "rewrite rule"
 
 exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option
 
-let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
+let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
 (*   ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
   let env = pf_env gl in
   let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in
@@ -357,7 +357,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   in
   ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
-    ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
+    ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl
   with _ -> 
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
@@ -385,7 +385,7 @@ let is_construct_ref sigma c r =
   EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
 let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
 
-let rwcltac cl rdx dir sr gl =
+let rwcltac ?under cl rdx dir sr gl =
   let sr =
     let sigma, r = sr in
     let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
@@ -405,7 +405,7 @@ let rwcltac cl rdx dir sr gl =
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
-          pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
+          pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
       | _ -> 
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
@@ -547,7 +547,7 @@ let rwprocess_rule dir rule gl =
   in
     r_sigma, rules
 
-let rwrxtac occ rdx_pat dir rule gl =
+let rwrxtac ?under occ rdx_pat dir rule gl =
   let env = pf_env gl in
   let r_sigma, rules = rwprocess_rule dir rule gl in
   let find_rule rdx =
@@ -585,7 +585,7 @@ let rwrxtac occ rdx_pat dir rule gl =
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
   let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in
-  rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
+  rwcltac ?under (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
 ;;
 
 let ssrinstancesofrule ist dir arg gl =
@@ -614,7 +614,7 @@ let ssrinstancesofrule ist dir arg gl =
 
 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 rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
   let interp_rpattern gl gc =
     try interp_rpattern gl gc
@@ -628,7 +628,7 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
     (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
+    | RWeq -> rwrxtac ?under occ rx dir t) 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
 
@@ -638,8 +638,8 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
 
 (** The "rewrite" tactic *)
 
-let ssrrewritetac ist rwargs =
-  tclTHENLIST (List.map (rwargtac ist) rwargs)
+let ssrrewritetac ?under ist rwargs =
+  tclTHENLIST (List.map (rwargtac ?under ist) rwargs)
 
 (** The "unlock" tactic *)
 
@@ -660,4 +660,3 @@ let unlocktac ist args gl =
     (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); 
     Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in
   tclTHENLIST (List.map utac args @ ktacs) gl
-
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index bbcd6b900a..2f95d3f22b 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -49,6 +49,7 @@ val ssrinstancesofrule :
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val ssrrewritetac :
+  ?under:bool ->
   Ltac_plugin.Tacinterp.interp_sign ->
   ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) *
      (((Ssrast.ssrhyps option * Ssrmatching.occ) *
-- 
cgit v1.2.3


From 3a10b4d89d3d0ba3cdc8f85fbe3b66e8653da117 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 31 May 2018 16:08:59 +0200
Subject: [ssr] move is_ind/constructor_ref to ssrcommon

---
 plugins/ssr/ssrcommon.ml   | 4 ++++
 plugins/ssr/ssrcommon.mli  | 3 +++
 plugins/ssr/ssrequality.ml | 7 +------
 3 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 2a84469af0..ec9a937f80 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1540,5 +1540,9 @@ let get g =
 
 end
 
+let is_construct_ref sigma c r =
+  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
+let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
+
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9662daa7c7..585db41de0 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -482,3 +482,6 @@ module MakeState(S : StateType) : sig
   val get : Proofview.Goal.t -> S.state
 
 end
+
+val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
+val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ccd0203b17..f55ece7d09 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -19,7 +19,6 @@ open Context
 open Vars
 open Locus
 open Printer
-open Globnames
 open Termops
 open Tacinterp
 
@@ -381,10 +380,6 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl
       (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
-let is_construct_ref sigma c r =
-  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
-let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
-
 let rwcltac ?under cl rdx dir sr gl =
   let sr =
     let sigma, r = sr in
@@ -403,7 +398,7 @@ let rwcltac ?under cl rdx dir sr gl =
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
-      | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
+      | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
       | _ -> 
-- 
cgit v1.2.3


From 0e38043fc616a8a5dac3cdace8f7bed8f1e295ce Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 31 May 2018 16:09:28 +0200
Subject: [ssr] clean up type declaration of ssrrewritetac

---
 plugins/ssr/ssrequality.mli | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index 2f95d3f22b..008c1d457c 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -51,11 +51,7 @@ val ssrinstancesofrule :
 val ssrrewritetac :
   ?under:bool ->
   Ltac_plugin.Tacinterp.interp_sign ->
-  ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) *
-     (((Ssrast.ssrhyps option * Ssrmatching.occ) *
-         Ssrmatching.rpattern option) *
-        (ssrwkind * Ssrast.ssrterm)))
-           list -> Tacmach.tactic
+   ssrrwarg list -> Tacmach.tactic
 
 val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic
 
-- 
cgit v1.2.3


From cb7f2a54e6a1e8430f74bb9a02c24b22556b2287 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 31 May 2018 16:11:52 +0200
Subject: [ssr] fix implementation of refine ~first_goes_last

---
 plugins/ssr/ssrcommon.ml  | 27 +++++++++++++--------------
 plugins/ssr/ssrcommon.mli |  1 +
 2 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ec9a937f80..0b3bfab366 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -973,7 +973,7 @@ let dependent_apply_error =
  *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
-let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
+let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl =
   if with_evars then
     let refine gl =
       let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in
@@ -985,8 +985,11 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
       pf_partial_solution gl t gs
     in
     Proofview.(V82.of_tactic
-      (tclTHEN (V82.tactic refine)
-        (if with_shelve then shelve_unifiable else tclUNIT ()))) gl
+      (Tacticals.New.tclTHENLIST [
+        V82.tactic refine;
+        (if with_shelve then shelve_unifiable else tclUNIT ());
+        (if first_goes_last then cycle 1 else tclUNIT ())
+        ])) gl
   else
     let t, gl = if n = 0 then t, gl else
       let sigma, si = project gl, sig_it gl in
@@ -1001,21 +1004,17 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
           | _ -> assert false
       in loop sigma t [] n in
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
-    Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
+    Proofview.(V82.of_tactic
+      (Tacticals.New.tclTHENLIST [
+         V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t));
+         (if first_goes_last then cycle 1 else tclUNIT ())
+      ])) gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
-  let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
   let uct = Evd.evar_universe_context (fst oc) in
-  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.Unsafe.to_constr (snd oc)) in
+  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
   let gl = pf_unsafe_merge_uc uct gl in
-  let oc = if not first_goes_last || n <= 1 then oc else
-    let l, c = decompose_lam oc in
-    if not (List.for_all_i (fun i (_,t) -> Vars.closedn ~-i t) (1-n) l) then oc else
-    compose_lam (let xs,y = List.chop (n-1) l in y @ xs) 
-      (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
-  in
-  pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc));
-  try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
+  try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 585db41de0..3049f67f87 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -312,6 +312,7 @@ val applyn :
            with_evars:bool ->
            ?beta:bool ->
            ?with_shelve:bool ->
+           ?first_goes_last:bool ->
            int ->
            EConstr.t -> v82tac
 exception NotEnoughProducts
-- 
cgit v1.2.3


From 2b2b70d2f0487994db7effc7ced89a658c0cf4f3 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 24 Feb 2019 19:01:46 +0100
Subject: [ssr] under: Add opaque modules for tagging and notation support

(Note: coq notations cannot contain \n)

Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
---
 plugins/ssr/ssreflect.v | 50 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 4721e19a8b..e0b775f07b 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -500,3 +500,53 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
 Lemma abstract_context T (P : T -> Type) x :
   (forall Q, Q = P -> Q x) -> P x.
 Proof. by move=> /(_ P); apply. Qed.
+
+(*****************************************************************************)
+(* Syntax proposal for the under tactic:
+
+under i: eq_bigr by []. (* renaming *)
+
+under i: eq_bigr.
+  by rewrite addnC over.
+(* oneliner version *)
+under i: eq_bigr by rewrite adnnC.
+
+under i: lem => /andP [H1 H2].
+  by rewrite addnC over.
+(* oneliner version *)
+under i: lem by move => /andP [H1 H2]; rewrite addnC.
+
+(* 2-var version *)
+under i j: {2}[in RHS]eq_mx.
+(* ... *)
+
+(* nested version *)
+under i: eq_bigr=> ?; under j: eq_bigl.
+ *)
+
+Module Type UNDER.
+Parameter Under :
+  forall (R : Type), R -> R -> Prop.
+Parameter Under_from_eq :
+  forall (T : Type) (x y : T),
+  @Under T x y -> x = y.
+Parameter over :
+  forall (T : Type) (x : T),
+  @Under T x x <-> True.
+Notation "''Under[' x ]" := (@Under _ x _)
+  (at level 8, format "''Under['  x  ]").
+End UNDER.
+
+Module Export Under : UNDER.
+Definition Under := @eq.
+Definition Under_done := @refl_equal.
+Lemma Under_from_eq (T : Type) (x y : T) :
+  @Under T x y -> x = y.
+Proof. easy. Qed.
+Lemma over (T : Type) (x : T) :
+  @Under T x x <-> True.
+Proof. easy. Qed.
+End Under.
+
+Register Under as plugins.ssreflect.Under.
+Register Under_from_eq as plugins.ssreflect.Under_from_eq.
-- 
cgit v1.2.3


From 717f77bbaf479ae1e8335ce226ad71c2c88df644 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 31 May 2018 16:12:33 +0200
Subject: [ssr] implement "under i: ext_lemma" by rewrite rule

Still to do: renaming the bound variables afterwards
---
 plugins/ssr/ssrfwd.ml     | 63 +++++++++++++++++++++++++++++++++++++++++++++++
 plugins/ssr/ssrfwd.mli    |  3 +++
 plugins/ssr/ssrparser.mlg |  5 ++++
 3 files changed, 71 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 3cadc92bcc..ff7b891319 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -319,3 +319,66 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
   Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
+
+open Proofview.Notations
+
+let is_app_evar sigma t =
+  match EConstr.kind sigma t with
+  | Constr.Evar _ -> true
+  | Constr.App(t,_) ->
+      begin match EConstr.kind sigma t with
+      | Constr.Evar _ -> true
+      | _ -> false end
+  | _ -> false
+
+let tmp = ref 0
+
+let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
+ let c = Proofview.Goal.concl gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let rec aux c =
+  match EConstr.kind_of_type sigma c with
+  | Term.SortType _ -> Proofview.tclUNIT ()
+  | ( Term.ProdType ({ Context.binder_name = name },_,t)
+    | Term.LetInType ({ Context.binder_name = name },_,_,t) ) ->
+      begin match names with
+      | n :: names -> Ssripats.(tclIPAT @@ [Ssripats.IOpId n]) <*> intro_lock names
+      | [] ->
+          (* after quell intro patterns, use IpatTemp *)
+          let id =
+            match name with
+            | Name.Anonymous -> Id.of_string (Printf.sprintf "_under_%d_" !tmp)
+            | Name.Name n -> n in
+          incr tmp;
+          Ssripats.tclIPAT [
+            Ssripats.IOpId id;
+            Ssripats.IOpEqGen (intro_lock names);
+            Ssripats.IOpEqGen (Tactics.revert [id])]
+      end
+  | Term.CastType (t,_) -> aux t
+  | Term.AtomicType _ ->
+      let t = Reductionops.whd_all env sigma c in
+      match EConstr.kind_of_type sigma t with
+      | Term.AtomicType(hd, args) when
+          Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
+          Array.length args = 3 && is_app_evar sigma args.(2) ->
+            Tactics.New.refine ~typecheck:true (fun sigma ->
+              let sigma, under =
+                Ssrcommon.mkSsrConst "Under" env sigma in
+              let sigma, under_from_eq =
+                Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
+              let ty = EConstr.mkApp (under,args) in
+              let sigma, t = Evarutil.new_evar env sigma ty in
+              sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
+      | _ -> Proofview.tclUNIT ()
+  in
+    aux c
+
+end
+
+let undertac ist varnames ((dir,mult),_ as rule) =
+  if mult <> Ssrequality.nomult then
+    Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
+  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ist [rule]) <*>
+  intro_lock varnames
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 35e89dbcea..fe7d84871e 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -57,3 +57,6 @@ val sufftac :
        (bool * Tacinterp.Value.t option list)) ->
   Tacmach.tactic
 
+val undertac :
+  Ltac_plugin.Tacinterp.interp_sign ->
+  Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0ec5f1673a..e63d1e5562 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2650,6 +2650,11 @@ TACTIC EXTEND ssrgenhave2
     V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) }
 END
 
+TACTIC EXTEND under
+  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] ->
+    { Ssrfwd.undertac ist names r }
+END
+
 {
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
-- 
cgit v1.2.3


From 8b8ab996552d79ac070af80eb0978b523d929833 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 21 Jun 2018 10:51:48 +0200
Subject: [ssr] rewrite takes optional function to make the new valued of the
 redex

---
 plugins/ssr/ssrequality.ml  | 32 ++++++++++++++++----------------
 plugins/ssr/ssrequality.mli |  5 +++++
 2 files changed, 21 insertions(+), 16 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index f55ece7d09..921dce4689 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -326,15 +326,15 @@ let rule_id = mk_internal_id "rewrite rule"
 
 exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option
 
-let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
+let id_map_redex _ sigma ~before:_ ~after = sigma, after
+
+let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
 (*   ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
   let env = pf_env gl in
   let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in
-  let sigma, p = 
-    let sigma = Evd.create_evar_defs sigma in
-    let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
-    (sigma, ev)
-  in
+  let sigma, new_rdx = map_redex env sigma ~before:rdx ~after:new_rdx in
+  let sigma, p = (* The resulting goal *)
+    Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
   let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
@@ -354,7 +354,8 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl
     | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
     | e when CErrors.noncritical e -> raise (PRtype_error None)
   in
-  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
+  ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
+  ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
     ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl
   with _ -> 
@@ -380,7 +381,7 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl
       (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
-let rwcltac ?under cl rdx dir sr gl =
+let rwcltac ?under ?map_redex cl rdx dir sr gl =
   let sr =
     let sigma, r = sr in
     let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
@@ -400,7 +401,7 @@ let rwcltac ?under cl rdx dir sr gl =
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
-          pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
+          pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
       | _ -> 
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
@@ -434,7 +435,6 @@ let rwcltac ?under cl rdx dir sr gl =
   in
   tclTHEN cvtac' rwtac gl
 
-
 [@@@ocaml.warning "-3"]
 let lz_coq_prod =
   let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod
@@ -542,7 +542,7 @@ let rwprocess_rule dir rule gl =
   in
     r_sigma, rules
 
-let rwrxtac ?under occ rdx_pat dir rule gl =
+let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
   let env = pf_env gl in
   let r_sigma, rules = rwprocess_rule dir rule gl in
   let find_rule rdx =
@@ -580,7 +580,7 @@ let rwrxtac ?under occ rdx_pat dir rule gl =
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
   let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in
-  rwcltac ?under (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
+  rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
 ;;
 
 let ssrinstancesofrule ist dir arg gl =
@@ -609,7 +609,7 @@ let ssrinstancesofrule ist dir arg gl =
 
 let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
 
-let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
+let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
   let interp_rpattern gl gc =
     try interp_rpattern gl gc
@@ -623,7 +623,7 @@ let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
     (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 ?under occ rx dir t) gl in
+    | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) 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
 
@@ -633,8 +633,8 @@ let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
 
 (** The "rewrite" tactic *)
 
-let ssrrewritetac ?under ist rwargs =
-  tclTHENLIST (List.map (rwargtac ?under ist) rwargs)
+let ssrrewritetac ?under ?map_redex ist rwargs =
+  tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs)
 
 (** The "unlock" tactic *)
 
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index 008c1d457c..601968d511 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -48,8 +48,13 @@ val ssrinstancesofrule :
   Ssrast.ssrterm ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
+(* map_redex (by default the identity on after) is called on the
+ * redex (before) and its replacement (after). It is used to
+ * "rename" binders by the under tactic *)
 val ssrrewritetac :
   ?under:bool ->
+  ?map_redex:(Environ.env -> Evd.evar_map ->
+                 before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) ->
   Ltac_plugin.Tacinterp.interp_sign ->
    ssrrwarg list -> Tacmach.tactic
 
-- 
cgit v1.2.3


From 964779322e0358dc821b03a67b4a7dd0b3b6d11e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 2 Apr 2019 21:48:40 +0200
Subject: [ssr] under: Rename bound variables a posteriori for cosmetic purpose

Rename the bound variables of the last (lambda) argument of the redex
w.r.t. the varnames specified by the user.

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
---
 plugins/ssr/ssrfwd.ml | 40 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index ff7b891319..29983e7504 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -377,8 +377,46 @@ let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
 
 end
 
+let rec pretty_rename evar_map term = function
+  | [] -> term
+  | varname :: varnames ->
+     try begin
+       match EConstr.destLambda evar_map term
+       with ({ Context.binder_relevance = r }, types, body) ->
+           let res = pretty_rename evar_map body varnames in
+           let name = Names.Name.mk_name varname in
+           (* Note: we don't explicitly check name \notin free_vars(res) here *)
+           EConstr.mkLambda (Context.make_annot name r, types, res)
+         end
+     with
+     | DestKO ->
+        ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
+        term
+
 let undertac ist varnames ((dir,mult),_ as rule) =
   if mult <> Ssrequality.nomult then
     Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
-  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ist [rule]) <*>
+
+  let map_redex env evar_map ~before:_ ~after:t =
+    ppdebug(lazy Pp.(str("under vars: " ^
+      (List.fold_right (fun e r -> Names.Id.to_string e ^ " " ^ r) varnames ""))));
+    ppdebug(lazy Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map t));
+
+    let evar_map, ty = Typing.type_of env evar_map t in
+    let new_t = (* pretty-rename the bound variables *)
+      try begin match EConstr.destApp evar_map t with (f, ar) ->
+            let lam = Array.last ar in
+            let new_lam = pretty_rename evar_map lam varnames in
+            let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
+            new_ar.(len1) <- new_lam;
+            EConstr.mkApp (f, new_ar)
+          end with
+      | DestKO ->
+        ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp"));
+        t
+    in
+    ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
+    evar_map, new_t
+  in
+  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
   intro_lock varnames
-- 
cgit v1.2.3


From 2fed7b9a1870c7b921255ec055f0511ef530749d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Jun 2018 15:37:17 +0200
Subject: [ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"

Both can be use to close the "under goals", in rewrite style or in
closing-tactic style.

Contrarily to the previous implementation that assumed
  "over : forall (T : Type) (x : T), @Under T x x <-> True"
this new design won't require the Setoid library.

Extend the test-suite (in test-suite/ssr/under.v)
---
 plugins/ssr/ssreflect.v | 42 +++++++++++++++++++++++++++++++++---------
 1 file changed, 33 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index e0b775f07b..d2b44a869a 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -528,25 +528,49 @@ Module Type UNDER.
 Parameter Under :
   forall (R : Type), R -> R -> Prop.
 Parameter Under_from_eq :
-  forall (T : Type) (x y : T),
-  @Under T x y -> x = y.
+  forall (T : Type) (x y : T), @Under T x y -> x = y.
+
+(** [Over, over, over_done]: for "by rewrite over" *)
+Parameter Over :
+  forall (R : Type), R -> R -> Prop.
 Parameter over :
-  forall (T : Type) (x : T),
-  @Under T x x <-> True.
+  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+Parameter over_done :
+  forall (T : Type) (x : T), @Over T x x.
+(* We need both hints below, otherwise the test-suite does not pass *)
+Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core.
+(* => for test_under_eq_big *)
+Hint Resolve over_done : core.
+(* => for test_over_1_1 *)
+
+(** [under_done]: for Ltac-style over *)
+Parameter under_done :
+  forall (T : Type) (x : T), @Under T x x.
 Notation "''Under[' x ]" := (@Under _ x _)
   (at level 8, format "''Under['  x  ]").
 End UNDER.
 
 Module Export Under : UNDER.
 Definition Under := @eq.
-Definition Under_done := @refl_equal.
 Lemma Under_from_eq (T : Type) (x y : T) :
   @Under T x y -> x = y.
-Proof. easy. Qed.
-Lemma over (T : Type) (x : T) :
-  @Under T x x <-> True.
-Proof. easy. Qed.
+Proof. by []. Qed.
+Definition Over := Under.
+Lemma over :
+  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+Proof. by []. Qed.
+Lemma over_done :
+  forall (T : Type) (x : T), @Over T x x.
+Proof. by []. Qed.
+Lemma under_done :
+  forall (T : Type) (x : T), @Under T x x.
+Proof. by []. Qed.
 End Under.
 
 Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
+
+Ltac over :=
+  by apply Under.under_done.
+(* [exact: Under.under_done] woud be more satisfying,
+   but issue with 2-var test-suite (test_over_2_2) *)
-- 
cgit v1.2.3


From 527e6a97d1429a58273ddc6b4ce2826df0dba1c6 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 24 Feb 2019 16:08:36 +0100
Subject: [ssr] over: also works on universally quantified goals

---
 plugins/ssr/ssreflect.v | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index d2b44a869a..e705942c36 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -571,6 +571,14 @@ Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
 Ltac over :=
-  by apply Under.under_done.
-(* [exact: Under.under_done] woud be more satisfying,
-   but issue with 2-var test-suite (test_over_2_2) *)
+  solve [ apply Under.under_done | by rewrite over ].
+
+(* The 2 variants below wouldn't work for the [test_over_2_1] test
+   (2-var case with evars)
+
+Ltac over :=
+  exact: Under.under_done.
+
+Ltac over :=
+  by rewrite over.
+ *)
-- 
cgit v1.2.3


From 1a5a4c9c8cacea6e6ed7ced8766cadb0195655d9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 24 Feb 2019 18:30:00 +0100
Subject: [ssr] under: Add support for one-liners "under (…) by [tac1|tac2]."

Supported syntax:

  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 *)

Equivalent, expanded form:

  under i: eq_bigr; [rewrite adnnC; over | idtac].
  under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | idtac].
---
 plugins/ssr/ssrfwd.ml     | 18 +++++++++++++++---
 plugins/ssr/ssrfwd.mli    |  3 ++-
 plugins/ssr/ssrparser.mlg |  4 ++--
 3 files changed, 19 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 29983e7504..570b5a8c61 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -393,7 +393,9 @@ let rec pretty_rename evar_map term = function
         ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
         term
 
-let undertac ist varnames ((dir,mult),_ as rule) =
+let overtac gl = ssr_n_tac "over" ~-1 gl
+
+let undertac ist varnames ((dir,mult),_ as rule) hint =
   if mult <> Ssrequality.nomult then
     Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
 
@@ -418,5 +420,15 @@ let undertac ist varnames ((dir,mult),_ as rule) =
     ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
     evar_map, new_t
   in
-  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
-  intro_lock varnames
+  let undertacs =
+    if hint = nohint then
+      Proofview.tclUNIT ()
+    else
+      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 ()])
+  in
+  (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
+     intro_lock varnames <*> undertacs)
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index fe7d84871e..63df8f5349 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -59,4 +59,5 @@ val sufftac :
 
 val undertac :
   Ltac_plugin.Tacinterp.interp_sign ->
-  Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic
+  Names.Id.t list -> Ssrequality.ssrrwarg ->
+  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index e63d1e5562..507cf8db70 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2651,8 +2651,8 @@ TACTIC EXTEND ssrgenhave2
 END
 
 TACTIC EXTEND under
-  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] ->
-    { Ssrfwd.undertac ist names r }
+  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] ->
+    { Ssrfwd.undertac ist names r hint }
 END
 
 {
-- 
cgit v1.2.3


From e22d8f725bae56550fed8cab8640447953cd3a47 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 00:04:44 +0100
Subject: [ssr] under: generate missing Under subgoal for eq_bigl/eq_big

in the particular case where the side-condition is phrased

  (_ : @eqfun bool I P1 P2)

instead of

  (_ : forall x : I, P1 x = P2 x)
---
 plugins/ssr/ssrfwd.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 570b5a8c61..491d6cfb33 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -360,6 +360,7 @@ let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
   | Term.AtomicType _ ->
       let t = Reductionops.whd_all env sigma c in
       match EConstr.kind_of_type sigma t with
+      | Term.ProdType _ -> aux t
       | Term.AtomicType(hd, args) when
           Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
           Array.length args = 3 && is_app_evar sigma args.(2) ->
-- 
cgit v1.2.3


From 8279f7673c89254139869ac3a3688e12658db471 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 24 Feb 2019 22:21:15 +0100
Subject: [ssr] under: Extend the test-suite to exemplify most use cases

---
 plugins/ssr/ssreflect.v | 30 +++++-------------------------
 1 file changed, 5 insertions(+), 25 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index e705942c36..229f6ceb1a 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -502,27 +502,7 @@ Lemma abstract_context T (P : T -> Type) x :
 Proof. by move=> /(_ P); apply. Qed.
 
 (*****************************************************************************)
-(* Syntax proposal for the under tactic:
-
-under i: eq_bigr by []. (* renaming *)
-
-under i: eq_bigr.
-  by rewrite addnC over.
-(* oneliner version *)
-under i: eq_bigr by rewrite adnnC.
-
-under i: lem => /andP [H1 H2].
-  by rewrite addnC over.
-(* oneliner version *)
-under i: lem by move => /andP [H1 H2]; rewrite addnC.
-
-(* 2-var version *)
-under i j: {2}[in RHS]eq_mx.
-(* ... *)
-
-(* nested version *)
-under i: eq_bigr=> ?; under j: eq_bigl.
- *)
+(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *)
 
 Module Type UNDER.
 Parameter Under :
@@ -539,9 +519,9 @@ Parameter over_done :
   forall (T : Type) (x : T), @Over T x x.
 (* We need both hints below, otherwise the test-suite does not pass *)
 Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core.
-(* => for test_under_eq_big *)
+(* => for [test-suite/ssr/under.v:test_big_nested_1] *)
 Hint Resolve over_done : core.
-(* => for test_over_1_1 *)
+(* => for [test-suite/ssr/over.v:test_over_1_1] *)
 
 (** [under_done]: for Ltac-style over *)
 Parameter under_done :
@@ -573,8 +553,8 @@ Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 Ltac over :=
   solve [ apply Under.under_done | by rewrite over ].
 
-(* The 2 variants below wouldn't work for the [test_over_2_1] test
-   (2-var case with evars)
+(* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1]
+   (2-var test case with evars).
 
 Ltac over :=
   exact: Under.under_done.
-- 
cgit v1.2.3


From 540a581a42114d7cf19b0135d7ad3702fa7cdaca Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 01:52:27 +0100
Subject: [ssr] under: Strenghten over & Add test_big_andb

* Rely on a new tactic unify_helper that workarounds the fact
  [apply Under.under_done] cannot unify (?G i...) with (expr i...) in
  [|- @Under T (expr i...) (?G i...)]
  when expr is a constant expression, or has more than one var (i...).
  Idea: massage the expression with Ltac to obtain a beta redex.

* Simplify test-suite/ssr/under.v by using TestSuite.ssr_mini_mathcomp
  and add a test-case [test_big_andb].

* Summary of commands to quickly test [under]:
  $ cd .../coq
  $ make plugins/ssr/ssreflect.vo plugins/ssr/ssrfun.vo plugins/ssr/ssrbool.vo
  $ cd test-suite
  $ touch prerequisite/ssr_mini_mathcomp.v
  $ make
  $ emacs under.v
---
 plugins/ssr/ssreflect.v | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 229f6ceb1a..7e2c1c913f 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -550,8 +550,33 @@ End Under.
 Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
+Ltac beta_expand c e :=
+  match e with
+  | ?G ?z =>
+    let T := type of z in
+    match c with
+    | context f [z] =>
+      let b := constr:(fun x : T => ltac:(let r := context f [x] in refine r)) in
+      rewrite -{1}[c]/(b z); beta_expand b G
+    | (* constante *) _ =>
+      let b := constr:(fun x : T => ltac:(exact c)) in
+      rewrite -{1}[c]/(b z); beta_expand b G
+    end
+  | ?G => idtac
+  end.
+
+Ltac unify_helper :=
+  move=> *;
+  lazymatch goal with
+  | [ |- @Under _ ?c ?e ] =>
+    beta_expand c e
+  end.
+
 Ltac over :=
-  solve [ apply Under.under_done | by rewrite over ].
+  solve [ apply Under.under_done
+        | by rewrite over
+        | unify_helper; eapply Under.under_done
+        ].
 
 (* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1]
    (2-var test case with evars).
-- 
cgit v1.2.3


From 0a00a122a04ed9afdaccc2dae85e61d51d5d7a89 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 02:05:40 +0100
Subject: [ssr] under: Move {beta_expand, unify_helper} in the module type
 (qualify them)

---
 plugins/ssr/ssreflect.v | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 7e2c1c913f..f8d761b088 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -528,27 +528,6 @@ Parameter under_done :
   forall (T : Type) (x : T), @Under T x x.
 Notation "''Under[' x ]" := (@Under _ x _)
   (at level 8, format "''Under['  x  ]").
-End UNDER.
-
-Module Export Under : UNDER.
-Definition Under := @eq.
-Lemma Under_from_eq (T : Type) (x y : T) :
-  @Under T x y -> x = y.
-Proof. by []. Qed.
-Definition Over := Under.
-Lemma over :
-  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
-Proof. by []. Qed.
-Lemma over_done :
-  forall (T : Type) (x : T), @Over T x x.
-Proof. by []. Qed.
-Lemma under_done :
-  forall (T : Type) (x : T), @Under T x x.
-Proof. by []. Qed.
-End Under.
-
-Register Under as plugins.ssreflect.Under.
-Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
 Ltac beta_expand c e :=
   match e with
@@ -571,6 +550,27 @@ Ltac unify_helper :=
   | [ |- @Under _ ?c ?e ] =>
     beta_expand c e
   end.
+End UNDER.
+
+Module Export Under : UNDER.
+Definition Under := @eq.
+Lemma Under_from_eq (T : Type) (x y : T) :
+  @Under T x y -> x = y.
+Proof. by []. Qed.
+Definition Over := Under.
+Lemma over :
+  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+Proof. by []. Qed.
+Lemma over_done :
+  forall (T : Type) (x : T), @Over T x x.
+Proof. by []. Qed.
+Lemma under_done :
+  forall (T : Type) (x : T), @Under T x x.
+Proof. by []. Qed.
+End Under.
+
+Register Under as plugins.ssreflect.Under.
+Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
 Ltac over :=
   solve [ apply Under.under_done
-- 
cgit v1.2.3


From d9db4dec813a18b205f1cd9bccca54aa23524706 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 02:58:45 +0100
Subject: [ssr] under: Change the style of a few tests (over tactic vs. lemma)

---
 plugins/ssr/ssreflect.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index f8d761b088..c78381d3cc 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -519,7 +519,7 @@ Parameter over_done :
   forall (T : Type) (x : T), @Over T x x.
 (* We need both hints below, otherwise the test-suite does not pass *)
 Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core.
-(* => for [test-suite/ssr/under.v:test_big_nested_1] *)
+(* => for [test-suite/ssr/under.v:test_big_patt1] *)
 Hint Resolve over_done : core.
 (* => for [test-suite/ssr/over.v:test_over_1_1] *)
 
-- 
cgit v1.2.3


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


From 19e3ce970fd8f6d9922006aa30620a2b9db1cd06 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 14:46:17 +0100
Subject: [ssr] under: Check that the number of hints and focused goals match

---
 plugins/ssr/ssrfwd.ml | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index be2732513f..6d0b6de40d 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -396,6 +396,18 @@ let rec pretty_rename evar_map term = function
 
 let overtac gl = ssr_n_tac "over" ~-1 gl
 
+let check_numgoals ?(minus = 0) nh =
+  Proofview.numgoals >>= fun ng ->
+  if nh <> ng then
+    let errmsg =
+      str"Incorrect number of hints" ++ spc() ++
+        str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++
+        str", was given "++ int (nh - minus)++str")."
+    in
+    CErrors.user_err errmsg
+  else
+    Proofview.tclUNIT ()
+
 let undertac ist varnames ((dir,mult),_ as rule) hint =
   if mult <> Ssrequality.nomult then
     Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
@@ -426,12 +438,14 @@ let undertac ist varnames ((dir,mult),_ as rule) hint =
       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))
-         @ [betaiota])
+      let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
+      check_numgoals ~minus:1 nh <*>
+        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))
+           @ [betaiota])
   in
   (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
      intro_lock varnames <*> undertacs)
-- 
cgit v1.2.3


From adbb10dc627faa199bc4164b45740f62af8dc3fc Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 18:12:06 +0100
Subject: [ssr] over: Add Ssrfwd.overtac in the .mli

---
 plugins/ssr/ssrfwd.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 63df8f5349..d57884c3ec 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -61,3 +61,6 @@ val undertac :
   Ltac_plugin.Tacinterp.interp_sign ->
   Names.Id.t list -> Ssrequality.ssrrwarg ->
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
+
+val overtac :
+  Tacmach.tactic
-- 
cgit v1.2.3


From f294fe1684e03f63871864def0f82190da087ebe Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 27 Feb 2019 18:53:11 +0100
Subject: [ssr] under: Fix rewrite goals order when called from under

* "under"-specific behavior:
  the order of goals is kept even if one issues

      Global Set SsrOldRewriteGoalsOrder.

* href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v
---
 plugins/ssr/ssrequality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 921dce4689..ff6dd8f75a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -357,7 +357,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
   ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
-    ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl
+    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl
   with _ -> 
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
-- 
cgit v1.2.3


From 01b5e6e64b2af828b18fa6ee7037a7b7055f026e Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Mar 2019 16:06:14 +0100
Subject: [ssr] Remove the unify_helper tactic that appears unnecessary

It was only required in the (not realistic) test case "test_over_2_2",
which happened to introduce evars after the context variables.
---
 plugins/ssr/ssreflect.v | 23 -----------------------
 1 file changed, 23 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index c78381d3cc..e1e4d25ced 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -528,28 +528,6 @@ Parameter under_done :
   forall (T : Type) (x : T), @Under T x x.
 Notation "''Under[' x ]" := (@Under _ x _)
   (at level 8, format "''Under['  x  ]").
-
-Ltac beta_expand c e :=
-  match e with
-  | ?G ?z =>
-    let T := type of z in
-    match c with
-    | context f [z] =>
-      let b := constr:(fun x : T => ltac:(let r := context f [x] in refine r)) in
-      rewrite -{1}[c]/(b z); beta_expand b G
-    | (* constante *) _ =>
-      let b := constr:(fun x : T => ltac:(exact c)) in
-      rewrite -{1}[c]/(b z); beta_expand b G
-    end
-  | ?G => idtac
-  end.
-
-Ltac unify_helper :=
-  move=> *;
-  lazymatch goal with
-  | [ |- @Under _ ?c ?e ] =>
-    beta_expand c e
-  end.
 End UNDER.
 
 Module Export Under : UNDER.
@@ -575,7 +553,6 @@ Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 Ltac over :=
   solve [ apply Under.under_done
         | by rewrite over
-        | unify_helper; eapply Under.under_done
         ].
 
 (* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1]
-- 
cgit v1.2.3


From c02ac6657863ba08b4c5f52dddf770d864ee6d4c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Mar 2019 17:07:41 +0100
Subject: [ssr] over: Expose the new type of tactic for Ssrfwd.overtac

---
 plugins/ssr/ssrfwd.ml  | 6 +++---
 plugins/ssr/ssrfwd.mli | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 6d0b6de40d..757a7968ca 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -394,7 +394,7 @@ let rec pretty_rename evar_map term = function
         ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
         term
 
-let overtac gl = ssr_n_tac "over" ~-1 gl
+let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1)
 
 let check_numgoals ?(minus = 0) nh =
   Proofview.numgoals >>= fun ng ->
@@ -441,9 +441,9 @@ let undertac ist varnames ((dir,mult),_ as rule) hint =
       let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
       check_numgoals ~minus:1 nh <*>
         Proofview.tclDISPATCH
-          ((List.map (function None -> Proofview.V82.tactic overtac
+          ((List.map (function None -> overtac
                              | Some e -> ssrevaltac ist e <*>
-                                           Proofview.V82.tactic overtac)
+                                           overtac)
               (if hint = nullhint then [None] else snd hint))
            @ [betaiota])
   in
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index d57884c3ec..745560da03 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -63,4 +63,4 @@ val undertac :
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
 
 val overtac :
-  Tacmach.tactic
+  unit Proofview.tactic
-- 
cgit v1.2.3


From f13c55b0c031b6ef92f28a3297ccfa0f7dde869d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Mar 2019 17:33:21 +0100
Subject: [ssr] under: Add comment to justify the need for check_numgoals

---
 plugins/ssr/ssrfwd.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 757a7968ca..8bca62a4ff 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -400,7 +400,7 @@ let check_numgoals ?(minus = 0) nh =
   Proofview.numgoals >>= fun ng ->
   if nh <> ng then
     let errmsg =
-      str"Incorrect number of hints" ++ spc() ++
+      str"Incorrect number of tactics" ++ spc() ++
         str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++
         str", was given "++ int (nh - minus)++str")."
     in
@@ -439,6 +439,9 @@ let undertac ist varnames ((dir,mult),_ as rule) hint =
     else
       let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
       let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
+      (* Usefulness of check_numgoals: tclDISPATCH would be enough,
+         except for the error message w.r.t. the number of
+         provided/expected tactics, as the last one is implied *)
       check_numgoals ~minus:1 nh <*>
         Proofview.tclDISPATCH
           ((List.map (function None -> overtac
-- 
cgit v1.2.3


From 600fef9a1c9cd15ad43196b7750ba15922c01752 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 3 Mar 2019 01:07:19 +0100
Subject: [ssr] under: Simplify the over tactic

* Use ssr `by […|…]` and `apply:`
---
 plugins/ssr/ssreflect.v | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index e1e4d25ced..37390e1af7 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -551,16 +551,6 @@ Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
 Ltac over :=
-  solve [ apply Under.under_done
-        | by rewrite over
-        ].
-
-(* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1]
-   (2-var test case with evars).
-
-Ltac over :=
-  exact: Under.under_done.
-
-Ltac over :=
-  by rewrite over.
- *)
+  by [ apply: Under.under_done
+     | rewrite over
+     ].
-- 
cgit v1.2.3


From e68bccba9344c1b3d77d3e815af6cce1ce50b731 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 21 Mar 2019 10:08:29 +0100
Subject: [ssr] new syntax for the under tactic

---
 plugins/ssr/ssrfwd.ml     | 144 ++++++++++++++++++++++++----------------------
 plugins/ssr/ssrfwd.mli    |   2 +-
 plugins/ssr/ssrparser.mlg |  47 ++++++++++++++-
 3 files changed, 120 insertions(+), 73 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8bca62a4ff..349f0082e1 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -331,68 +331,53 @@ let is_app_evar sigma t =
       | _ -> false end
   | _ -> false
 
-let tmp = ref 0
-
-let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
- let c = Proofview.Goal.concl gl in
- let sigma = Proofview.Goal.sigma gl in
- let env = Proofview.Goal.env gl in
- let rec aux c =
-  match EConstr.kind_of_type sigma c with
-  | Term.SortType _ -> Proofview.tclUNIT ()
-  | ( Term.ProdType ({ Context.binder_name = name },_,t)
-    | Term.LetInType ({ Context.binder_name = name },_,_,t) ) ->
-      begin match names with
-      | n :: names -> Ssripats.(tclIPAT @@ [Ssripats.IOpId n]) <*> intro_lock names
-      | [] ->
-          (* after quell intro patterns, use IpatTemp *)
-          let id =
-            match name with
-            | Name.Anonymous -> Id.of_string (Printf.sprintf "_under_%d_" !tmp)
-            | Name.Name n -> n in
-          incr tmp;
-          Ssripats.tclIPAT [
-            Ssripats.IOpId id;
-            Ssripats.IOpEqGen (intro_lock names);
-            Ssripats.IOpEqGen (Tactics.revert [id])]
-      end
-  | Term.CastType (t,_) -> aux t
-  | Term.AtomicType _ ->
-      let t = Reductionops.whd_all env sigma c in
-      match EConstr.kind_of_type sigma t with
-      | Term.ProdType _ -> aux t
-      | Term.AtomicType(hd, args) when
-          Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
-          Array.length args = 3 && is_app_evar sigma args.(2) ->
-            Tactics.New.refine ~typecheck:true (fun sigma ->
-              let sigma, under =
-                Ssrcommon.mkSsrConst "Under" env sigma in
-              let sigma, under_from_eq =
-                Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
-              let ty = EConstr.mkApp (under,args) in
-              let sigma, t = Evarutil.new_evar env sigma ty in
-              sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
-      | _ -> Proofview.tclUNIT ()
+let intro_lock ipats =
+  let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
+    Proofview.tclORELSE
+      (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
+      (fun _exn -> Proofview.Goal.enter begin fun gl ->
+        let c = Proofview.Goal.concl gl in
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
+        let t = Reductionops.whd_all env sigma c in
+        match EConstr.kind_of_type sigma t with
+        | Term.AtomicType(hd, args) when
+            Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
+            Array.length args = 3 && is_app_evar sigma args.(2) ->
+              Tactics.New.refine ~typecheck:true (fun sigma ->
+                let sigma, under =
+                  Ssrcommon.mkSsrConst "Under" env sigma in
+                let sigma, under_from_eq =
+                  Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
+                let ty = EConstr.mkApp (under,args) in
+                let sigma, t = Evarutil.new_evar env sigma ty in
+                sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
+        | _ ->
+    ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
+
+            Proofview.tclUNIT ()
+       end)
+    end
   in
-    aux c
-
-end
-
-let rec pretty_rename evar_map term = function
-  | [] -> term
-  | varname :: varnames ->
-     try begin
-       match EConstr.destLambda evar_map term
-       with ({ Context.binder_relevance = r }, types, body) ->
-           let res = pretty_rename evar_map body varnames in
-           let name = Names.Name.mk_name varname in
-           (* Note: we don't explicitly check name \notin free_vars(res) here *)
-           EConstr.mkLambda (Context.make_annot name r, types, res)
-         end
-     with
-     | DestKO ->
-        ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
-        term
+  Ssripats.tclIPATssr ipats <*> lock_eq ()
+
+let pretty_rename evar_map term varnames =
+  let rec aux term vars =
+    try
+      match vars with
+      | [] -> term
+      | Names.Name.Anonymous :: varnames ->
+          let name, types, body = EConstr.destLambda evar_map term in
+          let res = aux body varnames in
+          EConstr.mkLambda (name, types, res)
+      | Names.Name.Name _ as name :: varnames ->
+          let { Context.binder_relevance = r }, types, body =
+            EConstr.destLambda evar_map term in
+          let res = aux body varnames in
+          EConstr.mkLambda (Context.make_annot name r, types, res)
+    with DestKO -> term
+  in
+    aux term varnames
 
 let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1)
 
@@ -408,19 +393,37 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-let undertac ist varnames ((dir,mult),_ as rule) hint =
-  if mult <> Ssrequality.nomult then
-    Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
+let undertac ist ipats ((dir,_),_ as rule) hint =
+
+  let varnames =
+    let rec aux acc = function
+      | IPatId id :: rest -> aux (Names.Name.Name id :: acc) rest
+      | IPatClear _ :: rest -> aux acc rest
+      | IPatSimpl _ :: rest -> aux acc rest
+      | IPatAnon (One _ | Drop) :: rest ->
+          aux (Names.Name.Anonymous :: acc) rest
+      | _ -> List.rev acc in
+    aux [] (Option.default [] ipats) in
+
+  (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra
+   * goal (the one that is left once we run over) *)
+  let ipats =
+    match ipats with
+    | None -> [IPatNoop]
+    | Some (IPatCase(Regular []) :: _ as ipats) -> ipats
+    | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest
+    | Some (IPatCase(Block _) :: _ as l) -> l
+    | Some l -> [IPatCase(Regular [l;[]])] in
 
   let map_redex env evar_map ~before:_ ~after:t =
-    ppdebug(lazy Pp.(str("under vars: " ^
-      (List.fold_right (fun e r -> Names.Id.to_string e ^ " " ^ r) varnames ""))));
-    ppdebug(lazy Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map t));
+    ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
 
     let evar_map, ty = Typing.type_of env evar_map t in
     let new_t = (* pretty-rename the bound variables *)
       try begin match EConstr.destApp evar_map t with (f, ar) ->
             let lam = Array.last ar in
+            ppdebug(lazy Pp.(str"under: mapping:" ++
+                             pr_econstr_env env evar_map lam));
             let new_lam = pretty_rename evar_map lam varnames in
             let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
             new_ar.(len1) <- new_lam;
@@ -450,5 +453,8 @@ let undertac ist varnames ((dir,mult),_ as rule) hint =
               (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)
+  let rew =
+    Proofview.V82.tactic
+      (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule])
+  in
+  rew <*> intro_lock ipats <*> undertacs
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 745560da03..6f7cc6d445 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -59,7 +59,7 @@ val sufftac :
 
 val undertac :
   Ltac_plugin.Tacinterp.interp_sign ->
-  Names.Id.t list -> Ssrequality.ssrrwarg ->
+  Ssrast.ssripats option -> Ssrequality.ssrrwarg ->
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
 
 val overtac :
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 507cf8db70..2c46947658 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -741,15 +741,33 @@ let pushIPatNoop = function
   | pats :: orpat -> (IPatNoop :: pats) :: orpat
   | [] -> []
 
+let test_ident_no_do strm =
+  match Util.stream_nth 0 strm with
+  | Tok.IDENT s when s <> "do" -> ()
+  | _ -> raise Stream.Failure
+
+let test_ident_no_do =
+  Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do
+
 }
 
+ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print }
+| [ "YouShouldNotTypeThis" ident(id) ] -> { id }
+END
+
+
+GRAMMAR EXTEND Gram
+  GLOBAL: ident_no_do;
+  ident_no_do: [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ];
+END
+
 ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
   INTERPRETED BY { interp_ipats }
   GLOBALIZED BY { intern_ipats }
   | [ "_" ] -> { [IPatAnon Drop] }
   | [ "*" ] -> { [IPatAnon All] }
   | [ ">" ] -> { [IPatFastNondep] }
-  | [ ident(id) ] -> { [IPatId id] }
+  | [ ident_no_do(id) ] -> { [IPatId id] }
   | [ "?" ] -> { [IPatAnon (One None)] }
   | [ "+" ] -> { [IPatAnon Temporary] }
   | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
@@ -2650,9 +2668,32 @@ TACTIC EXTEND ssrgenhave2
     V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) }
 END
 
+{
+
+let check_under_arg ((_dir,mult),((_occ,_rpattern),_rule)) =
+  if mult <> nomult then
+    CErrors.user_err Pp.(str"under does not support multipliers")
+
+}
+
+
 TACTIC EXTEND under
-  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] ->
-    { Ssrfwd.undertac ist names r hint }
+  | [ "under" ssrrwarg(arg) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist None arg nohint
+    }
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some ipats) arg nohint
+    }
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhintarg(h) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some ipats) arg h
+    }
+  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *)
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some [IPatAnon All]) arg h
+    }
 END
 
 {
-- 
cgit v1.2.3


From 7c598f9f1f6da2cecc70557f9f436392322fc6d9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 2 Apr 2019 01:47:11 +0200
Subject: [ssr] under: use varnames from the 1st ipat with multi-goal under
 lemmas

In particular, this enhances support for lemma eq_big (with 2 side-conditions).
---
 plugins/ssr/ssrfwd.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 349f0082e1..b5082582c9 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -403,7 +403,10 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
       | IPatAnon (One _ | Drop) :: rest ->
           aux (Names.Name.Anonymous :: acc) rest
       | _ -> List.rev acc in
-    aux [] (Option.default [] ipats) in
+    aux [] @@ match ipats with
+              | None -> []
+              | Some (IPatCase(Regular (l :: _)) :: _) -> l
+              | Some l -> l in
 
   (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra
    * goal (the one that is left once we run over) *)
-- 
cgit v1.2.3


From bb6dc2355bcd027a3a89c40629b82eb2019eff6a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 Mar 2019 01:25:39 +0100
Subject: [ssr] under: Add iff support in side-conditions

---
 plugins/ssr/ssrcommon.ml   |  9 ++++++---
 plugins/ssr/ssrcommon.mli  |  3 ++-
 plugins/ssr/ssreflect.v    | 42 ++++++++++++++++++++++++++++++++++++++++++
 plugins/ssr/ssrequality.ml |  4 ++--
 plugins/ssr/ssrfwd.ml      | 13 +++++++++++++
 5 files changed, 65 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 0b3bfab366..a05b1e3d81 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -828,10 +828,12 @@ let view_error s gv =
 open Locus
 (****************************** tactics ***********************************)
 
-let rewritetac dir c =
+let rewritetac ?(under=false) dir c =
   (* Due to the new optional arg ?tac, application shouldn't be too partial *)
+  let open Proofview.Notations in
   Proofview.V82.of_tactic begin
-    Equality.general_rewrite (dir = L2R) AllOccurrences true false c
+      Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*>
+        if under then Proofview.cycle 1 else Proofview.tclUNIT ()
   end
 
 (**********************`:********* hooks ************************************)
@@ -1542,6 +1544,7 @@ end
 let is_construct_ref sigma c r =
   EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
 let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
-
+let is_const_ref sigma c r =
+  EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 3049f67f87..58ce84ecb3 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -349,7 +349,7 @@ val resolve_typeclasses :
 
 (*********************** Wrapped Coq  tactics *****************************)
 
-val rewritetac : ssrdir -> EConstr.t -> tactic
+val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic
 
 type name_hint = (int * EConstr.types array) option ref
 
@@ -486,3 +486,4 @@ end
 
 val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
 val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
+val is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 37390e1af7..94e0b2a724 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -550,7 +550,49 @@ End Under.
 Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
+Module Type UNDER_IFF.
+Parameter Under_iff : Prop -> Prop -> Prop.
+Parameter Under_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
+
+(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *)
+Parameter Over_iff : Prop -> Prop -> Prop.
+Parameter over_iff :
+  forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
+Parameter over_iff_done :
+  forall (x : Prop), @Over_iff x x.
+Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core.
+Hint Resolve over_iff_done : core.
+
+(** [under_iff_done]: for Ltac-style over *)
+Parameter under_iff_done :
+  forall (x : Prop), @Under_iff x x.
+Notation "''Under_iff[' x ]" := (@Under_iff x _)
+  (at level 8, format "''Under_iff['  x  ]").
+End UNDER_IFF.
+
+Module Export Under_iff : UNDER_IFF.
+Definition Under_iff := iff.
+Lemma Under_from_iff (x y : Prop) :
+  @Under_iff x y -> x <-> y.
+Proof. by []. Qed.
+Definition Over_iff := Under_iff.
+Lemma over_iff :
+  forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
+Proof. by []. Qed.
+Lemma over_iff_done :
+  forall (x : Prop), @Over_iff x x.
+Proof. by []. Qed.
+Lemma under_iff_done :
+  forall (x : Prop), @Under_iff x x.
+Proof. by []. Qed.
+End Under_iff.
+
+Register Under_iff as plugins.ssreflect.Under_iff.
+Register Under_from_iff as plugins.ssreflect.Under_from_iff.
+
 Ltac over :=
   by [ apply: Under.under_done
      | rewrite over
+     | apply: Under_iff.under_iff_done
+     | rewrite over_iff
      ].
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ff6dd8f75a..842e4feecf 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
           let gl = pf_merge_uc_of sigma gl in
-          Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl
+          Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl
     else
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
       let r3, _, r3t  = 
@@ -417,7 +417,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
       let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
       let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
-      let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in
+      let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in
       apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl
   in
   let cvtac' _ =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index b5082582c9..2bac69b5b7 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -339,6 +339,19 @@ let intro_lock ipats =
         let c = Proofview.Goal.concl gl in
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
+        match EConstr.kind_of_type sigma c with
+        | Term.AtomicType(hd, args) when
+            Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") &&
+           Array.length args = 2 && is_app_evar sigma args.(1) ->
+           Tactics.New.refine ~typecheck:true (fun sigma ->
+               let sigma, under_iff =
+                 Ssrcommon.mkSsrConst "Under_iff" env sigma in
+               let sigma, under_from_iff =
+                 Ssrcommon.mkSsrConst "Under_from_iff" env sigma in
+               let ty = EConstr.mkApp (under_iff,args) in
+               let sigma, t = Evarutil.new_evar env sigma ty in
+               sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|]))
+        | _ ->
         let t = Reductionops.whd_all env sigma c in
         match EConstr.kind_of_type sigma t with
         | Term.AtomicType(hd, args) when
-- 
cgit v1.2.3


From 04da1739139c8d96469a2b86280e520e532beb39 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 01:08:38 +0200
Subject: [ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc

* Add tests accordingly.
---
 plugins/ssr/ssrfwd.ml     | 15 +++++++++++++--
 plugins/ssr/ssrfwd.mli    |  6 ++++++
 plugins/ssr/ssrparser.mlg |  4 ++--
 3 files changed, 21 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2bac69b5b7..d60e3857b1 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -406,7 +406,15 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-let undertac ist ipats ((dir,_),_ as rule) hint =
+let rec ncons n e = match n with
+  | 0 -> []
+  | n when n > 0 -> e :: ncons (n - 1) e
+  | _ -> failwith "ncons"
+
+let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
+
+  (* total number of implied hints *)
+  let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
 
   let varnames =
     let rec aux acc = function
@@ -426,7 +434,11 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
   let ipats =
     match ipats with
     | None -> [IPatNoop]
+    | Some l when pad_intro -> (* typically, ipats = Some [IPatAnon All] *)
+       let new_l = ncons (nh - 1) l in
+       [IPatCase(Regular (new_l @ [[]]))]
     | Some (IPatCase(Regular []) :: _ as ipats) -> ipats
+    (* Erik: is the previous line correct/useful? *)
     | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest
     | Some (IPatCase(Block _) :: _ as l) -> l
     | Some l -> [IPatCase(Regular [l;[]])] in
@@ -457,7 +469,6 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
       Proofview.tclUNIT ()
     else
       let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
-      let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
       (* Usefulness of check_numgoals: tclDISPATCH would be enough,
          except for the error message w.r.t. the number of
          provided/expected tactics, as the last one is implied *)
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 6f7cc6d445..6dd01ca6fc 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -57,7 +57,13 @@ val sufftac :
        (bool * Tacinterp.Value.t option list)) ->
   Tacmach.tactic
 
+(* pad_intro (by default false) indicates whether the intro-pattern
+   "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches,
+   assuming there are n provided tactics in the ssrhint argument
+   "do [...|...|...]"; it is useful when the intro-pattern is "=> *").
+   Otherwise, "=> i..." is turned into "=> [i...|]". *)
 val undertac :
+  ?pad_intro:bool ->
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssripats option -> Ssrequality.ssrrwarg ->
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 2c46947658..4286ace519 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2690,9 +2690,9 @@ TACTIC EXTEND under
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg h
     }
-  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *)
+  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *)
     check_under_arg arg;
-    Ssrfwd.undertac ist (Some [IPatAnon All]) arg h
+    Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
     }
 END
 
-- 
cgit v1.2.3


From 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 15:03:02 +0200
Subject: [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations

as suggested by @gares, and:

* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
---
 plugins/ssr/ssreflect.v | 83 +++++++++++++++++++++++++------------------------
 plugins/ssr/ssrfwd.ml   |  6 ++--
 2 files changed, 45 insertions(+), 44 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 94e0b2a724..6c74ac1960 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -504,55 +504,55 @@ Proof. by move=> /(_ P); apply. Qed.
 (*****************************************************************************)
 (* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *)
 
-Module Type UNDER.
-Parameter Under :
+Module Type UNDER_EQ.
+Parameter Under_eq :
   forall (R : Type), R -> R -> Prop.
-Parameter Under_from_eq :
-  forall (T : Type) (x y : T), @Under T x y -> x = y.
+Parameter Under_eq_from_eq :
+  forall (T : Type) (x y : T), @Under_eq T x y -> x = y.
 
-(** [Over, over, over_done]: for "by rewrite over" *)
-Parameter Over :
+(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *)
+Parameter Over_eq :
   forall (R : Type), R -> R -> Prop.
-Parameter over :
-  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
-Parameter over_done :
-  forall (T : Type) (x : T), @Over T x x.
+Parameter over_eq :
+  forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y.
+Parameter over_eq_done :
+  forall (T : Type) (x : T), @Over_eq T x x.
 (* We need both hints below, otherwise the test-suite does not pass *)
-Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core.
+Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core.
 (* => for [test-suite/ssr/under.v:test_big_patt1] *)
-Hint Resolve over_done : core.
+Hint Resolve over_eq_done : core.
 (* => for [test-suite/ssr/over.v:test_over_1_1] *)
 
-(** [under_done]: for Ltac-style over *)
-Parameter under_done :
-  forall (T : Type) (x : T), @Under T x x.
-Notation "''Under[' x ]" := (@Under _ x _)
-  (at level 8, format "''Under['  x  ]").
-End UNDER.
-
-Module Export Under : UNDER.
-Definition Under := @eq.
-Lemma Under_from_eq (T : Type) (x y : T) :
-  @Under T x y -> x = y.
+(** [under_eq_done]: for Ltac-style over *)
+Parameter under_eq_done :
+  forall (T : Type) (x : T), @Under_eq T x x.
+Notation "''Under[' x ]" := (@Under_eq _ x _)
+  (at level 8, format "''Under['  x  ]", only printing).
+End UNDER_EQ.
+
+Module Export Under_eq : UNDER_EQ.
+Definition Under_eq := @eq.
+Lemma Under_eq_from_eq (T : Type) (x y : T) :
+  @Under_eq T x y -> x = y.
 Proof. by []. Qed.
-Definition Over := Under.
-Lemma over :
-  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+Definition Over_eq := Under_eq.
+Lemma over_eq :
+  forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y.
 Proof. by []. Qed.
-Lemma over_done :
-  forall (T : Type) (x : T), @Over T x x.
+Lemma over_eq_done :
+  forall (T : Type) (x : T), @Over_eq T x x.
 Proof. by []. Qed.
-Lemma under_done :
-  forall (T : Type) (x : T), @Under T x x.
+Lemma under_eq_done :
+  forall (T : Type) (x : T), @Under_eq T x x.
 Proof. by []. Qed.
-End Under.
+End Under_eq.
 
-Register Under as plugins.ssreflect.Under.
-Register Under_from_eq as plugins.ssreflect.Under_from_eq.
+Register Under_eq as plugins.ssreflect.Under_eq.
+Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq.
 
 Module Type UNDER_IFF.
 Parameter Under_iff : Prop -> Prop -> Prop.
-Parameter Under_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
+Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
 
 (** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *)
 Parameter Over_iff : Prop -> Prop -> Prop.
@@ -566,13 +566,13 @@ Hint Resolve over_iff_done : core.
 (** [under_iff_done]: for Ltac-style over *)
 Parameter under_iff_done :
   forall (x : Prop), @Under_iff x x.
-Notation "''Under_iff[' x ]" := (@Under_iff x _)
-  (at level 8, format "''Under_iff['  x  ]").
+Notation "''Under[' x ]" := (@Under_iff x _)
+  (at level 8, format "''Under['  x  ]", only printing).
 End UNDER_IFF.
 
 Module Export Under_iff : UNDER_IFF.
 Definition Under_iff := iff.
-Lemma Under_from_iff (x y : Prop) :
+Lemma Under_iff_from_iff (x y : Prop) :
   @Under_iff x y -> x <-> y.
 Proof. by []. Qed.
 Definition Over_iff := Under_iff.
@@ -588,11 +588,12 @@ Proof. by []. Qed.
 End Under_iff.
 
 Register Under_iff as plugins.ssreflect.Under_iff.
-Register Under_from_iff as plugins.ssreflect.Under_from_iff.
+Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff.
+
+Definition over := (over_eq, over_iff).
 
 Ltac over :=
-  by [ apply: Under.under_done
-     | rewrite over
+  by [ apply: Under_eq.under_eq_done
      | apply: Under_iff.under_iff_done
-     | rewrite over_iff
+     | rewrite over
      ].
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index d60e3857b1..313b46ddc3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -347,7 +347,7 @@ let intro_lock ipats =
                let sigma, under_iff =
                  Ssrcommon.mkSsrConst "Under_iff" env sigma in
                let sigma, under_from_iff =
-                 Ssrcommon.mkSsrConst "Under_from_iff" env sigma in
+                 Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in
                let ty = EConstr.mkApp (under_iff,args) in
                let sigma, t = Evarutil.new_evar env sigma ty in
                sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|]))
@@ -359,9 +359,9 @@ let intro_lock ipats =
             Array.length args = 3 && is_app_evar sigma args.(2) ->
               Tactics.New.refine ~typecheck:true (fun sigma ->
                 let sigma, under =
-                  Ssrcommon.mkSsrConst "Under" env sigma in
+                  Ssrcommon.mkSsrConst "Under_eq" env sigma in
                 let sigma, under_from_eq =
-                  Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
+                  Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in
                 let ty = EConstr.mkApp (under,args) in
                 let sigma, t = Evarutil.new_evar env sigma ty in
                 sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
-- 
cgit v1.2.3


From 36488400952da5e12c8af451b1a936a34b26039d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 15:39:11 +0200
Subject: [ssr] under: optimization of the tactic for (under eq_bigl => *)

so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|].

Also: replace "by over." in the doc example with "over."
---
 plugins/ssr/ssrfwd.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 313b46ddc3..01d71aa96a 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -331,7 +331,15 @@ let is_app_evar sigma t =
       | _ -> false end
   | _ -> false
 
+let rec ncons n e = match n with
+  | 0 -> []
+  | n when n > 0 -> e :: ncons (n - 1) e
+  | _ -> failwith "ncons"
+
 let intro_lock ipats =
+  let hnf' = Proofview.numgoals >>= fun ng ->
+             Proofview.tclDISPATCH
+               (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
   let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
     Proofview.tclORELSE
       (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
@@ -372,7 +380,7 @@ let intro_lock ipats =
        end)
     end
   in
-  Ssripats.tclIPATssr ipats <*> lock_eq ()
+  hnf' <*> Ssripats.tclIPATssr ipats <*> lock_eq ()
 
 let pretty_rename evar_map term varnames =
   let rec aux term vars =
@@ -406,11 +414,6 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-let rec ncons n e = match n with
-  | 0 -> []
-  | n when n > 0 -> e :: ncons (n - 1) e
-  | _ -> failwith "ncons"
-
 let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
 
   (* total number of implied hints *)
-- 
cgit v1.2.3


From 92e2bb2bebc99b6a72ea0babad9a1c374129a0c0 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 16 Apr 2019 03:18:03 +0200
Subject: [ssr] set under's tactic argument at LEVEL 3

So if the underlying tactic "contains a ;" one should actually write:

    under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
---
 plugins/ssr/ssrparser.mlg | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 4286ace519..4d65fc81d1 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -86,6 +86,15 @@ GRAMMAR EXTEND Gram
   ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
 END
 
+(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
+ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
+| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
+END
+GRAMMAR EXTEND Gram
+  GLOBAL: ssrtac3arg;
+  ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+END
+
 {
 
 (* Lexically closed tactic for tacticals. *)
@@ -1065,6 +1074,13 @@ ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintar
 | [ ssrtacarg(arg) ] -> { mk_hint arg }
 END
 
+(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *)
+ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
+| [ "[" "]" ] -> { nullhint }
+| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
+| [ ssrtac3arg(arg) ] -> { mk_hint arg }
+END
+
 ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 END
@@ -2686,11 +2702,11 @@ TACTIC EXTEND under
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg nohint
     }
-  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhintarg(h) ] -> {
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhint3arg(h) ] -> {
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg h
     }
-  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *)
+  | [ "under" ssrrwarg(arg) "do" ssrhint3arg(h) ] -> { (* implicit "=> [*|*]" *)
     check_under_arg arg;
     Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
     }
-- 
cgit v1.2.3