diff options
| author | Jason Gross | 2018-08-23 11:03:29 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:54 -0400 |
| commit | 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 (patch) | |
| tree | 41abb312099ed7481e16462107f3790b4295f8fb /interp | |
| parent | 548976ac825298f27e6be00bbbb1be0752568f6f (diff) | |
Make Numeral Notation follow Import, not Require
Because that's the sane thing to do.
This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.
We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 56d6acbdae..d6bd62e121 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -431,8 +431,8 @@ let subst_prim_token_interpretation (subs,infos) = 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); cache_function = cache_prim_token_interpretation; - load_function = (fun _ -> cache_prim_token_interpretation); subst_function = subst_prim_token_interpretation; classify_function = (fun o -> Substitute o)} |