diff options
| author | Hugo Herbelin | 2015-06-23 16:59:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-06-23 19:09:11 +0200 |
| commit | f39a711555d76926b6e0ddf5480a6411abc862a9 (patch) | |
| tree | 51d3f2ae8c87129966cd75919201224f11b61999 /kernel/cbytecodes.ml | |
| parent | 47860acaffe6017c3b5165d6442f9fbf5c524495 (diff) | |
Fixing incompatibility introduced with simpl in commit 364decf59c1 (or
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions