From 6160f53e89800a785d773c4130b08fbe7c345651 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 6 Feb 2009 21:25:52 +0000
Subject: pushed evar reduction in kernel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation.ml')

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
-- 
cgit v1.2.3