From 0077eb84e8eda65e5ac327aecba7e3fbf77ee016 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 8 Nov 2013 19:03:58 +0000
Subject: Reverting the old LIFO behaviour of the notation finding algorithm.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17072 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.mli | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index e4a912494a..192e2b6e6c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -118,13 +118,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
 val interp_notation : Loc.t -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
+type notation_rule = interp_rule * interpretation * int option
+
 (** Return the possible notations for a given term *)
-val uninterp_notations : glob_constr ->
-      (interp_rule * interpretation * int option) list
-val uninterp_cases_pattern_notations : cases_pattern ->
-      (interp_rule * interpretation * int option) list
-val uninterp_ind_pattern_notations : inductive ->
-      (interp_rule * interpretation * int option) list
+val uninterp_notations : glob_constr -> notation_rule list
+val uninterp_cases_pattern_notations : cases_pattern -> notation_rule list
+val uninterp_ind_pattern_notations : 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