diff options
| author | Maxime Dénès | 2013-12-26 15:52:50 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 17:34:57 -0400 |
| commit | 286abd141d415a621cc8ea98055d8dc744c8b752 (patch) | |
| tree | e3811f8c42d965af5870b412b0499cb0ff89c3cd /kernel/type_errors.ml | |
| parent | 9b272a861bc3263c69b699cd2ac40ab2606543fa (diff) | |
Refining match subterm and commutative cut rules. The parameters that are
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions