From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- plugins/quote/quote.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/quote') 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) -- cgit v1.2.3