This replaces opA, opC, opAC, opCA, ... and any combinations of them

- Right now the rewrite relies on an rather efficient computation
  of perm_eq using a "spaghetti sort" in O(n log n)
- Wrongly formed AC statements send error messages showing the
  discrepancy between LHS and RHS patterns.

 Usage :
   rewrite [pattern](AC operator pattern-shape re-ordering)
   rewrite [pattern](ACl operator re-ordering)

 - pattern is optional, as usual,
 - operator must have a canonical Monoid.com_law structure
   (additions, multiplications, conjunction and disjunction do)
 - pattern-shape is expressed using the syntax
      p := n | p * p'
      where "*" is purely formal
        and n > 0 is number of left associated symbols
   examples of pattern shapes:
   + 4 represents (n * m * p * q)
   + (1*2) represents (n * (m * p))
 - re-ordering is expressed using the syntax
     s := n | s * s'
   where "*" is purely formal and n is the position in the LHS

 If the ACl variant is used, the pattern-shape defaults to the
 pattern fully associated to the left i.e. n i.e (x * y * ...)

 Examples of re-orderings:
 - ACl op ((0*1)*2) is the identity (and should fail to rewrite)
 - opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1)
 - opCA == AC op (2*1) (0*1*2)
 - rewrite opCA -opA == rewrite (ACl op (0*(2*1))
 - opACA == AC (2*2) ((0*2)*(1*3))

The content of this file is similar to that of ssrfun.v and aims to
increase compatibility with Coq 8.6+ for third-party libraries that
depend on both math-comp and ssrmatching.v

Close #63

it is to the caller of coq_makefile to eventually add .ml4 files