diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-09 20:04:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-09 20:04:43 +0000 |
| commit | 97e46c18bb207726cfc42f25fc901772579d7057 (patch) | |
| tree | 89ec6b1fa38fd5341ea8c8039804634632a92c1a /theories/Numbers/Natural/BigN/BigN.v | |
| parent | 015e33fb137c89ba96b2806f828cd47341c3bd92 (diff) | |
NMake : another round of heavy rework
- generic iterator [iter] factorized in the same way as [same_level]
- as a consequence, remaining operations [mul] [compare] [div_gt]
are now defined and proved in a short and nice way and moved to
NMake.v.
- lots of other simplifications / factorisations in NMake_gen.
This file is still macro-generated, but is much shorter,
and the major part of it is now invariant.
- As advised by B. Gregoire, try to (re)create clever partial
applications in code of operators, in order to avoid projecting
ZnZ fields all the time in base cases. Case 0 can still be improved,
but it's already better this way :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index ad7d322ab..2bb79280c 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -40,7 +40,7 @@ Notation bigN := BigN.t. Delimit Scope bigN_scope with bigN. Bind Scope bigN_scope with bigN. Bind Scope bigN_scope with BigN.t. -Bind Scope bigN_scope with BigN.t_. +Bind Scope bigN_scope with BigN.t'. (* Bind Scope has no retroactive effect, let's declare scopes by hand. *) Arguments Scope BigN.to_Z [bigN_scope]. Arguments Scope BigN.succ [bigN_scope]. |