diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 0556191be8..47c78ae5c2 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -438,14 +438,22 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) +let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = + pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') + +let problem_inclusion x y = + List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x + let evd_convertible env evd x y = try - let evd = Evarconv.the_conv_x env x y evd in (* Unfortunately, the_conv_x might say they are unifiable even if some - unsolvable constraints remain, so we check them here *) - let evd = Evarconv.consider_remaining_unif_problems env evd in - let () = Evarconv.check_problems_are_solved env evd in - Some evd + unsolvable constraints remain, so we check that this unification + does not introduce any new problem. *) + let _, pbs = Evd.extract_all_conv_pbs evd in + let evd' = Evarconv.the_conv_x env x y evd in + let _, pbs' = Evd.extract_all_conv_pbs evd' in + if evd' == evd || problem_inclusion pbs' pbs then Some evd' + else None with e when CErrors.noncritical e -> None let convertible env evd x y = @@ -581,9 +589,9 @@ let general_rewrite_unif_flags () = let core_flags = { rewrite_core_unif_flags with Unification.modulo_conv_on_closed_terms = Some ts; - Unification.use_evars_eagerly_in_conv_on_closed_terms = false; + Unification.use_evars_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; - Unification.modulo_delta_types = ts; + Unification.modulo_delta_types = full_transparent_state; Unification.modulo_betaiota = true } in { Unification.core_unify_flags = core_flags; |