diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 7 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 6291a88bb0..0afbb9cd62 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -206,7 +206,7 @@ let classify_scope (local,_,_ as o) = let inScope : bool * bool * scope_item -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; - open_function = open_scope; + open_function = simple_open open_scope; subst_function = subst_scope; discharge_function = discharge_scope; classify_function = classify_scope } @@ -980,9 +980,12 @@ let subst_prim_token_interpretation (subs,infos) = let classify_prim_token_interpretation infos = if infos.pt_local then Dispose else Substitute infos +let open_prim_token_interpretation i o = + if Int.equal i 1 then cache_prim_token_interpretation o + let inPrimTokenInterp : prim_token_infos -> obj = declare_object {(default_object "PRIM-TOKEN-INTERP") with - open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o); + open_function = simple_open open_prim_token_interpretation; cache_function = cache_prim_token_interpretation; subst_function = subst_prim_token_interpretation; classify_function = classify_prim_token_interpretation} diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 767c69e3b6..d6aa527f4d 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -71,7 +71,7 @@ let in_syntax_constant : (bool * syndef) -> obj = declare_object {(default_object "SYNDEF") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; - open_function = open_syntax_constant; + open_function = todo_filter open_syntax_constant; subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } |