[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.

2 files changed, 45 insertions, 44 deletions

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