From 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 11:03:29 -0400
Subject: 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.
---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

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)}
 
-- 
cgit v1.2.3