diff options
| -rw-r--r-- | interp/notation.ml | 33 | ||||
| -rw-r--r-- | interp/notation.mli | 11 |
2 files changed, 10 insertions, 34 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 737687adc3..fa428f1b3b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -236,41 +236,18 @@ let key_compare k1 k2 = match k1, k2 with module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -module InterpretationOrd = -struct - type t = interp_rule * interpretation * int option - let compare (ir1, i1, io1) (ir2, i2, io2) = - let cmp = compare_interp_rule ir1 ir2 in - if cmp = 0 then - let cmp' = Pervasives.compare i1 i2 in (* FIXME: to be explicitely written *) - if cmp' = 0 then - match io1, io2 with - | None, None -> 0 - | None, Some _ -> -1 - | Some x, Some y -> Pervasives.compare x y - | Some _, None -> 1 - else - cmp' - else - cmp -end - -module InterpretationSet = Set.Make (InterpretationOrd) -(** ppedrot: We changed the semantics here. Before it was a FIFO stack, now it - is an ordered set with an badly defined comparison... *) +type notation_rule = interp_rule * interpretation * int option let keymap_add key interp map = - let old = try KeyMap.find key map with Not_found -> InterpretationSet.empty in - KeyMap.add key (InterpretationSet.add interp old) map + let old = try KeyMap.find key map with Not_found -> [] in + KeyMap.add key (interp :: old) map let keymap_find key map = - try - let set = KeyMap.find key map in - InterpretationSet.elements set + try KeyMap.find key map with Not_found -> [] (* Scopes table : interpretation -> scope_name *) -let notations_key_table = ref (KeyMap.empty : InterpretationSet.t KeyMap.t) +let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) let prim_token_key_table = Hashtbl.create 7 let glob_prim_constr_key = function 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 |