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 /theories/Numbers | |
| 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 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index bd4f0279d4..ec480bb1eb 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -23,8 +23,6 @@ Require Import Zpow_facts. Require Import CyclicAxioms. Require Import ROmega. -Declare ML Module "int31_syntax_plugin". - Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -128,7 +126,7 @@ Section Basics. Lemma nshiftl_S_tail : forall n x, nshiftl x (S n) = nshiftl (shiftl x) n. - Proof. + Proof. intros n; elim n; simpl; intros; now f_equal. Qed. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 9f8da831d8..39af62c32f 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,6 +15,8 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. +Declare ML Module "int31_syntax_plugin". + (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer |