diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da30bd9c9..6fd2f7c2bc 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2055b25ff4..ea54973fdc 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -449,7 +449,7 @@ let evd_convertible env evd x y = 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 evd' = Evarconv.unify_delay env evd x y in let _, pbs' = Evd.extract_all_conv_pbs evd' in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 552a4048b1..fb99b87108 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a = loop 0 let unif_HO env ise p c = - try Evarconv.the_conv_x env p c ise + try Evarconv.unify_delay env ise p c with Evarconv.UnableToUnify(ise, err) -> raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) |