diff options
| author | Pierre-Marie Pédrot | 2015-09-22 15:40:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-22 15:57:01 +0200 |
| commit | e1146f44229b380a8f52c67e1a51df4d6c03086e (patch) | |
| tree | 41a3d1cc643ae214c522dec24955f69bb4011422 /kernel/type_errors.ml | |
| parent | 7c5356ed487dcf7cf915e5471832852f7002586c (diff) | |
Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.
We purge the environment given to the morphism searcher from all dependencies
on the considered variable. I hope it is not too costly.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions