diff options
| author | Hugo Herbelin | 2018-09-03 17:52:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-03 17:52:20 +0200 |
| commit | f61ee79e4a6db070e3bf26f76e8bdb42b85c3a72 (patch) | |
| tree | 930037d2d2d21e3ac8a986f718b64719de64c099 /theories/Numbers/Cyclic | |
| parent | c880e9e01d57eb4beca561e209839caa66d38742 (diff) | |
| parent | f7cf1f7e6f7f010e57e925e2fbb76a52fef74068 (diff) | |
Merge PR #8064: Numeral notation (revisited again)
Diffstat (limited to 'theories/Numbers/Cyclic')
| -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 |