diff options
| author | Hugo Herbelin | 2014-12-09 17:44:57 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-10 15:49:52 +0100 |
| commit | d50c25ca21b9fab6da6301201fed5be32449f88f (patch) | |
| tree | 90b494e57e62160dffc8c892234343163240d180 /pretyping | |
| parent | 3e935b3af6ab35ed0bda93087cd784ea1427b536 (diff) | |
Fixing orientation of postponed subtyping problems.
In the case of conversion, postponing by preserving the
initial orientation.
Was wrong from its initial version in Jan 2014, but was not visible
because evar-evar subtyping was approximated by evar-evar conversion.
Thanks to Enrico for a very short example highlighting the problem. In
particular, this fixes Ergo.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index d0a7e39822..cb5673c2ea 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -120,9 +120,9 @@ let test_success conv_algo env evd c c' rhs = let add_conv_oriented_pb (pbty,env,t1,t2) evd = match pbty with - | Some true -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd + | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd - | None -> add_conv_pb (Reduction.CONV,env,t2,t1) evd + | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd (*------------------------------------* * Restricting existing evars * |