diff options
| author | Pierre-Marie Pédrot | 2016-11-06 03:23:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:25:28 +0100 |
| commit | b365304d32db443194b7eaadda63c784814f53f1 (patch) | |
| tree | 95c09bc42f35a5d49af5aeb16a281105e674a824 /ltac | |
| parent | b113f9e1ca88514cd9d94dfe90669a27689b7434 (diff) | |
Evarconv API using EConstr.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 80307ce8e3..076e4c05e4 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -454,7 +454,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.the_conv_x env (EConstr.of_constr x) (EConstr.of_constr y) evd in let _, pbs' = Evd.extract_all_conv_pbs evd' in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None |