diff options
| author | Pierre Letouzey | 2018-03-14 10:23:51 +0100 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:52 -0400 |
| commit | 64cb952f3fcf41c25a66a92bd124bba82e6db3f6 (patch) | |
| tree | 79e72103750c5be9e5c74e98c2a7ac3c25051b23 /interp | |
| parent | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (diff) | |
Notation: no more chains of prim_token_interpreter
This cleanup prepares for forthcoming synchronization of prim_token_interpreter
wrt to Summary. These chains of prim_token_interpreter were anyway never used,
only one interpreter was declared per numeral scope.
After sync wrt Summary, we'll anyway be able to backtrack to a previous
interpreter.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 625d072b9f..36d4b0aa15 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -319,12 +319,7 @@ let prim_token_interpreter_tab = (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) let add_prim_token_interpreter sc interp = - try - let cont = Hashtbl.find prim_token_interpreter_tab sc in - Hashtbl.replace prim_token_interpreter_tab sc (interp cont) - with Not_found -> - let cont = (fun ?loc _p -> raise Not_found) in - Hashtbl.add prim_token_interpreter_tab sc (interp cont) + Hashtbl.replace prim_token_interpreter_tab sc interp let declare_prim_token_interpreter sc interp (patl,uninterp,b) = declare_scope sc; @@ -351,8 +346,8 @@ type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) - | p -> cont ?loc p) + (fun ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) + | _ -> raise Not_found) (patl, (fun r -> match uninterp r with | None -> None | Some (n,s) -> Some (Numeral (n,s))), inpat) @@ -360,13 +355,14 @@ let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) - | p -> cont ?loc p) + (fun ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) + | _ -> raise Not_found) (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc - (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p) + (fun ?loc -> function String s -> delay dir interp ?loc s + | _ -> raise Not_found) (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = |