diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index fcb2b6f5..776fff79 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 11512 2008-10-27 12:28:36Z herbelin $ *) +(* $Id: notation.ml 11897 2009-02-09 19:28:02Z barras $ *) (*i*) open Util @@ -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 |