aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml2
1 files changed, 1 insertions, 1 deletions
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