#63 (May 2, 2020, 8:47:00 AM)

Started by GitHub push by gasche

• origin/trunk

1. matching: matcher_* take Simple.pattern arguments (commit: 67c56e6) (details / githubweb)
2. matching: specialize_matrix uses non-empty rows (commit: 97caf28) (details / githubweb)
3. matching: consolidate all matcher_ functions in a single matcher_head (commit: 0f5a1c4) (details / githubweb)
4. matching: refine the types in Context.ctx_matcher (commit: 387955e) (details / githubweb)
5. matching: finally, merge matcher and Context.ctx_matcher (commit: a26e509) (details / githubweb)
6. Changes (commit: ae4621c) (details / githubweb)
7. matching: use heads in the make_*_matching specialization calls (commit: ac1243c) (details / githubweb)
8. [minor] matching.ml: tune ~scopes handling (commit: 50fdc06) (details / githubweb)
9. matching: add a comment suggested by Florian Angeletti's review (commit: 3527653) (details / githubweb)
10. parmatch: normalize_pat is not used anymore (commit: 3903f9f) (details / githubweb)