diff options
| author | Maxime Dénès | 2014-04-28 20:34:44 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 18:05:00 -0400 |
| commit | dcd3ec87a3bf26fab2856af720bbea5b0209cae5 (patch) | |
| tree | c92cece474e78d76ab7b4f6e6c67cb190da9aadf /checker/type_errors.ml | |
| parent | cc001c2b8d5ababee585cc43e07e0f9089b5d40e (diff) | |
Refine check_is_subterm.
Following Bruno's suggestion, we check if the tree expected for the recursive
argument is included in the one which is inferred. This check is probably
not necessary in the current state of affairs, but might become so after
further extensions of the guard condition.
Diffstat (limited to 'checker/type_errors.ml')
0 files changed, 0 insertions, 0 deletions