Actually abstracting large nat constants

[proux01]

Instead of parsing large nat constants as Nat.of_uint <decimal encoding> and just leaving the term unevaluated and ready to blow up at next computation or unification, we hide the definition of Nat.of_uint behind a module type, thus preventing any accidental blowup. The actual definition can still be recovered by a simple rewriting.

(* previously *)
Goal 12000 = 6000 + 6000.
(* Warning: To avoid stack overflow, large numbers in nat are interpreted as applications of Nat.of_num_uint. [abstract-large-number,numbers,default] [x3] *)
Proof.
(* Nat.of_num_uint 12000%uint = Nat.of_uint 6000%uint + Nat.of_uint 6000%uint *)
vm_compute.
(* 12000 = 12000 *)
reflexivity.
Qed.

(* this PR *)
Goal 12000 = 6000 + 6000.
Proof.
(* Nat.Of_uint.locked 12000%uint = Nat.Of_uint.locked 6000%uint + Nat.Of_uint.locked 6000%uint *)
vm_compute.
(* essentially no change *)
Fail reflexivity.
Search Nat.Of_uint.locked.
(* Nat.Of_uint.unlock: Nat.Of_uint.locked = Nat.of_uint *)
rewrite Nat.Of_uint.unlock.
(* Nat.of_uint 12000%uint = Nat.of_uint 6000%uint + Nat.of_uint 6000%uint *)
vm_compute.
(* 12000 = 12000 *)
reflexivity.
Qed.

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

• TODO coqutil
• TODO engine_bench
• TODO paramcoq
• TODO equations tests
• TODO mathcomp tests

[proux01]

@silene you're probably the expert here, do you think we should do this? If yes, I'll complete the PR / do the few overlays and cleanup the adhoc abstract after and warning after options of Number Notation, for which this was the only use. Otherwise, let's just drop this experiment.

[silene]

I am not convinced. I understand where this is coming from, but I am not sure there is a proper solution. It might be better to not fix it, so that users encounter hard failures as early as possible, rather than to hide the issue and delay it further and further. It is important that users understand that there is an inherent cost to using unary integers.