diff options
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 948d624a2..88ae4695b 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 t) with + match kind_of_term (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 |