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 b6c1bfa40e..bb17eda2c9 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -422,7 +422,7 @@ let find_class_scope cl = Gmap.find cl !class_scope_map let find_class t = - let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in + let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in match kind_of_term t with | Var id -> CL_SECVAR id | Const sp -> CL_CONST sp @@ -435,7 +435,7 @@ let find_class t = (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_scope t = - match kind_of_term (Reductionops.whd_betaiotazeta t) with + match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with | Prod (_,t,u) -> let sc = try Some (find_class_scope (find_class t)) with Not_found -> None in |