From f93f073df630bb46ddd07802026c0326dc72dafd Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:55:59 +0000 Subject: Notation: a new annotation "compat 8.x" extending "only parsing" Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/BinNat.v | 166 ++++++++++++++++++++++---------------------- theories/NArith/Ndigits.v | 26 +++---- theories/NArith/Ndiv_def.v | 12 ++-- theories/NArith/Nnat.v | 54 +++++++------- theories/NArith/Nsqrt_def.v | 10 +-- 5 files changed, 134 insertions(+), 134 deletions(-) (limited to 'theories/NArith') diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 30e35f501..6128b9740 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1013,95 +1013,95 @@ Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope. (** Compatibility notations *) -(*Notation N := N (only parsing).*) (*hidden by module N above *) +(*Notation N := N (compat "8.3").*) (*hidden by module N above *) Notation N_rect := N_rect (only parsing). Notation N_rec := N_rec (only parsing). Notation N_ind := N_ind (only parsing). Notation N0 := N0 (only parsing). Notation Npos := Npos (only parsing). -Notation Ndiscr := N.discr (only parsing). -Notation Ndouble_plus_one := N.succ_double. -Notation Ndouble := N.double (only parsing). -Notation Nsucc := N.succ (only parsing). -Notation Npred := N.pred (only parsing). -Notation Nsucc_pos := N.succ_pos (only parsing). -Notation Ppred_N := Pos.pred_N (only parsing). -Notation Nplus := N.add (only parsing). -Notation Nminus := N.sub (only parsing). -Notation Nmult := N.mul (only parsing). -Notation Neqb := N.eqb (only parsing). -Notation Ncompare := N.compare (only parsing). -Notation Nlt := N.lt (only parsing). -Notation Ngt := N.gt (only parsing). -Notation Nle := N.le (only parsing). -Notation Nge := N.ge (only parsing). -Notation Nmin := N.min (only parsing). -Notation Nmax := N.max (only parsing). -Notation Ndiv2 := N.div2 (only parsing). -Notation Neven := N.even (only parsing). -Notation Nodd := N.odd (only parsing). -Notation Npow := N.pow (only parsing). -Notation Nlog2 := N.log2 (only parsing). - -Notation nat_of_N := N.to_nat (only parsing). -Notation N_of_nat := N.of_nat (only parsing). -Notation N_eq_dec := N.eq_dec (only parsing). -Notation Nrect := N.peano_rect (only parsing). -Notation Nrect_base := N.peano_rect_base (only parsing). -Notation Nrect_step := N.peano_rect_succ (only parsing). -Notation Nind := N.peano_ind (only parsing). -Notation Nrec := N.peano_rec (only parsing). -Notation Nrec_base := N.peano_rec_base (only parsing). -Notation Nrec_succ := N.peano_rec_succ (only parsing). - -Notation Npred_succ := N.pred_succ (only parsing). -Notation Npred_minus := N.pred_sub (only parsing). -Notation Nsucc_pred := N.succ_pred (only parsing). -Notation Ppred_N_spec := N.pos_pred_spec (only parsing). -Notation Nsucc_pos_spec := N.succ_pos_spec (only parsing). -Notation Ppred_Nsucc := N.pos_pred_succ (only parsing). -Notation Nplus_0_l := N.add_0_l (only parsing). -Notation Nplus_0_r := N.add_0_r (only parsing). -Notation Nplus_comm := N.add_comm (only parsing). -Notation Nplus_assoc := N.add_assoc (only parsing). -Notation Nplus_succ := N.add_succ_l (only parsing). -Notation Nsucc_0 := N.succ_0_discr (only parsing). -Notation Nsucc_inj := N.succ_inj (only parsing). -Notation Nminus_N0_Nle := N.sub_0_le (only parsing). -Notation Nminus_0_r := N.sub_0_r (only parsing). -Notation Nminus_succ_r:= N.sub_succ_r (only parsing). -Notation Nmult_0_l := N.mul_0_l (only parsing). -Notation Nmult_1_l := N.mul_1_l (only parsing). -Notation Nmult_1_r := N.mul_1_r (only parsing). -Notation Nmult_comm := N.mul_comm (only parsing). -Notation Nmult_assoc := N.mul_assoc (only parsing). -Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing). -Notation Neqb_eq := N.eqb_eq (only parsing). -Notation Nle_0 := N.le_0_l (only parsing). -Notation Ncompare_refl := N.compare_refl (only parsing). -Notation Ncompare_Eq_eq := N.compare_eq (only parsing). -Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing). -Notation Nlt_irrefl := N.lt_irrefl (only parsing). -Notation Nlt_trans := N.lt_trans (only parsing). -Notation Nle_lteq := N.lt_eq_cases (only parsing). -Notation Nlt_succ_r := N.lt_succ_r (only parsing). -Notation Nle_trans := N.le_trans (only parsing). -Notation Nle_succ_l := N.le_succ_l (only parsing). -Notation Ncompare_spec := N.compare_spec (only parsing). -Notation Ncompare_0 := N.compare_0_r (only parsing). -Notation Ndouble_div2 := N.div2_double (only parsing). -Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing). -Notation Ndouble_inj := N.double_inj (only parsing). -Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing). -Notation Npow_0_r := N.pow_0_r (only parsing). -Notation Npow_succ_r := N.pow_succ_r (only parsing). -Notation Nlog2_spec := N.log2_spec (only parsing). -Notation Nlog2_nonpos := N.log2_nonpos (only parsing). -Notation Neven_spec := N.even_spec (only parsing). -Notation Nodd_spec := N.odd_spec (only parsing). -Notation Nlt_not_eq := N.lt_neq (only parsing). -Notation Ngt_Nlt := N.gt_lt (only parsing). +Notation Ndiscr := N.discr (compat "8.3"). +Notation Ndouble_plus_one := N.succ_double (compat "8.3"). +Notation Ndouble := N.double (compat "8.3"). +Notation Nsucc := N.succ (compat "8.3"). +Notation Npred := N.pred (compat "8.3"). +Notation Nsucc_pos := N.succ_pos (compat "8.3"). +Notation Ppred_N := Pos.pred_N (compat "8.3"). +Notation Nplus := N.add (compat "8.3"). +Notation Nminus := N.sub (compat "8.3"). +Notation Nmult := N.mul (compat "8.3"). +Notation Neqb := N.eqb (compat "8.3"). +Notation Ncompare := N.compare (compat "8.3"). +Notation Nlt := N.lt (compat "8.3"). +Notation Ngt := N.gt (compat "8.3"). +Notation Nle := N.le (compat "8.3"). +Notation Nge := N.ge (compat "8.3"). +Notation Nmin := N.min (compat "8.3"). +Notation Nmax := N.max (compat "8.3"). +Notation Ndiv2 := N.div2 (compat "8.3"). +Notation Neven := N.even (compat "8.3"). +Notation Nodd := N.odd (compat "8.3"). +Notation Npow := N.pow (compat "8.3"). +Notation Nlog2 := N.log2 (compat "8.3"). + +Notation nat_of_N := N.to_nat (compat "8.3"). +Notation N_of_nat := N.of_nat (compat "8.3"). +Notation N_eq_dec := N.eq_dec (compat "8.3"). +Notation Nrect := N.peano_rect (compat "8.3"). +Notation Nrect_base := N.peano_rect_base (compat "8.3"). +Notation Nrect_step := N.peano_rect_succ (compat "8.3"). +Notation Nind := N.peano_ind (compat "8.3"). +Notation Nrec := N.peano_rec (compat "8.3"). +Notation Nrec_base := N.peano_rec_base (compat "8.3"). +Notation Nrec_succ := N.peano_rec_succ (compat "8.3"). + +Notation Npred_succ := N.pred_succ (compat "8.3"). +Notation Npred_minus := N.pred_sub (compat "8.3"). +Notation Nsucc_pred := N.succ_pred (compat "8.3"). +Notation Ppred_N_spec := N.pos_pred_spec (compat "8.3"). +Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.3"). +Notation Ppred_Nsucc := N.pos_pred_succ (compat "8.3"). +Notation Nplus_0_l := N.add_0_l (compat "8.3"). +Notation Nplus_0_r := N.add_0_r (compat "8.3"). +Notation Nplus_comm := N.add_comm (compat "8.3"). +Notation Nplus_assoc := N.add_assoc (compat "8.3"). +Notation Nplus_succ := N.add_succ_l (compat "8.3"). +Notation Nsucc_0 := N.succ_0_discr (compat "8.3"). +Notation Nsucc_inj := N.succ_inj (compat "8.3"). +Notation Nminus_N0_Nle := N.sub_0_le (compat "8.3"). +Notation Nminus_0_r := N.sub_0_r (compat "8.3"). +Notation Nminus_succ_r:= N.sub_succ_r (compat "8.3"). +Notation Nmult_0_l := N.mul_0_l (compat "8.3"). +Notation Nmult_1_l := N.mul_1_l (compat "8.3"). +Notation Nmult_1_r := N.mul_1_r (compat "8.3"). +Notation Nmult_comm := N.mul_comm (compat "8.3"). +Notation Nmult_assoc := N.mul_assoc (compat "8.3"). +Notation Nmult_plus_distr_r := N.mul_add_distr_r (compat "8.3"). +Notation Neqb_eq := N.eqb_eq (compat "8.3"). +Notation Nle_0 := N.le_0_l (compat "8.3"). +Notation Ncompare_refl := N.compare_refl (compat "8.3"). +Notation Ncompare_Eq_eq := N.compare_eq (compat "8.3"). +Notation Ncompare_eq_correct := N.compare_eq_iff (compat "8.3"). +Notation Nlt_irrefl := N.lt_irrefl (compat "8.3"). +Notation Nlt_trans := N.lt_trans (compat "8.3"). +Notation Nle_lteq := N.lt_eq_cases (compat "8.3"). +Notation Nlt_succ_r := N.lt_succ_r (compat "8.3"). +Notation Nle_trans := N.le_trans (compat "8.3"). +Notation Nle_succ_l := N.le_succ_l (compat "8.3"). +Notation Ncompare_spec := N.compare_spec (compat "8.3"). +Notation Ncompare_0 := N.compare_0_r (compat "8.3"). +Notation Ndouble_div2 := N.div2_double (compat "8.3"). +Notation Ndouble_plus_one_div2 := N.div2_succ_double (compat "8.3"). +Notation Ndouble_inj := N.double_inj (compat "8.3"). +Notation Ndouble_plus_one_inj := N.succ_double_inj (compat "8.3"). +Notation Npow_0_r := N.pow_0_r (compat "8.3"). +Notation Npow_succ_r := N.pow_succ_r (compat "8.3"). +Notation Nlog2_spec := N.log2_spec (compat "8.3"). +Notation Nlog2_nonpos := N.log2_nonpos (compat "8.3"). +Notation Neven_spec := N.even_spec (compat "8.3"). +Notation Nodd_spec := N.odd_spec (compat "8.3"). +Notation Nlt_not_eq := N.lt_neq (compat "8.3"). +Notation Ngt_Nlt := N.gt_lt (compat "8.3"). (** More complex compatibility facts, expressed as lemmas (to preserve scopes for instance) *) diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index b0c335957..06f47d719 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -15,17 +15,17 @@ Local Open Scope N_scope. (** Compatibility names for some bitwise operations *) -Notation Pxor := Pos.lxor (only parsing). -Notation Nxor := N.lxor (only parsing). -Notation Pbit := Pos.testbit_nat (only parsing). -Notation Nbit := N.testbit_nat (only parsing). - -Notation Nxor_eq := N.lxor_eq (only parsing). -Notation Nxor_comm := N.lxor_comm (only parsing). -Notation Nxor_assoc := N.lxor_assoc (only parsing). -Notation Nxor_neutral_left := N.lxor_0_l (only parsing). -Notation Nxor_neutral_right := N.lxor_0_r (only parsing). -Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing). +Notation Pxor := Pos.lxor (compat "8.3"). +Notation Nxor := N.lxor (compat "8.3"). +Notation Pbit := Pos.testbit_nat (compat "8.3"). +Notation Nbit := N.testbit_nat (compat "8.3"). + +Notation Nxor_eq := N.lxor_eq (compat "8.3"). +Notation Nxor_comm := N.lxor_comm (compat "8.3"). +Notation Nxor_assoc := N.lxor_assoc (compat "8.3"). +Notation Nxor_neutral_left := N.lxor_0_l (compat "8.3"). +Notation Nxor_neutral_right := N.lxor_0_r (compat "8.3"). +Notation Nxor_nilpotent := N.lxor_nilpotent (compat "8.3"). (** Equivalence of bit-testing functions, either with index in [N] or in [nat]. *) @@ -247,7 +247,7 @@ Local Close Scope N_scope. (** Checking whether a number is odd, i.e. if its lower bit is set. *) -Notation Nbit0 := N.odd (only parsing). +Notation Nbit0 := N.odd (compat "8.3"). Definition Nodd (n:N) := Nbit0 n = true. Definition Neven (n:N) := Nbit0 n = false. @@ -493,7 +493,7 @@ Qed. (** Number of digits in a number *) -Notation Nsize := N.size_nat (only parsing). +Notation Nsize := N.size_nat (compat "8.3"). (** conversions between N and bit vectors. *) diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 559f01f16..21f15f976 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -22,10 +22,10 @@ Lemma Pdiv_eucl_remainder a b : snd (Pdiv_eucl a b) < Npos b. Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed. -Notation Ndiv_eucl := N.div_eucl (only parsing). -Notation Ndiv := N.div (only parsing). -Notation Nmod := N.modulo (only parsing). +Notation Ndiv_eucl := N.div_eucl (compat "8.3"). +Notation Ndiv := N.div (compat "8.3"). +Notation Nmod := N.modulo (compat "8.3"). -Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing). -Notation Ndiv_mod_eq := N.div_mod' (only parsing). -Notation Nmod_lt := N.mod_lt (only parsing). +Notation Ndiv_eucl_correct := N.div_eucl_spec (compat "8.3"). +Notation Ndiv_mod_eq := N.div_mod' (compat "8.3"). +Notation Nmod_lt := N.mod_lt (compat "8.3"). diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 133d4c23b..eb8d5961b 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -203,30 +203,30 @@ Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) -Notation nat_of_N_inj := N2Nat.inj (only parsing). -Notation N_of_nat_of_N := N2Nat.id (only parsing). -Notation nat_of_Ndouble := N2Nat.inj_double (only parsing). -Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing). -Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing). -Notation nat_of_Nplus := N2Nat.inj_add (only parsing). -Notation nat_of_Nmult := N2Nat.inj_mul (only parsing). -Notation nat_of_Nminus := N2Nat.inj_sub (only parsing). -Notation nat_of_Npred := N2Nat.inj_pred (only parsing). -Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing). -Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing). -Notation nat_of_Nmax := N2Nat.inj_max (only parsing). -Notation nat_of_Nmin := N2Nat.inj_min (only parsing). - -Notation nat_of_N_of_nat := Nat2N.id (only parsing). -Notation N_of_nat_inj := Nat2N.inj (only parsing). -Notation N_of_double := Nat2N.inj_double (only parsing). -Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing). -Notation N_of_S := Nat2N.inj_succ (only parsing). -Notation N_of_pred := Nat2N.inj_pred (only parsing). -Notation N_of_plus := Nat2N.inj_add (only parsing). -Notation N_of_minus := Nat2N.inj_sub (only parsing). -Notation N_of_mult := Nat2N.inj_mul (only parsing). -Notation N_of_div2 := Nat2N.inj_div2 (only parsing). -Notation N_of_nat_compare := Nat2N.inj_compare (only parsing). -Notation N_of_min := Nat2N.inj_min (only parsing). -Notation N_of_max := Nat2N.inj_max (only parsing). +Notation nat_of_N_inj := N2Nat.inj (compat "8.3"). +Notation N_of_nat_of_N := N2Nat.id (compat "8.3"). +Notation nat_of_Ndouble := N2Nat.inj_double (compat "8.3"). +Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (compat "8.3"). +Notation nat_of_Nsucc := N2Nat.inj_succ (compat "8.3"). +Notation nat_of_Nplus := N2Nat.inj_add (compat "8.3"). +Notation nat_of_Nmult := N2Nat.inj_mul (compat "8.3"). +Notation nat_of_Nminus := N2Nat.inj_sub (compat "8.3"). +Notation nat_of_Npred := N2Nat.inj_pred (compat "8.3"). +Notation nat_of_Ndiv2 := N2Nat.inj_div2 (compat "8.3"). +Notation nat_of_Ncompare := N2Nat.inj_compare (compat "8.3"). +Notation nat_of_Nmax := N2Nat.inj_max (compat "8.3"). +Notation nat_of_Nmin := N2Nat.inj_min (compat "8.3"). + +Notation nat_of_N_of_nat := Nat2N.id (compat "8.3"). +Notation N_of_nat_inj := Nat2N.inj (compat "8.3"). +Notation N_of_double := Nat2N.inj_double (compat "8.3"). +Notation N_of_double_plus_one := Nat2N.inj_succ_double (compat "8.3"). +Notation N_of_S := Nat2N.inj_succ (compat "8.3"). +Notation N_of_pred := Nat2N.inj_pred (compat "8.3"). +Notation N_of_plus := Nat2N.inj_add (compat "8.3"). +Notation N_of_minus := Nat2N.inj_sub (compat "8.3"). +Notation N_of_mult := Nat2N.inj_mul (compat "8.3"). +Notation N_of_div2 := Nat2N.inj_div2 (compat "8.3"). +Notation N_of_nat_compare := Nat2N.inj_compare (compat "8.3"). +Notation N_of_min := Nat2N.inj_min (compat "8.3"). +Notation N_of_max := Nat2N.inj_max (compat "8.3"). diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index edb6b2895..1375f2803 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -11,8 +11,8 @@ Require Import BinNat. (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) -Notation Nsqrtrem := N.sqrtrem (only parsing). -Notation Nsqrt := N.sqrt (only parsing). -Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing). -Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing). -Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing). +Notation Nsqrtrem := N.sqrtrem (compat "8.3"). +Notation Nsqrt := N.sqrt (compat "8.3"). +Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.3"). +Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (compat "8.3"). +Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.3"). -- cgit v1.2.3