diff options
| author | Matthieu Sozeau | 2014-09-17 16:20:50 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 17:57:08 +0200 |
| commit | 17f68d403d248e899efbb76afeed169232946ecf (patch) | |
| tree | 5eb60ef760ea388670612c4c0ece96a43e7dad87 /pretyping/patternops.ml | |
| parent | cc6afad3bcfaa5b7fa57c8cd3035fe520c93afda (diff) | |
Fix bug #3633 properly, by delaying the interpetation of constrs in
apply f, g,... so that apply f, g. succeeds when apply f; apply g
does. It just mimicks the behavior of rewrite foo bar.
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions