[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

1 files changed, 26 insertions, 1 deletions

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