diff options
Diffstat (limited to 'plugins/quote/quote.ml')
| -rw-r--r-- | plugins/quote/quote.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index c6376727a..afc7e6665 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -249,8 +249,8 @@ let compute_ivs f cs gl = (* Then we test if the RHS is the RHS for variables *) else begin match decompose_app bodyi with | vmf, [_; _; a3; a4 ] - when isRel a3 && isRel a4 && is_conv vmf - (Lazy.force coq_varmap_find)-> + when isRel a3 && isRel a4 && is_conv (EConstr.of_constr vmf) + (EConstr.of_constr (Lazy.force coq_varmap_find)) -> v_lhs := Some (compute_lhs (snd (List.hd args3)) i nargsi) |