From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 948d624a27..88ae4695b8 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 t) with
+  match kind_of_term (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
-- 
cgit v1.2.3


From ce2b509734f3b70494a0a35b0b4eda593c1c8eb6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Nov 2016 19:07:16 +0100
Subject: Classops API using EConstr.

---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 88ae4695b8..d264a19047 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -585,7 +585,7 @@ let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
 let compute_scope_class t =
-  let (cl,_,_) = find_class_type Evd.empty t in
+  let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in
   cl
 
 module ScopeClassOrd =
-- 
cgit v1.2.3


From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index d264a19047..29e5a3bfd8 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
-- 
cgit v1.2.3