diff options
| author | Hugo Herbelin | 2017-10-25 12:24:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-10-30 21:12:32 +0100 |
| commit | 424c682a1f9d2dfcac28318bc38c4602c180f5dc (patch) | |
| tree | 6968d6c2c29946ea651c60d2ef3a1548dee4451a /dev/header | |
| parent | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (diff) | |
Fixing #2881 ("change with" failing in an Ltac definition).
We fix by interpreting the pattern in "change pat with term" in strict
mode by using the same interning code as for "match goal" (even if the
pattern is dropped afterwards).
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions