diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 12 | ||||
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 |
3 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 307edcc89a..9f1b118fb3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -121,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false let test_success conv_algo env evd c c' rhs = is_success (conv_algo env evd c c' rhs) -let add_conv_oriented_pb (pbty,env,t1,t2) evd = +let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = match pbty with - | 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,t1,t2) evd + | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd + | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd + | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd (*------------------------------------* * Restricting existing evars * @@ -1111,13 +1111,13 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a with CannotProject (evd,ev2) -> try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let pbty = if force then None else pbty in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 9313e22320..4e38bd4e66 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -779,7 +779,9 @@ let merge_universe_context evd uctx' = let set_universe_context evd uctx' = { evd with universes = uctx' } -let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} +let add_conv_pb ?(tail=false) pb d = + if tail then {d with conv_pbs = d.conv_pbs @ [pb]} + else {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (find d evk).evar_source diff --git a/pretyping/evd.mli b/pretyping/evd.mli index cf6ba07c60..48704f75bb 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -397,7 +397,7 @@ type clbinding = (** Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : evar_constraint -> evar_map -> evar_map +val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> |