From e4a09fc480f512f54d5e7ba05d7e408dc5817a46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Jul 2017 17:12:59 +0200
Subject: Selecting which notation to print based on current stack of scope.

See discussion on coq-club starting on 23 August 2016.

An open question: what priority to give to "abbreviations"?
---
 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 2066d346fe..7d055571c8 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -124,9 +124,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
 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 : local_scopes -> 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list
+val uninterp_ind_pattern_notations : local_scopes -> 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