diff options
| author | Pierre-Marie Pédrot | 2015-07-28 17:00:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-28 17:29:29 +0200 |
| commit | 0621891c4ba7606d91e614408378af17d3b0aee3 (patch) | |
| tree | 7e6e55ae8173fd1d28c9d2b3bff6a0e2eb9cfca3 /kernel/nativecode.ml | |
| parent | c544167584024513648b23052db1aa9dcd993c01 (diff) | |
Fix for bug #4280: "decide equality produces terms that don't compute well".
We postpone the rewriting of hypothesis until we actually commit to one
branch instead of doing it upfront.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions