diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-02 20:40:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 01:35:09 +0100 |
| commit | 28a2641df29cd7530c3ebe329dc118ba3f444b10 (patch) | |
| tree | 96e334e8aa6b9227892818a707d7ac09fc99630d /interp/notation.ml | |
| parent | 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae (diff) | |
Fixing generic hashes and replacing them with proper ones.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 262cbab2f..6e5ac5f33 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -254,7 +254,8 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = Hashtbl.create 7 + +let prim_token_key_table = ref KeyMap.empty let glob_prim_constr_key = function | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref) @@ -309,8 +310,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = declare_scope sc; add_prim_token_interpreter sc interp; List.iter (fun pat -> - Hashtbl.add prim_token_key_table - (glob_prim_constr_key pat) (sc,uninterp,b)) + prim_token_key_table := KeyMap.add + (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) patl let mkNumeral n = Numeral n @@ -487,7 +488,7 @@ let availability_of_notation (ntn_scope,ntn) scopes = let uninterp_prim_token c = try let (sc,numpr,_) = - Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in + KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in match numpr c with | None -> raise Notation_ops.No_match | Some n -> (sc,n) @@ -496,8 +497,8 @@ let uninterp_prim_token c = let uninterp_prim_token_ind_pattern ind args = let ref = IndRef ind in try - let (sc,numpr,b) = Hashtbl.find prim_token_key_table - (RefKey (canonical_gr ref)) in + let k = RefKey (canonical_gr ref) in + let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in @@ -510,7 +511,7 @@ let uninterp_prim_token_ind_pattern ind args = let uninterp_prim_token_cases_pattern c = try let k = cases_pattern_key c in - let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in + let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in if not b then raise Notation_ops.No_match; let na,c = glob_constr_of_closed_cases_pattern c in match numpr c with |