diff options
| author | Pierre-Marie Pédrot | 2015-11-12 14:14:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-12 15:10:30 +0100 |
| commit | 0c11bc39927c7756a0e3c3a6c445f20d0daaad7f (patch) | |
| tree | 39a53913a6ff2deb6f5597507780d9479ce62488 /dev/doc | |
| parent | db002583b18c8742c0cd8e1a12305166b6b791ce (diff) | |
Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions