[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

0 files changed, 0 insertions, 0 deletions