diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:15:06 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:15:06 +0200 |
commit | 1c8ed18d5f67d7d5656342584b8dcf8a441cb87f (patch) | |
tree | ce90c93341c58e82813da8b1a567ce6a3f3ed424 /interp/constrexpr_ops.mli | |
parent | 4f742e14441581ece247d33020055f15732f126b (diff) |
Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
Diffstat (limited to 'interp/constrexpr_ops.mli')
0 files changed, 0 insertions, 0 deletions