diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 8495b623f..b0645744b 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -269,7 +269,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2 + Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) |