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 dae1cc9f1..46600cdd7 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -284,7 +284,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = match find_rel ctype with | Some c -> Some c | None -> - let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) + let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None |