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 | |
| 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')
| -rw-r--r-- | pretyping/unification.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9b6e856b8..cd0bbfa30 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1532,8 +1532,9 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with - | Some (evd,c1,_) as x, Some (_,c2,_) -> - if is_conv env sigma c1 c2 then x else raise (NotUnifiable None) + | Some (evd,c1,x), Some (_,c2,_) -> + let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in + if b then Some (evd, c1, x) else raise (NotUnifiable None) | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in |