diff options
| author | Matthieu Sozeau | 2018-10-17 18:04:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:19:38 +0100 |
| commit | 78b51f541d0107f06c21fc1260aae2ab9f7229c5 (patch) | |
| tree | 07fef2f70c6f67a08bf07c85b2690fdee9ec35c7 /plugins/ltac | |
| parent | 1c60cbedfd8a5e64bfa95dfb9a9497e278458c30 (diff) | |
Change interfaces of evarconv as suggested by Enrico.
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |