diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-03-17 17:53:25 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-03-17 18:05:59 +0100 |
| commit | 82b371aceb1ef6b1e15bdace2cf142e65724a3c6 (patch) | |
| tree | 9ee71f0380702f159f68b2b2651526eb5c60c559 /pretyping/tacred.mli | |
| parent | 4849c8eb1b7a386d2abcbc80c40de34b0a69b8ea (diff) | |
Fix #4623: set tactic too weak with universes (regression)
The regression was introduced by efa1c32a4d178, which replaced
unification by conversion when looking for more occurrences of a
subterm. The conversion function called was not the right one, as it
was not inferring constraints.
Diffstat (limited to 'pretyping/tacred.mli')
0 files changed, 0 insertions, 0 deletions