diff options
| author | Hugo Herbelin | 2020-02-23 22:18:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-27 14:41:11 +0100 |
| commit | 830cdec8704d14bca0b3db390ecb9661e01eb106 (patch) | |
| tree | e3ff5ae4739551f6cf5f46f5a32aa1776cf77611 /dev | |
| parent | bc500cd96c7142cda5ad6f992c7c656d6499b0c6 (diff) | |
Helping issue #11659 by leaving only the Cast hack in the grammar.
We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions