From 93a65415ff582d2ceb5bb9d994edaa6068da8280 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 12:14:59 +0100
Subject: Pre-isolating a notation test to avoid interferences.

---
 interp/notation.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 734198bbf6..40b7f2c2c9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -214,9 +214,9 @@ val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
 type notation_rule = interp_rule * interpretation * int option
 
 (** Return the possible notations for a given term *)
-val uninterp_notations : 'a glob_constr_g -> notation_rule list
-val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list
-val uninterp_ind_pattern_notations : inductive -> notation_rule list
+val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list
+val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list
 
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
-- 
cgit v1.2.3