prim notations backtrackable, their declarations now in two parts (API change)

 The first part (e.g. register_bignumeral_interpretation) deals only with
 the interp/uninterp closures. It should typically be done as a side
 effect during a syntax plugin loading. No prim notation are active yet
 after this phase.

 The second part (enable_prim_token_interpretation) activates the prim
 notation. It is now correctly talking to Summary and to the LibStack.
 To avoid "phantom" objects in libstack after a mere Require, this
 second part should be done inside a Mltop.declare_cache_obj

 The link between the two parts is a prim_token_uid (a string), which
 should be unique for each primitive notation. When this primitive
 notation is specific to a scope, the scope_name could be used as uid.

 Btw, the list of "patterns" for detecting when an uninterpreter should
 be considered is now restricted to a list of global_reference
 (inductive constructors, or injection functions such as IZR).
 The earlier API was accepting a glob_constr list, but was actually
 only working well for global_reference.

 A minimal compatibility is provided (declare_numeral_interpreter),
 but is discouraged, since it is known to store uncessary objects
 in the libstack.

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
new file mode 100644
index 0000000000..ca8cba67d5
--- /dev/null
+++ b/test-suite/interactive/PrimNotation.v
@@ -0,0 +1,18 @@
+(* Until recently, the Notation.declare_numeral_notation wasn't synchronized
+   w.r.t. backtracking. This should be ok now.
+   This test is pretty artificial (we must declare Z_scope for this to work).
+*)
+
+Delimit Scope Z_scope with Z.
+Open Scope Z_scope.
+Check 0.
+(* 0 : nat *)
+Require BinNums.
+Check 0.
+(* 0 : BinNums.Z *)
+Back 2.
+Check 0.
+(* Expected answer: 0 : nat *)
+(* Used to fail with:
+Error: Cannot interpret in Z_scope without requiring first module BinNums.
+*)