diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-16 22:53:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-16 22:53:10 +0200 |
| commit | fdd6a17b272995237c9f95fc465bb1ff6871bedc (patch) | |
| tree | 81d478b093830b4e144303f15586d41fb9c1fcf9 /engine/namegen.ml | |
| parent | e0d36d4afd7f38eb6816b92d03ecc2d2f7dc8d3f (diff) | |
Refining 71def2f8 on too strong occur-check limiting evar-evar
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
Diffstat (limited to 'engine/namegen.ml')
0 files changed, 0 insertions, 0 deletions