diff options
| author | Pierre-Marie Pédrot | 2016-03-20 16:37:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 16:37:09 +0100 |
| commit | 2349d740caa4d9248ba5485aebbcce9ec18d3fd2 (patch) | |
| tree | 18a3bc56f498049b28bc0d7a3266c8e6f5dbc272 /pretyping | |
| parent | 1890a2cdc0dcda7335d7f81fc9ce77c0debc4324 (diff) | |
| parent | 09c2011fbdbb2ac1ce33e5abe52d93b907b21a3c (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 1 | ||||
| -rw-r--r-- | pretyping/unification.ml | 5 |
2 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f77e3312bb..489a8a729d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -143,6 +143,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = try match kind_of_term t2 with Prod (_,a,b) -> (* assert (l2=[]); *) + let _, a, b = destProd (Evarutil.nf_evar sigma t2) in if dependent (mkRel 1) b then raise Not_found else lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 15e8022af0..a7b415552a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1555,8 +1555,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 |