diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 8779f4be37..b5cc4c51d8 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -49,7 +49,7 @@ pr (** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *) -Require Import BigNumPrelude ZArith CyclicAxioms +Require Import BigNumPrelude ZArith Ndigits CyclicAxioms DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic Wf_nat StreamMemo. @@ -248,10 +248,10 @@ pr Qed. Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww), - ZnZ.digits (nmake_op _ w_op n) = Pshiftl (ZnZ.digits w_op) n. + ZnZ.digits (nmake_op _ w_op n) = Pshiftl_nat (ZnZ.digits w_op) n. Proof. induction n. auto. - intros ww ww_op; simpl Pshiftl. rewrite <- IHn; auto. + intros ww ww_op. rewrite Pshiftl_nat_S, <- IHn; auto. Qed. Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww), @@ -331,7 +331,7 @@ pr " (** * Digits *) Lemma digits_make_op_0 : forall n, - ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits (dom_op Size)) (S n). + ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits (dom_op Size)) (S n). Proof. induction n. auto. @@ -341,15 +341,15 @@ pr " Qed. Lemma digits_make_op : forall n, - ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits w0_op) (SizePlus (S n)). + ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)). Proof. intros. rewrite digits_make_op_0. replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto). - rewrite Pshiftl_plus. auto. + rewrite Pshiftl_nat_plus. auto. Qed. Lemma digits_dom_op : forall n, - ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits w0_op) n. + ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits w0_op) n. Proof. do_size (destruct n; try reflexivity). exact (digits_make_op n). @@ -358,7 +358,7 @@ pr " Lemma digits_dom_op_nmake : forall n m, ZnZ.digits (dom_op (m+n)) = ZnZ.digits (nmake_op _ (dom_op n) m). Proof. - intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_plus. + intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_nat_plus. Qed. (** * Conversion between [zn2z (dom_t n)] and [dom_t (S n)]. |