Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10299 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 222 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
deleted file mode 100644
index 349892b99..000000000
--- a/theories/NArith/BinNat.v
+++ /dev/null
@@ -1,222 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
-
-(*i i*)
-
-Require Import BinPos.
-Require Import NBinDefs.
-
-(*Unset Boxed Definitions.*)
-
-Delimit Scope N_scope with N.
-Bind Scope N_scope with N.
-Open Local Scope N_scope.
-
-(** Operations *)
-
-Notation N := N.
-Notation N0 := N0.
-Notation Npos := Npos.
-Notation Nsucc := succ.
-Notation Npred := pred.
-Notation Nplus := plus.
-Notation Nminus := minus.
-Notation Nmult := times.
-Notation Ncompare := Ncompare.
-Notation Nlt := lt.
-Notation Nle := le.
-Definition Ngt (x y : N) := (Ncompare x y) = Gt.
-Definition Nge (x y : N) := (Ncompare x y) <> Lt.
-Notation Nmin := min.
-Notation Nmax := max.
-
-(* If the notations for operations above had been actual definitions, the
-arguments scopes would have been N_scope due to the instruction "Bind Scope
-N_scope with N". However, the operations were declared in NBinary, where
-N_scope has not yet been declared. Therefore, we need to assign the
-arguments scopes manually. Note that this has to be done before declaring
-infix notations below. Ngt and Nge get their scope from the definition. *)
-
-Arguments Scope succ [N_scope].
-Arguments Scope pred [N_scope].
-Arguments Scope plus [N_scope N_scope].
-Arguments Scope minus [N_scope N_scope].
-Arguments Scope times [N_scope N_scope].
-Arguments Scope NBinDefs.Ncompare [N_scope N_scope].
-Arguments Scope lt [N_scope N_scope].
-Arguments Scope le [N_scope N_scope].
-Arguments Scope min [N_scope N_scope].
-Arguments Scope max [N_scope N_scope].
-
-Infix "+" := Nplus : N_scope.
-Infix "-" := Nminus : N_scope.
-Infix "*" := Nmult : N_scope.
-Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
-Infix "<=" := Nle : N_scope.
-Infix "<" := Nlt : N_scope.
-Infix ">=" := Nge : N_scope.
-Infix ">" := Ngt : N_scope.
-
-(** Peano induction and recursion *)
-
-Notation Nrect := Nrect.
-Notation Nrect_base := Nrect_base.
-Notation Nrect_step := Nrect_step.
-Definition Nind (P : N -> Prop) := Nrect P.
-Definition Nrec (P : N -> Set) := Nrect P.
-
-Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
-Proof.
-intros P a f; unfold Nrec; apply Nrect_base.
-Qed.
-
-Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n).
-Proof.
-intros P a f; unfold Nrec; apply Nrect_step.
-Qed.
-
-(** Properties of successor and predecessor *)
-
-Notation Npred_succ := pred_succ.
-Notation Nsucc_0 := neq_succ_0.
-Notation Nsucc_inj := succ_inj.
-
-(** Properties of addition *)
-
-Notation Nplus_0_l := plus_0_l.
-Notation Nplus_0_r := plus_0_r.
-Notation Nplus_comm := plus_comm.
-Notation Nplus_assoc := plus_assoc.
-Notation Nplus_succ := plus_succ_l.
-Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)).
-
-(** Properties of subtraction. *)
-
-Notation Nminus_N0_Nle :=
-  (fun n m : N => (conj (proj2 (le_minus_0 n m)) (proj1 (le_minus_0 n m)))).
-Notation Nminus_0_r := minus_0_r.
-Notation Nminus_succ_r := minus_succ_r.
-
-(** Properties of multiplication *)
-
-Notation Nmult_0_l := times_0_l.
-Notation Nmult_1_l := times_1_l.
-Notation Nmult_1_r := times_1_r.
-Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
-Proof.
-intros; now rewrite times_succ_l, Nplus_comm.
-Qed.
-Notation Nmult_comm := times_comm.
-Notation Nmult_assoc := times_assoc.
-Notation Nmult_plus_distr_r := times_plus_distr_r.
-Notation Nmult_reg_r :=
-  (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)).
-
-(** Properties of comparison *)
-
-Notation Ncompare_Eq_eq := (fun n m : N => proj1 (Ncompare_eq_correct n m)).
-Notation Ncompare_refl := Ncompare_diag.
-Notation Nlt_irrefl := lt_irrefl.
-
-Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
-Proof.
-destruct n; destruct m; simpl; auto.
-exact (Pcompare_antisym p p0 Eq).
-Qed.
-
-Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
-Proof.
-destruct n; discriminate.
-Qed.
-
-(** Other properties and operations; given explicitly *)
-
-Definition Ndiscr : forall n : N, {p : positive | n = Npos p} + {n = N0}.
-Proof.
-destruct n; auto.
-left; exists p; auto.
-Defined.
-
-(** Operation x -> 2 * x + 1 *)
-
-Definition Ndouble_plus_one x :=
-match x with
-| N0 => Npos 1
-| Npos p => Npos (xI p)
-end.
-
-(** Operation x -> 2 * x *)
-
-Definition Ndouble n :=
-match n with
-| N0 => N0
-| Npos p => Npos (xO p)
-end.
-
-(** convenient induction principles *)
-
-Theorem N_ind_double :
- forall (a:N) (P:N -> Prop),
-   P N0 ->
-   (forall a, P a -> P (Ndouble a)) ->
-   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
-Proof.
-  intros; elim a. trivial.
-  simple induction p. intros.
-  apply (H1 (Npos p0)); trivial.
-  intros; apply (H0 (Npos p0)); trivial.
-  intros; apply (H1 N0); assumption.
-Qed.
-
-Lemma N_rec_double :
- forall (a:N) (P:N -> Set),
-   P N0 ->
-   (forall a, P a -> P (Ndouble a)) ->
-   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
-Proof.
-  intros; elim a. trivial.
-  simple induction p. intros.
-  apply (H1 (Npos p0)); trivial.
-  intros; apply (H0 (Npos p0)); trivial.
-  intros; apply (H1 N0); assumption.
-Qed.
-
-(** Division by 2 *)
-
-Definition Ndiv2 (n:N) :=
-  match n with
-  | N0 => N0
-  | Npos 1 => N0
-  | Npos (xO p) => Npos p
-  | Npos (xI p) => Npos p
-  end.
-
-Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n.
-Proof.
-  destruct n; trivial.
-Qed.
-
-Lemma Ndouble_plus_one_div2 :
- forall n:N, Ndiv2 (Ndouble_plus_one n) = n.
-Proof.
-  destruct n; trivial.
-Qed.
-
-Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m.
-Proof.
-  intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2.
-Qed.
-
-Lemma Ndouble_plus_one_inj :
- forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m.
-Proof.
-  intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2.
-Qed.
-