diff options
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 |