From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index d264a1904..29e5a3bfd 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -615,7 +615,7 @@ let find_scope_class_opt = function (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_classes t = - match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t)) with + match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with | Prod (_,t,u) -> let cl = try Some (compute_scope_class t) with Not_found -> None in cl :: compute_arguments_classes u -- cgit v1.2.3