diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 076570c8a..f36294f73 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -11,7 +11,7 @@ open CErrors open Util open Pp open Names -open Term +open Constr open Libnames open Globnames open Constrexpr @@ -653,7 +653,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 (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with + match Constr.kind (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 |