diff options
| author | ppedrot | 2013-11-08 19:03:58 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-08 19:03:58 +0000 |
| commit | 0077eb84e8eda65e5ac327aecba7e3fbf77ee016 (patch) | |
| tree | 5f6dff632ce4b2959b7f34280ff1c818f1eda558 /interp/notation.mli | |
| parent | dea497aa1846f19693a4ae9c88497e4484d1fba0 (diff) | |
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
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 11 |
1 files changed, 5 insertions, 6 deletions
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 |