diff options
| author | Pierre-Marie Pédrot | 2020-09-22 14:19:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:20:10 +0200 |
| commit | 0590764209dcb8540b5292aca38fe2df38b90ab9 (patch) | |
| tree | cede5a6e0a7fabcfd55f7635604493876821afc6 /pretyping/evarconv.ml | |
| parent | 2b91a8989687e152f7120aa6c907ffeba8495bab (diff) | |
Same little game with Projection.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6a668e79e8..08cb173442 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -387,7 +387,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> - if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) + if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, @@ -429,7 +429,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> - if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) + if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> |