diff options
40 files changed, 791 insertions, 694 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 7415931f0..0e1a54e4e 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -19,7 +19,9 @@ open Nametab (* Syntactic definitions. *) -let syntax_table = ref (KNmap.empty : interpretation KNmap.t) +type version = Flags.compat_version option + +let syntax_table = ref (KNmap.empty : (interpretation*version) KNmap.t) let _ = Summary.declare_summary "SYNTAXCONSTANT" @@ -27,14 +29,14 @@ let _ = Summary.declare_summary Summary.unfreeze_function = (fun ft -> syntax_table := ft); Summary.init_function = (fun () -> syntax_table := KNmap.empty) } -let add_syntax_constant kn c = - syntax_table := KNmap.add kn c !syntax_table +let add_syntax_constant kn c onlyparse = + syntax_table := KNmap.add kn (c,onlyparse) !syntax_table -let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = +let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); - add_syntax_constant kn pat; + add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function @@ -47,7 +49,7 @@ let is_alias_of_already_visible_name sp = function let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if not (is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; - if not onlyparse then + if onlyparse = None then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared inbetween *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat @@ -63,7 +65,8 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) = let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o -let in_syntax_constant : bool * interpretation * bool -> obj = +let in_syntax_constant + : bool * interpretation * Flags.compat_version option -> obj = declare_object {(default_object "SYNTAXCONSTANT") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; @@ -81,5 +84,50 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () +let pr_global r = pr_global_env Idset.empty r +let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Idset.empty kn) + +let allow_compat_notations = ref true +let verbose_compat_notations = ref false + +let is_verbose_compat () = + !verbose_compat_notations || not !allow_compat_notations + +let verbose_compat kn def = function + | Some v when is_verbose_compat () && Flags.version_strictly_greater v -> + let act = + if !verbose_compat_notations then msg_warning else errorlabstrm "" + in + let pp_def = match def with + | [], NRef r -> str " is " ++ pr_global_env Idset.empty r + | _ -> str " is a compatibility notation" + in + let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in + act (pr_syndef kn ++ pp_def ++ since) + | _ -> () + let search_syntactic_definition kn = - out_pat (KNmap.find kn !syntax_table) + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + verbose_compat kn def v; + def + +open Goptions + +let set_verbose_compat_notations = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "verbose compatibility notations"; + optkey = ["Verbose";"Compat";"Notations"]; + optread = (fun () -> !verbose_compat_notations); + optwrite = ((:=) verbose_compat_notations) } + +let set_compat_notations = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "accept compatibility notations"; + optkey = ["Compat"; "Notations"]; + optread = (fun () -> !allow_compat_notations); + optwrite = ((:=) allow_compat_notations) } diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index d977a728d..25bceb3d2 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -16,7 +16,13 @@ open Libnames type syndef_interpretation = (identifier * subscopes) list * notation_constr -val declare_syntactic_definition : bool -> identifier -> bool -> - syndef_interpretation -> unit +val declare_syntactic_definition : bool -> identifier -> + Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : kernel_name -> syndef_interpretation + +(** Options concerning verbose display of compatibility notations + or their deactivation *) + +val set_verbose_compat_notations : bool -> unit +val set_compat_notations : bool -> unit diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 568d8a38e..37f25e0ac 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -122,9 +122,12 @@ type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) type inductive_flag = Decl_kinds.recursivity_kind -type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) +type onlyparsing_flag = Flags.compat_version option + (* Some v = Parse only; None = Print also. + If v<>Current, it contains the name of the coq version + which this notation is trying to be compatible with *) type option_value = Interface.option_value = | BoolValue of bool @@ -183,7 +186,7 @@ type syntax_modifier = | SetLevel of int | SetAssoc of Compat.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing + | SetOnlyParsing of Flags.compat_version | SetFormat of string located type proof_end = diff --git a/lib/flags.ml b/lib/flags.ml index b4f6272ac..8cce04c50 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -38,12 +38,19 @@ let record_print = ref true (* Compatibility mode *) -type compat_version = V8_2 | V8_3 -let compat_version = ref None -let version_strictly_greater v = - match !compat_version with None -> true | Some v' -> v'>v +(* Current means no particular compatibility consideration. + For correct comparisons, this constructor should remain the last one. *) + +type compat_version = V8_2 | V8_3 | Current +let compat_version = ref Current +let version_strictly_greater v = !compat_version > v let version_less_or_equal v = not (version_strictly_greater v) +let pr_version = function + | V8_2 -> "8.2" + | V8_3 -> "8.3" + | Current -> "current" + (* Translate *) let beautify = ref false let make_beautify f = beautify := f diff --git a/lib/flags.mli b/lib/flags.mli index 77399b9e5..0aceee045 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -26,10 +26,11 @@ val load_proofs : load_proofs ref val raw_print : bool ref val record_print : bool ref -type compat_version = V8_2 | V8_3 -val compat_version : compat_version option ref +type compat_version = V8_2 | V8_3 | Current +val compat_version : compat_version ref val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool +val pr_version : compat_version -> string val beautify : bool ref val make_beautify : bool -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index fbf1c64f2..509d266be 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -985,8 +985,7 @@ GEXTEND Gram sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (enforce_module_locality local,(op,modl),p,sc) | IDENT "Notation"; local = obsolete_locality; id = identref; - idl = LIST0 ident; ":="; c = constr; - b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> + idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition (id,(idl,c),enforce_module_locality local,b) | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":="; @@ -1014,6 +1013,13 @@ GEXTEND Gram to factorize with other "Print"-based vernac entries *) ] ] ; + only_parsing: + [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> + Some Flags.Current + | "("; IDENT "compat"; s = STRING; ")" -> + Some (Coqinit.get_compat_version s) + | -> None ] ] + ; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; @@ -1029,7 +1035,10 @@ GEXTEND Gram | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA - | IDENT "only"; IDENT "parsing" -> SetOnlyParsing + | IDENT "only"; IDENT "parsing" -> + SetOnlyParsing Flags.Current + | IDENT "compat"; s = STRING -> + SetOnlyParsing (Coqinit.get_compat_version s) | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9513001f4..d7b36d287 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -381,7 +381,8 @@ let pr_syntax_modifier = function | SetAssoc RightA -> str"right associativity" | SetAssoc NonA -> str"no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ - | SetOnlyParsing -> str"only parsing" + | SetOnlyParsing Flags.Current -> str"only parsing" + | SetOnlyParsing v -> str("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat s -> str"format " ++ pr_located qs s let pr_syntax_modifiers = function @@ -779,7 +780,8 @@ let rec pr_vernac = function hov 2 (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++ prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) + pr_syntax_modifiers + (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) | VernacDeclareImplicits (local,q,[]) -> hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ pr_smart_global q) diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index c9e6d3cf3..d0075d741 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -10,8 +10,6 @@ Open Local Scope nat_scope. -Notation not_eq_sym := sym_not_eq. - Implicit Types m n p q : nat. Require Import Arith_base. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d391611dc..1dc998cdf 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -399,14 +399,14 @@ Qed. (* Aliases *) -Notation sym_eq := eq_sym (only parsing). -Notation trans_eq := eq_trans (only parsing). -Notation sym_not_eq := not_eq_sym (only parsing). - -Notation refl_equal := eq_refl (only parsing). -Notation sym_equal := eq_sym (only parsing). -Notation trans_equal := eq_trans (only parsing). -Notation sym_not_equal := not_eq_sym (only parsing). +Notation sym_eq := eq_sym (compat "8.3"). +Notation trans_eq := eq_trans (compat "8.3"). +Notation sym_not_eq := not_eq_sym (compat "8.3"). + +Notation refl_equal := eq_refl (compat "8.3"). +Notation sym_equal := eq_sym (compat "8.3"). +Notation trans_equal := eq_trans (compat "8.3"). +Notation sym_not_equal := not_eq_sym (compat "8.3"). Hint Immediate eq_sym not_eq_sym: core. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 4d64b8238..9b2a026c2 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -75,7 +75,7 @@ Ltac false_hyp H G := (* A case with no loss of information. *) -Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x. +Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) 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"). diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 2e4d52a29..e22cac7be 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,183 +1871,183 @@ Notation xI := xI (only parsing). Notation xO := xO (only parsing). Notation xH := xH (only parsing). -Notation Psucc := Pos.succ (only parsing). -Notation Pplus := Pos.add (only parsing). -Notation Pplus_carry := Pos.add_carry (only parsing). -Notation Ppred := Pos.pred (only parsing). -Notation Piter_op := Pos.iter_op (only parsing). -Notation Piter_op_succ := Pos.iter_op_succ (only parsing). -Notation Pmult_nat := (Pos.iter_op plus) (only parsing). -Notation nat_of_P := Pos.to_nat (only parsing). -Notation P_of_succ_nat := Pos.of_succ_nat (only parsing). -Notation Pdouble_minus_one := Pos.pred_double (only parsing). -Notation positive_mask := Pos.mask (only parsing). -Notation IsNul := Pos.IsNul (only parsing). -Notation IsPos := Pos.IsPos (only parsing). -Notation IsNeg := Pos.IsNeg (only parsing). -Notation positive_mask_rect := Pos.mask_rect (only parsing). -Notation positive_mask_ind := Pos.mask_ind (only parsing). -Notation positive_mask_rec := Pos.mask_rec (only parsing). -Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing). -Notation Pdouble_mask := Pos.double_mask (only parsing). -Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing). -Notation Pminus_mask := Pos.sub_mask (only parsing). -Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing). -Notation Pminus := Pos.sub (only parsing). -Notation Pmult := Pos.mul (only parsing). -Notation iter_pos := @Pos.iter (only parsing). -Notation Ppow := Pos.pow (only parsing). -Notation Pdiv2 := Pos.div2 (only parsing). -Notation Pdiv2_up := Pos.div2_up (only parsing). -Notation Psize := Pos.size_nat (only parsing). -Notation Psize_pos := Pos.size (only parsing). -Notation Pcompare := Pos.compare_cont (only parsing). -Notation Plt := Pos.lt (only parsing). -Notation Pgt := Pos.gt (only parsing). -Notation Ple := Pos.le (only parsing). -Notation Pge := Pos.ge (only parsing). -Notation Pmin := Pos.min (only parsing). -Notation Pmax := Pos.max (only parsing). -Notation Peqb := Pos.eqb (only parsing). -Notation positive_eq_dec := Pos.eq_dec (only parsing). -Notation xI_succ_xO := Pos.xI_succ_xO (only parsing). -Notation Psucc_discr := Pos.succ_discr (only parsing). +Notation Psucc := Pos.succ (compat "8.3"). +Notation Pplus := Pos.add (compat "8.3"). +Notation Pplus_carry := Pos.add_carry (compat "8.3"). +Notation Ppred := Pos.pred (compat "8.3"). +Notation Piter_op := Pos.iter_op (compat "8.3"). +Notation Piter_op_succ := Pos.iter_op_succ (compat "8.3"). +Notation Pmult_nat := (Pos.iter_op plus) (compat "8.3"). +Notation nat_of_P := Pos.to_nat (compat "8.3"). +Notation P_of_succ_nat := Pos.of_succ_nat (compat "8.3"). +Notation Pdouble_minus_one := Pos.pred_double (compat "8.3"). +Notation positive_mask := Pos.mask (compat "8.3"). +Notation IsNul := Pos.IsNul (compat "8.3"). +Notation IsPos := Pos.IsPos (compat "8.3"). +Notation IsNeg := Pos.IsNeg (compat "8.3"). +Notation positive_mask_rect := Pos.mask_rect (compat "8.3"). +Notation positive_mask_ind := Pos.mask_ind (compat "8.3"). +Notation positive_mask_rec := Pos.mask_rec (compat "8.3"). +Notation Pdouble_plus_one_mask := Pos.succ_double_mask (compat "8.3"). +Notation Pdouble_mask := Pos.double_mask (compat "8.3"). +Notation Pdouble_minus_two := Pos.double_pred_mask (compat "8.3"). +Notation Pminus_mask := Pos.sub_mask (compat "8.3"). +Notation Pminus_mask_carry := Pos.sub_mask_carry (compat "8.3"). +Notation Pminus := Pos.sub (compat "8.3"). +Notation Pmult := Pos.mul (compat "8.3"). +Notation iter_pos := @Pos.iter (compat "8.3"). +Notation Ppow := Pos.pow (compat "8.3"). +Notation Pdiv2 := Pos.div2 (compat "8.3"). +Notation Pdiv2_up := Pos.div2_up (compat "8.3"). +Notation Psize := Pos.size_nat (compat "8.3"). +Notation Psize_pos := Pos.size (compat "8.3"). +Notation Pcompare := Pos.compare_cont (compat "8.3"). +Notation Plt := Pos.lt (compat "8.3"). +Notation Pgt := Pos.gt (compat "8.3"). +Notation Ple := Pos.le (compat "8.3"). +Notation Pge := Pos.ge (compat "8.3"). +Notation Pmin := Pos.min (compat "8.3"). +Notation Pmax := Pos.max (compat "8.3"). +Notation Peqb := Pos.eqb (compat "8.3"). +Notation positive_eq_dec := Pos.eq_dec (compat "8.3"). +Notation xI_succ_xO := Pos.xI_succ_xO (compat "8.3"). +Notation Psucc_discr := Pos.succ_discr (compat "8.3"). Notation Psucc_o_double_minus_one_eq_xO := - Pos.succ_pred_double (only parsing). + Pos.succ_pred_double (compat "8.3"). Notation Pdouble_minus_one_o_succ_eq_xI := - Pos.pred_double_succ (only parsing). -Notation xO_succ_permute := Pos.double_succ (only parsing). + Pos.pred_double_succ (compat "8.3"). +Notation xO_succ_permute := Pos.double_succ (compat "8.3"). Notation double_moins_un_xO_discr := - Pos.pred_double_xO_discr (only parsing). -Notation Psucc_not_one := Pos.succ_not_1 (only parsing). -Notation Ppred_succ := Pos.pred_succ (only parsing). -Notation Psucc_pred := Pos.succ_pred_or (only parsing). -Notation Psucc_inj := Pos.succ_inj (only parsing). -Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing). -Notation Pplus_comm := Pos.add_comm (only parsing). -Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing). -Notation Pplus_succ_permute_l := Pos.add_succ_l (only parsing). -Notation Pplus_no_neutral := Pos.add_no_neutral (only parsing). -Notation Pplus_carry_plus := Pos.add_carry_add (only parsing). -Notation Pplus_reg_r := Pos.add_reg_r (only parsing). -Notation Pplus_reg_l := Pos.add_reg_l (only parsing). -Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (only parsing). -Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (only parsing). -Notation Pplus_assoc := Pos.add_assoc (only parsing). -Notation Pplus_xO := Pos.add_xO (only parsing). -Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (only parsing). -Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (only parsing). -Notation Pplus_diag := Pos.add_diag (only parsing). -Notation PeanoView := Pos.PeanoView (only parsing). -Notation PeanoOne := Pos.PeanoOne (only parsing). -Notation PeanoSucc := Pos.PeanoSucc (only parsing). -Notation PeanoView_rect := Pos.PeanoView_rect (only parsing). -Notation PeanoView_ind := Pos.PeanoView_ind (only parsing). -Notation PeanoView_rec := Pos.PeanoView_rec (only parsing). -Notation peanoView_xO := Pos.peanoView_xO (only parsing). -Notation peanoView_xI := Pos.peanoView_xI (only parsing). -Notation peanoView := Pos.peanoView (only parsing). -Notation PeanoView_iter := Pos.PeanoView_iter (only parsing). -Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (only parsing). -Notation PeanoViewUnique := Pos.PeanoViewUnique (only parsing). -Notation Prect := Pos.peano_rect (only parsing). -Notation Prect_succ := Pos.peano_rect_succ (only parsing). -Notation Prect_base := Pos.peano_rect_base (only parsing). -Notation Prec := Pos.peano_rec (only parsing). -Notation Pind := Pos.peano_ind (only parsing). -Notation Pcase := Pos.peano_case (only parsing). -Notation Pmult_1_r := Pos.mul_1_r (only parsing). -Notation Pmult_Sn_m := Pos.mul_succ_l (only parsing). -Notation Pmult_xO_permute_r := Pos.mul_xO_r (only parsing). -Notation Pmult_xI_permute_r := Pos.mul_xI_r (only parsing). -Notation Pmult_comm := Pos.mul_comm (only parsing). -Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (only parsing). -Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (only parsing). -Notation Pmult_assoc := Pos.mul_assoc (only parsing). -Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (only parsing). -Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing). -Notation Pmult_reg_r := Pos.mul_reg_r (only parsing). -Notation Pmult_reg_l := Pos.mul_reg_l (only parsing). -Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing). -Notation Psquare_xO := Pos.square_xO (only parsing). -Notation Psquare_xI := Pos.square_xI (only parsing). -Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing). -Notation iter_pos_swap := Pos.iter_swap (only parsing). -Notation iter_pos_succ := Pos.iter_succ (only parsing). -Notation iter_pos_plus := Pos.iter_add (only parsing). -Notation iter_pos_invariant := Pos.iter_invariant (only parsing). -Notation Ppow_1_r := Pos.pow_1_r (only parsing). -Notation Ppow_succ_r := Pos.pow_succ_r (only parsing). -Notation Peqb_refl := Pos.eqb_refl (only parsing). -Notation Peqb_eq := Pos.eqb_eq (only parsing). -Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing). -Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing). -Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing). -Notation Pcompare_eq_Lt := Pos.compare_lt_iff (only parsing). -Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing). - -Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing). -Notation ZC1 := Pos.gt_lt (only parsing). -Notation ZC2 := Pos.lt_gt (only parsing). -Notation Pcompare_spec := Pos.compare_spec (only parsing). -Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing). -Notation Pcompare_succ_succ := Pos.compare_succ_succ (only parsing). -Notation Pcompare_1 := Pos.nlt_1_r (only parsing). -Notation Plt_1 := Pos.nlt_1_r (only parsing). -Notation Plt_1_succ := Pos.lt_1_succ (only parsing). -Notation Plt_lt_succ := Pos.lt_lt_succ (only parsing). -Notation Plt_irrefl := Pos.lt_irrefl (only parsing). -Notation Plt_trans := Pos.lt_trans (only parsing). -Notation Plt_ind := Pos.lt_ind (only parsing). -Notation Ple_lteq := Pos.le_lteq (only parsing). -Notation Ple_refl := Pos.le_refl (only parsing). -Notation Ple_lt_trans := Pos.le_lt_trans (only parsing). -Notation Plt_le_trans := Pos.lt_le_trans (only parsing). -Notation Ple_trans := Pos.le_trans (only parsing). -Notation Plt_succ_r := Pos.lt_succ_r (only parsing). -Notation Ple_succ_l := Pos.le_succ_l (only parsing). -Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing). -Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing). -Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing). -Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (only parsing). -Notation Pplus_lt_mono := Pos.add_lt_mono (only parsing). -Notation Pplus_le_mono_l := Pos.add_le_mono_l (only parsing). -Notation Pplus_le_mono_r := Pos.add_le_mono_r (only parsing). -Notation Pplus_le_mono := Pos.add_le_mono (only parsing). -Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (only parsing). -Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (only parsing). -Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (only parsing). -Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (only parsing). -Notation Pmult_lt_mono := Pos.mul_lt_mono (only parsing). -Notation Pmult_le_mono_l := Pos.mul_le_mono_l (only parsing). -Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing). -Notation Pmult_le_mono := Pos.mul_le_mono (only parsing). -Notation Plt_plus_r := Pos.lt_add_r (only parsing). -Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing). -Notation Ppow_gt_1 := Pos.pow_gt_1 (only parsing). -Notation Ppred_mask := Pos.pred_mask (only parsing). -Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing). -Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing). -Notation Pminus_succ_r := Pos.sub_succ_r (only parsing). -Notation Pminus_mask_diag := Pos.sub_mask_diag (only parsing). - -Notation Pplus_minus_eq := Pos.add_sub (only parsing). -Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (only parsing). -Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (only parsing). -Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (only parsing). -Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (only parsing). -Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (only parsing). -Notation Pminus_decr := Pos.sub_decr (only parsing). -Notation Pminus_xI_xI := Pos.sub_xI_xI (only parsing). -Notation Pplus_minus_assoc := Pos.add_sub_assoc (only parsing). -Notation Pminus_plus_distr := Pos.sub_add_distr (only parsing). -Notation Pminus_minus_distr := Pos.sub_sub_distr (only parsing). -Notation Pminus_mask_Lt := Pos.sub_mask_neg (only parsing). -Notation Pminus_Lt := Pos.sub_lt (only parsing). -Notation Pminus_Eq := Pos.sub_diag (only parsing). -Notation Psize_monotone := Pos.size_nat_monotone (only parsing). -Notation Psize_pos_gt := Pos.size_gt (only parsing). -Notation Psize_pos_le := Pos.size_le (only parsing). + Pos.pred_double_xO_discr (compat "8.3"). +Notation Psucc_not_one := Pos.succ_not_1 (compat "8.3"). +Notation Ppred_succ := Pos.pred_succ (compat "8.3"). +Notation Psucc_pred := Pos.succ_pred_or (compat "8.3"). +Notation Psucc_inj := Pos.succ_inj (compat "8.3"). +Notation Pplus_carry_spec := Pos.add_carry_spec (compat "8.3"). +Notation Pplus_comm := Pos.add_comm (compat "8.3"). +Notation Pplus_succ_permute_r := Pos.add_succ_r (compat "8.3"). +Notation Pplus_succ_permute_l := Pos.add_succ_l (compat "8.3"). +Notation Pplus_no_neutral := Pos.add_no_neutral (compat "8.3"). +Notation Pplus_carry_plus := Pos.add_carry_add (compat "8.3"). +Notation Pplus_reg_r := Pos.add_reg_r (compat "8.3"). +Notation Pplus_reg_l := Pos.add_reg_l (compat "8.3"). +Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (compat "8.3"). +Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (compat "8.3"). +Notation Pplus_assoc := Pos.add_assoc (compat "8.3"). +Notation Pplus_xO := Pos.add_xO (compat "8.3"). +Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (compat "8.3"). +Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (compat "8.3"). +Notation Pplus_diag := Pos.add_diag (compat "8.3"). +Notation PeanoView := Pos.PeanoView (compat "8.3"). +Notation PeanoOne := Pos.PeanoOne (compat "8.3"). +Notation PeanoSucc := Pos.PeanoSucc (compat "8.3"). +Notation PeanoView_rect := Pos.PeanoView_rect (compat "8.3"). +Notation PeanoView_ind := Pos.PeanoView_ind (compat "8.3"). +Notation PeanoView_rec := Pos.PeanoView_rec (compat "8.3"). +Notation peanoView_xO := Pos.peanoView_xO (compat "8.3"). +Notation peanoView_xI := Pos.peanoView_xI (compat "8.3"). +Notation peanoView := Pos.peanoView (compat "8.3"). +Notation PeanoView_iter := Pos.PeanoView_iter (compat "8.3"). +Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (compat "8.3"). +Notation PeanoViewUnique := Pos.PeanoViewUnique (compat "8.3"). +Notation Prect := Pos.peano_rect (compat "8.3"). +Notation Prect_succ := Pos.peano_rect_succ (compat "8.3"). +Notation Prect_base := Pos.peano_rect_base (compat "8.3"). +Notation Prec := Pos.peano_rec (compat "8.3"). +Notation Pind := Pos.peano_ind (compat "8.3"). +Notation Pcase := Pos.peano_case (compat "8.3"). +Notation Pmult_1_r := Pos.mul_1_r (compat "8.3"). +Notation Pmult_Sn_m := Pos.mul_succ_l (compat "8.3"). +Notation Pmult_xO_permute_r := Pos.mul_xO_r (compat "8.3"). +Notation Pmult_xI_permute_r := Pos.mul_xI_r (compat "8.3"). +Notation Pmult_comm := Pos.mul_comm (compat "8.3"). +Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (compat "8.3"). +Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (compat "8.3"). +Notation Pmult_assoc := Pos.mul_assoc (compat "8.3"). +Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (compat "8.3"). +Notation Pmult_xO_discr := Pos.mul_xO_discr (compat "8.3"). +Notation Pmult_reg_r := Pos.mul_reg_r (compat "8.3"). +Notation Pmult_reg_l := Pos.mul_reg_l (compat "8.3"). +Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (compat "8.3"). +Notation Psquare_xO := Pos.square_xO (compat "8.3"). +Notation Psquare_xI := Pos.square_xI (compat "8.3"). +Notation iter_pos_swap_gen := Pos.iter_swap_gen (compat "8.3"). +Notation iter_pos_swap := Pos.iter_swap (compat "8.3"). +Notation iter_pos_succ := Pos.iter_succ (compat "8.3"). +Notation iter_pos_plus := Pos.iter_add (compat "8.3"). +Notation iter_pos_invariant := Pos.iter_invariant (compat "8.3"). +Notation Ppow_1_r := Pos.pow_1_r (compat "8.3"). +Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.3"). +Notation Peqb_refl := Pos.eqb_refl (compat "8.3"). +Notation Peqb_eq := Pos.eqb_eq (compat "8.3"). +Notation Pcompare_refl_id := Pos.compare_cont_refl (compat "8.3"). +Notation Pcompare_eq_iff := Pos.compare_eq_iff (compat "8.3"). +Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (compat "8.3"). +Notation Pcompare_eq_Lt := Pos.compare_lt_iff (compat "8.3"). +Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (compat "8.3"). + +Notation Pcompare_antisym := Pos.compare_cont_antisym (compat "8.3"). +Notation ZC1 := Pos.gt_lt (compat "8.3"). +Notation ZC2 := Pos.lt_gt (compat "8.3"). +Notation Pcompare_spec := Pos.compare_spec (compat "8.3"). +Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (compat "8.3"). +Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.3"). +Notation Pcompare_1 := Pos.nlt_1_r (compat "8.3"). +Notation Plt_1 := Pos.nlt_1_r (compat "8.3"). +Notation Plt_1_succ := Pos.lt_1_succ (compat "8.3"). +Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.3"). +Notation Plt_irrefl := Pos.lt_irrefl (compat "8.3"). +Notation Plt_trans := Pos.lt_trans (compat "8.3"). +Notation Plt_ind := Pos.lt_ind (compat "8.3"). +Notation Ple_lteq := Pos.le_lteq (compat "8.3"). +Notation Ple_refl := Pos.le_refl (compat "8.3"). +Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.3"). +Notation Plt_le_trans := Pos.lt_le_trans (compat "8.3"). +Notation Ple_trans := Pos.le_trans (compat "8.3"). +Notation Plt_succ_r := Pos.lt_succ_r (compat "8.3"). +Notation Ple_succ_l := Pos.le_succ_l (compat "8.3"). +Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (compat "8.3"). +Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (compat "8.3"). +Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (compat "8.3"). +Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (compat "8.3"). +Notation Pplus_lt_mono := Pos.add_lt_mono (compat "8.3"). +Notation Pplus_le_mono_l := Pos.add_le_mono_l (compat "8.3"). +Notation Pplus_le_mono_r := Pos.add_le_mono_r (compat "8.3"). +Notation Pplus_le_mono := Pos.add_le_mono (compat "8.3"). +Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (compat "8.3"). +Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (compat "8.3"). +Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (compat "8.3"). +Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (compat "8.3"). +Notation Pmult_lt_mono := Pos.mul_lt_mono (compat "8.3"). +Notation Pmult_le_mono_l := Pos.mul_le_mono_l (compat "8.3"). +Notation Pmult_le_mono_r := Pos.mul_le_mono_r (compat "8.3"). +Notation Pmult_le_mono := Pos.mul_le_mono (compat "8.3"). +Notation Plt_plus_r := Pos.lt_add_r (compat "8.3"). +Notation Plt_not_plus_l := Pos.lt_not_add_l (compat "8.3"). +Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.3"). +Notation Ppred_mask := Pos.pred_mask (compat "8.3"). +Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (compat "8.3"). +Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (compat "8.3"). +Notation Pminus_succ_r := Pos.sub_succ_r (compat "8.3"). +Notation Pminus_mask_diag := Pos.sub_mask_diag (compat "8.3"). + +Notation Pplus_minus_eq := Pos.add_sub (compat "8.3"). +Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (compat "8.3"). +Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (compat "8.3"). +Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (compat "8.3"). +Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (compat "8.3"). +Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (compat "8.3"). +Notation Pminus_decr := Pos.sub_decr (compat "8.3"). +Notation Pminus_xI_xI := Pos.sub_xI_xI (compat "8.3"). +Notation Pplus_minus_assoc := Pos.add_sub_assoc (compat "8.3"). +Notation Pminus_plus_distr := Pos.sub_add_distr (compat "8.3"). +Notation Pminus_minus_distr := Pos.sub_sub_distr (compat "8.3"). +Notation Pminus_mask_Lt := Pos.sub_mask_neg (compat "8.3"). +Notation Pminus_Lt := Pos.sub_lt (compat "8.3"). +Notation Pminus_Eq := Pos.sub_diag (compat "8.3"). +Notation Psize_monotone := Pos.size_nat_monotone (compat "8.3"). +Notation Psize_pos_gt := Pos.size_gt (compat "8.3"). +Notation Psize_pos_le := Pos.size_le (compat "8.3"). (** More complex compatibility facts, expressed as lemmas (to preserve scopes for instance) *) diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index f9df70bd3..0fa6972b7 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -378,36 +378,36 @@ End SuccNat2Pos. (** For compatibility, old names and old-style lemmas *) -Notation Psucc_S := Pos2Nat.inj_succ (only parsing). -Notation Pplus_plus := Pos2Nat.inj_add (only parsing). -Notation Pmult_mult := Pos2Nat.inj_mul (only parsing). -Notation Pcompare_nat_compare := Pos2Nat.inj_compare (only parsing). -Notation nat_of_P_xH := Pos2Nat.inj_1 (only parsing). -Notation nat_of_P_xO := Pos2Nat.inj_xO (only parsing). -Notation nat_of_P_xI := Pos2Nat.inj_xI (only parsing). -Notation nat_of_P_is_S := Pos2Nat.is_succ (only parsing). -Notation nat_of_P_pos := Pos2Nat.is_pos (only parsing). -Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (only parsing). -Notation nat_of_P_inj := Pos2Nat.inj (only parsing). -Notation Plt_lt := Pos2Nat.inj_lt (only parsing). -Notation Pgt_gt := Pos2Nat.inj_gt (only parsing). -Notation Ple_le := Pos2Nat.inj_le (only parsing). -Notation Pge_ge := Pos2Nat.inj_ge (only parsing). -Notation Pminus_minus := Pos2Nat.inj_sub (only parsing). -Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing). - -Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (only parsing). -Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (only parsing). - -Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (only parsing). -Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (only parsing). -Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (only parsing). -Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (only parsing). -Notation lt_O_nat_of_P := Pos2Nat.is_pos (only parsing). -Notation ZL4 := Pos2Nat.is_succ (only parsing). -Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (only parsing). -Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (only parsing). -Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (only parsing). +Notation Psucc_S := Pos2Nat.inj_succ (compat "8.3"). +Notation Pplus_plus := Pos2Nat.inj_add (compat "8.3"). +Notation Pmult_mult := Pos2Nat.inj_mul (compat "8.3"). +Notation Pcompare_nat_compare := Pos2Nat.inj_compare (compat "8.3"). +Notation nat_of_P_xH := Pos2Nat.inj_1 (compat "8.3"). +Notation nat_of_P_xO := Pos2Nat.inj_xO (compat "8.3"). +Notation nat_of_P_xI := Pos2Nat.inj_xI (compat "8.3"). +Notation nat_of_P_is_S := Pos2Nat.is_succ (compat "8.3"). +Notation nat_of_P_pos := Pos2Nat.is_pos (compat "8.3"). +Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (compat "8.3"). +Notation nat_of_P_inj := Pos2Nat.inj (compat "8.3"). +Notation Plt_lt := Pos2Nat.inj_lt (compat "8.3"). +Notation Pgt_gt := Pos2Nat.inj_gt (compat "8.3"). +Notation Ple_le := Pos2Nat.inj_le (compat "8.3"). +Notation Pge_ge := Pos2Nat.inj_ge (compat "8.3"). +Notation Pminus_minus := Pos2Nat.inj_sub (compat "8.3"). +Notation iter_nat_of_P := @Pos2Nat.inj_iter (compat "8.3"). + +Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (compat "8.3"). +Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (compat "8.3"). + +Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (compat "8.3"). +Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (compat "8.3"). +Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (compat "8.3"). +Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (compat "8.3"). +Notation lt_O_nat_of_P := Pos2Nat.is_pos (compat "8.3"). +Notation ZL4 := Pos2Nat.is_succ (compat "8.3"). +Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (compat "8.3"). +Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (compat "8.3"). +Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (compat "8.3"). Lemma nat_of_P_minus_morphism p q : Pcompare p q Eq = Gt -> Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index f3f7b850e..0f709d686 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1375,87 +1375,87 @@ Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope. (** Compatibility Notations *) -Notation Zdouble_plus_one := Z.succ_double (only parsing). -Notation Zdouble_minus_one := Z.pred_double (only parsing). -Notation Zdouble := Z.double (only parsing). -Notation ZPminus := Z.pos_sub (only parsing). -Notation Zsucc' := Z.succ (only parsing). -Notation Zpred' := Z.pred (only parsing). -Notation Zplus' := Z.add (only parsing). -Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) -Notation Zopp := Z.opp (only parsing). -Notation Zsucc := Z.succ (only parsing). -Notation Zpred := Z.pred (only parsing). -Notation Zminus := Z.sub (only parsing). -Notation Zmult := Z.mul (only parsing). -Notation Zcompare := Z.compare (only parsing). -Notation Zsgn := Z.sgn (only parsing). -Notation Zle := Z.le (only parsing). -Notation Zge := Z.ge (only parsing). -Notation Zlt := Z.lt (only parsing). -Notation Zgt := Z.gt (only parsing). -Notation Zmax := Z.max (only parsing). -Notation Zmin := Z.min (only parsing). -Notation Zabs := Z.abs (only parsing). -Notation Zabs_nat := Z.abs_nat (only parsing). -Notation Zabs_N := Z.abs_N (only parsing). -Notation Z_of_nat := Z.of_nat (only parsing). -Notation Z_of_N := Z.of_N (only parsing). - -Notation Zind := Z.peano_ind (only parsing). -Notation Zopp_0 := Z.opp_0 (only parsing). -Notation Zopp_neg := Z.opp_Zneg (only parsing). -Notation Zopp_involutive := Z.opp_involutive (only parsing). -Notation Zopp_inj := Z.opp_inj (only parsing). -Notation Zplus_0_l := Z.add_0_l (only parsing). -Notation Zplus_0_r := Z.add_0_r (only parsing). -Notation Zplus_comm := Z.add_comm (only parsing). -Notation Zopp_plus_distr := Z.opp_add_distr (only parsing). -Notation Zopp_succ := Z.opp_succ (only parsing). -Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing). -Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing). -Notation Zplus_assoc := Z.add_assoc (only parsing). -Notation Zplus_permute := Z.add_shuffle3 (only parsing). -Notation Zplus_reg_l := Z.add_reg_l (only parsing). -Notation Zplus_succ_l := Z.add_succ_l (only parsing). -Notation Zplus_succ_comm := Z.add_succ_comm (only parsing). -Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing). -Notation Zsucc_inj := Z.succ_inj (only parsing). -Notation Zsucc'_inj := Z.succ_inj (only parsing). -Notation Zsucc'_pred' := Z.succ_pred (only parsing). -Notation Zpred'_succ' := Z.pred_succ (only parsing). -Notation Zpred'_inj := Z.pred_inj (only parsing). -Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing). -Notation Zminus_0_r := Z.sub_0_r (only parsing). -Notation Zminus_diag := Z.sub_diag (only parsing). -Notation Zminus_plus_distr := Z.sub_add_distr (only parsing). -Notation Zminus_succ_r := Z.sub_succ_r (only parsing). -Notation Zminus_plus := Z.add_simpl_l (only parsing). -Notation Zmult_0_l := Z.mul_0_l (only parsing). -Notation Zmult_0_r := Z.mul_0_r (only parsing). -Notation Zmult_1_l := Z.mul_1_l (only parsing). -Notation Zmult_1_r := Z.mul_1_r (only parsing). -Notation Zmult_comm := Z.mul_comm (only parsing). -Notation Zmult_assoc := Z.mul_assoc (only parsing). -Notation Zmult_permute := Z.mul_shuffle3 (only parsing). -Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing). -Notation Zdouble_mult := Z.double_spec (only parsing). -Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing). -Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing). -Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing). -Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing). -Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing). -Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing). -Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing). -Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing). -Notation Zmult_reg_l := Z.mul_reg_l (only parsing). -Notation Zmult_reg_r := Z.mul_reg_r (only parsing). -Notation Zmult_succ_l := Z.mul_succ_l (only parsing). -Notation Zmult_succ_r := Z.mul_succ_r (only parsing). -Notation Zpos_xI := Z.pos_xI (only parsing). -Notation Zpos_xO := Z.pos_xO (only parsing). -Notation Zneg_xI := Z.neg_xI (only parsing). -Notation Zneg_xO := Z.neg_xO (only parsing). +Notation Zdouble_plus_one := Z.succ_double (compat "8.3"). +Notation Zdouble_minus_one := Z.pred_double (compat "8.3"). +Notation Zdouble := Z.double (compat "8.3"). +Notation ZPminus := Z.pos_sub (compat "8.3"). +Notation Zsucc' := Z.succ (compat "8.3"). +Notation Zpred' := Z.pred (compat "8.3"). +Notation Zplus' := Z.add (compat "8.3"). +Notation Zplus := Z.add (compat "8.3"). (* Slightly incompatible *) +Notation Zopp := Z.opp (compat "8.3"). +Notation Zsucc := Z.succ (compat "8.3"). +Notation Zpred := Z.pred (compat "8.3"). +Notation Zminus := Z.sub (compat "8.3"). +Notation Zmult := Z.mul (compat "8.3"). +Notation Zcompare := Z.compare (compat "8.3"). +Notation Zsgn := Z.sgn (compat "8.3"). +Notation Zle := Z.le (compat "8.3"). +Notation Zge := Z.ge (compat "8.3"). +Notation Zlt := Z.lt (compat "8.3"). +Notation Zgt := Z.gt (compat "8.3"). +Notation Zmax := Z.max (compat "8.3"). +Notation Zmin := Z.min (compat "8.3"). +Notation Zabs := Z.abs (compat "8.3"). +Notation Zabs_nat := Z.abs_nat (compat "8.3"). +Notation Zabs_N := Z.abs_N (compat "8.3"). +Notation Z_of_nat := Z.of_nat (compat "8.3"). +Notation Z_of_N := Z.of_N (compat "8.3"). + +Notation Zind := Z.peano_ind (compat "8.3"). +Notation Zopp_0 := Z.opp_0 (compat "8.3"). +Notation Zopp_neg := Z.opp_Zneg (compat "8.3"). +Notation Zopp_involutive := Z.opp_involutive (compat "8.3"). +Notation Zopp_inj := Z.opp_inj (compat "8.3"). +Notation Zplus_0_l := Z.add_0_l (compat "8.3"). +Notation Zplus_0_r := Z.add_0_r (compat "8.3"). +Notation Zplus_comm := Z.add_comm (compat "8.3"). +Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3"). +Notation Zopp_succ := Z.opp_succ (compat "8.3"). +Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3"). +Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3"). +Notation Zplus_assoc := Z.add_assoc (compat "8.3"). +Notation Zplus_permute := Z.add_shuffle3 (compat "8.3"). +Notation Zplus_reg_l := Z.add_reg_l (compat "8.3"). +Notation Zplus_succ_l := Z.add_succ_l (compat "8.3"). +Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3"). +Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zsucc_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.3"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.3"). +Notation Zpred'_inj := Z.pred_inj (compat "8.3"). +Notation Zsucc'_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zminus_0_r := Z.sub_0_r (compat "8.3"). +Notation Zminus_diag := Z.sub_diag (compat "8.3"). +Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3"). +Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3"). +Notation Zminus_plus := Z.add_simpl_l (compat "8.3"). +Notation Zmult_0_l := Z.mul_0_l (compat "8.3"). +Notation Zmult_0_r := Z.mul_0_r (compat "8.3"). +Notation Zmult_1_l := Z.mul_1_l (compat "8.3"). +Notation Zmult_1_r := Z.mul_1_r (compat "8.3"). +Notation Zmult_comm := Z.mul_comm (compat "8.3"). +Notation Zmult_assoc := Z.mul_assoc (compat "8.3"). +Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3"). +Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3"). +Notation Zdouble_mult := Z.double_spec (compat "8.3"). +Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3"). +Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3"). +Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3"). +Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3"). +Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3"). +Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3"). +Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3"). +Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3"). +Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3"). +Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3"). +Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3"). +Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3"). +Notation Zpos_xI := Z.pos_xI (compat "8.3"). +Notation Zpos_xO := Z.pos_xO (compat "8.3"). +Notation Zneg_xI := Z.neg_xI (compat "8.3"). +Notation Zneg_xO := Z.neg_xO (compat "8.3"). Notation Z := Z (only parsing). Notation Z_rect := Z_rect (only parsing). diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 76308e60b..ca26787bd 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -36,7 +36,7 @@ Proof. intro; apply Zcompare_rect. Defined. -Notation Z_eq_dec := Z.eq_dec (only parsing). +Notation Z_eq_dec := Z.eq_dec (compat "8.3"). Section decidability. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 23473e932..2e43b3554 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -27,17 +27,17 @@ Local Open Scope Z_scope. (**********************************************************************) (** * Properties of absolute value *) -Notation Zabs_eq := Z.abs_eq (only parsing). -Notation Zabs_non_eq := Z.abs_neq (only parsing). -Notation Zabs_Zopp := Z.abs_opp (only parsing). -Notation Zabs_pos := Z.abs_nonneg (only parsing). -Notation Zabs_involutive := Z.abs_involutive (only parsing). -Notation Zabs_eq_case := Z.abs_eq_cases (only parsing). -Notation Zabs_triangle := Z.abs_triangle (only parsing). -Notation Zsgn_Zabs := Z.sgn_abs (only parsing). -Notation Zabs_Zsgn := Z.abs_sgn (only parsing). -Notation Zabs_Zmult := Z.abs_mul (only parsing). -Notation Zabs_square := Z.abs_square (only parsing). +Notation Zabs_eq := Z.abs_eq (compat "8.3"). +Notation Zabs_non_eq := Z.abs_neq (compat "8.3"). +Notation Zabs_Zopp := Z.abs_opp (compat "8.3"). +Notation Zabs_pos := Z.abs_nonneg (compat "8.3"). +Notation Zabs_involutive := Z.abs_involutive (compat "8.3"). +Notation Zabs_eq_case := Z.abs_eq_cases (compat "8.3"). +Notation Zabs_triangle := Z.abs_triangle (compat "8.3"). +Notation Zsgn_Zabs := Z.sgn_abs (compat "8.3"). +Notation Zabs_Zsgn := Z.abs_sgn (compat "8.3"). +Notation Zabs_Zmult := Z.abs_mul (compat "8.3"). +Notation Zabs_square := Z.abs_square (compat "8.3"). (** * Proving a property of the absolute value by cases *) @@ -68,11 +68,11 @@ Qed. (** * Some results about the sign function. *) -Notation Zsgn_Zmult := Z.sgn_mul (only parsing). -Notation Zsgn_Zopp := Z.sgn_opp (only parsing). -Notation Zsgn_pos := Z.sgn_pos_iff (only parsing). -Notation Zsgn_neg := Z.sgn_neg_iff (only parsing). -Notation Zsgn_null := Z.sgn_null_iff (only parsing). +Notation Zsgn_Zmult := Z.sgn_mul (compat "8.3"). +Notation Zsgn_Zopp := Z.sgn_opp (compat "8.3"). +Notation Zsgn_pos := Z.sgn_pos_iff (compat "8.3"). +Notation Zsgn_neg := Z.sgn_neg_iff (compat "8.3"). +Notation Zsgn_null := Z.sgn_null_iff (compat "8.3"). (** A characterization of the sign function: *) @@ -86,13 +86,13 @@ Qed. (** Compatibility *) -Notation inj_Zabs_nat := Zabs2Nat.id_abs (only parsing). -Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (only parsing). -Notation Zabs_nat_mult := Zabs2Nat.inj_mul (only parsing). -Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (only parsing). -Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (only parsing). -Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (only parsing). -Notation Zabs_nat_compare := Zabs2Nat.inj_compare (only parsing). +Notation inj_Zabs_nat := Zabs2Nat.id_abs (compat "8.3"). +Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (compat "8.3"). +Notation Zabs_nat_mult := Zabs2Nat.inj_mul (compat "8.3"). +Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (compat "8.3"). +Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (compat "8.3"). +Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (compat "8.3"). +Notation Zabs_nat_compare := Zabs2Nat.inj_compare (compat "8.3"). Lemma Zabs_nat_le n m : 0 <= n <= m -> (Z.abs_nat n <= Z.abs_nat m)%nat. Proof. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index d09012820..7c1e096ed 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -33,10 +33,10 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). (**********************************************************************) (** * Boolean comparisons of binary integers *) -Notation Zle_bool := Z.leb (only parsing). -Notation Zge_bool := Z.geb (only parsing). -Notation Zlt_bool := Z.ltb (only parsing). -Notation Zgt_bool := Z.gtb (only parsing). +Notation Zle_bool := Z.leb (compat "8.3"). +Notation Zge_bool := Z.geb (compat "8.3"). +Notation Zlt_bool := Z.ltb (compat "8.3"). +Notation Zgt_bool := Z.gtb (compat "8.3"). (** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare]. The old [Zeq_bool] is kept for compatibility. *) @@ -87,7 +87,7 @@ Proof. apply Z.leb_le. Qed. -Notation Zle_bool_refl := Z.leb_refl (only parsing). +Notation Zle_bool_refl := Z.leb_refl (compat "8.3"). Lemma Zle_bool_antisym n m : (n <=? m) = true -> (m <=? n) = true -> n = m. diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 20e1b006a..703a3972f 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -181,18 +181,18 @@ Qed. (** Compatibility notations *) -Notation Zcompare_refl := Z.compare_refl (only parsing). -Notation Zcompare_Eq_eq := Z.compare_eq (only parsing). -Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing). -Notation Zcompare_spec := Z.compare_spec (only parsing). -Notation Zmin_l := Z.min_l (only parsing). -Notation Zmin_r := Z.min_r (only parsing). -Notation Zmax_l := Z.max_l (only parsing). -Notation Zmax_r := Z.max_r (only parsing). -Notation Zabs_eq := Z.abs_eq (only parsing). -Notation Zabs_non_eq := Z.abs_neq (only parsing). -Notation Zsgn_0 := Z.sgn_null (only parsing). -Notation Zsgn_1 := Z.sgn_pos (only parsing). -Notation Zsgn_m1 := Z.sgn_neg (only parsing). +Notation Zcompare_refl := Z.compare_refl (compat "8.3"). +Notation Zcompare_Eq_eq := Z.compare_eq (compat "8.3"). +Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (compat "8.3"). +Notation Zcompare_spec := Z.compare_spec (compat "8.3"). +Notation Zmin_l := Z.min_l (compat "8.3"). +Notation Zmin_r := Z.min_r (compat "8.3"). +Notation Zmax_l := Z.max_l (compat "8.3"). +Notation Zmax_r := Z.max_r (compat "8.3"). +Notation Zabs_eq := Z.abs_eq (compat "8.3"). +Notation Zabs_non_eq := Z.abs_neq (compat "8.3"). +Notation Zsgn_0 := Z.sgn_null (compat "8.3"). +Notation Zsgn_1 := Z.sgn_pos (compat "8.3"). +Notation Zsgn_m1 := Z.sgn_neg (compat "8.3"). (** Not kept: Zcompare_egal_dec *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 314f696a2..057fd6d34 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -18,16 +18,16 @@ Local Open Scope Z_scope. (** The definition of the division is now in [BinIntDef], the initial specifications and properties are in [BinInt]. *) -Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing). -Notation Zdiv_eucl := Z.div_eucl (only parsing). -Notation Zdiv := Z.div (only parsing). -Notation Zmod := Z.modulo (only parsing). - -Notation Zdiv_eucl_eq := Z.div_eucl_eq (only parsing). -Notation Z_div_mod_eq_full := Z.div_mod (only parsing). -Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing). -Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing). -Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing). +Notation Zdiv_eucl_POS := Z.pos_div_eucl (compat "8.3"). +Notation Zdiv_eucl := Z.div_eucl (compat "8.3"). +Notation Zdiv := Z.div (compat "8.3"). +Notation Zmod := Z.modulo (compat "8.3"). + +Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.3"). +Notation Z_div_mod_eq_full := Z.div_mod (compat "8.3"). +Notation Zmod_POS_bound := Z.pos_div_eucl_bound (compat "8.3"). +Notation Zmod_pos_bound := Z.mod_pos_bound (compat "8.3"). +Notation Zmod_neg_bound := Z.mod_neg_bound (compat "8.3"). (** * Main division theorems *) diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 8e6cc07bf..a032a801d 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -58,8 +58,8 @@ Proof (Zodd_equiv n). (** Boolean tests of parity (now in BinInt.Z) *) -Notation Zeven_bool := Z.even (only parsing). -Notation Zodd_bool := Z.odd (only parsing). +Notation Zeven_bool := Z.even (compat "8.3"). +Notation Zodd_bool := Z.odd (compat "8.3"). Lemma Zeven_bool_iff n : Z.even n = true <-> Zeven n. Proof. @@ -130,17 +130,17 @@ Qed. Hint Unfold Zeven Zodd: zarith. -Notation Zeven_bool_succ := Z.even_succ (only parsing). -Notation Zeven_bool_pred := Z.even_pred (only parsing). -Notation Zodd_bool_succ := Z.odd_succ (only parsing). -Notation Zodd_bool_pred := Z.odd_pred (only parsing). +Notation Zeven_bool_succ := Z.even_succ (compat "8.3"). +Notation Zeven_bool_pred := Z.even_pred (compat "8.3"). +Notation Zodd_bool_succ := Z.odd_succ (compat "8.3"). +Notation Zodd_bool_pred := Z.odd_pred (compat "8.3"). (******************************************************************) (** * Definition of [Zquot2], [Zdiv2] and properties wrt [Zeven] and [Zodd] *) -Notation Zdiv2 := Z.div2 (only parsing). -Notation Zquot2 := Z.quot2 (only parsing). +Notation Zdiv2 := Z.div2 (compat "8.3"). +Notation Zquot2 := Z.quot2 (compat "8.3"). (** Properties of [Z.div2] *) diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 999564f03..a3eeb4160 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -104,8 +104,8 @@ Qed. (* begin hide *) (* Compatibility *) -Notation Zmax1 := Z.le_max_l (only parsing). -Notation Zmax2 := Z.le_max_r (only parsing). -Notation Zmax_irreducible_inf := Z.max_dec (only parsing). -Notation Zmax_le_prime_inf := Z.max_le (only parsing). +Notation Zmax1 := Z.le_max_l (compat "8.3"). +Notation Zmax2 := Z.le_max_r (compat "8.3"). +Notation Zmax_irreducible_inf := Z.max_dec (compat "8.3"). +Notation Zmax_le_prime_inf := Z.max_le (compat "8.3"). (* end hide *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 2c5003a6d..fbb31632c 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -45,7 +45,7 @@ Proof Z.min_le_compat_l. (** * Semi-lattice properties of min *) Lemma Zmin_idempotent : forall n, Z.min n n = n. Proof Z.min_id. -Notation Zmin_n_n := Z.min_id (only parsing). +Notation Zmin_n_n := Z.min_id (compat "8.3"). Lemma Zmin_comm : forall n m, Z.min n m = Z.min m n. Proof Z.min_comm. Lemma Zmin_assoc : forall n m p, Z.min n (Z.min m p) = Z.min (Z.min n m) p. Proof Z.min_assoc. diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index 8908175f6..8c22efc30 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -12,11 +12,11 @@ Require Import Orders BinInt Zcompare Zorder. (*begin hide*) (* Compatibility with names of the old Zminmax file *) -Notation Zmin_max_absorption_r_r := Z.min_max_absorption (only parsing). -Notation Zmax_min_absorption_r_r := Z.max_min_absorption (only parsing). -Notation Zmax_min_distr_r := Z.max_min_distr (only parsing). -Notation Zmin_max_distr_r := Z.min_max_distr (only parsing). -Notation Zmax_min_modular_r := Z.max_min_modular (only parsing). -Notation Zmin_max_modular_r := Z.min_max_modular (only parsing). -Notation max_min_disassoc := Z.max_min_disassoc (only parsing). +Notation Zmin_max_absorption_r_r := Z.min_max_absorption (compat "8.3"). +Notation Zmax_min_absorption_r_r := Z.max_min_absorption (compat "8.3"). +Notation Zmax_min_distr_r := Z.max_min_distr (compat "8.3"). +Notation Zmin_max_distr_r := Z.min_max_distr (compat "8.3"). +Notation Zmax_min_modular_r := Z.max_min_modular (compat "8.3"). +Notation Zmin_max_modular_r := Z.min_max_modular (compat "8.3"). +Notation max_min_disassoc := Z.max_min_disassoc (compat "8.3"). (*end hide*) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index ff844ec28..a6da9d7e7 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -18,7 +18,7 @@ Open Local Scope Z_scope. (** [n]th iteration of the function [f] *) -Notation iter := @Z.iter (only parsing). +Notation iter := @Z.iter (compat "8.3"). Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> iter n A f x = iter_nat (Z.abs_nat n) A f x. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index e3843990c..2c3288f6c 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -931,65 +931,65 @@ Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m). (** For the others, a Notation is fine *) -Notation inj_0 := Nat2Z.inj_0 (only parsing). -Notation inj_S := Nat2Z.inj_succ (only parsing). -Notation inj_compare := Nat2Z.inj_compare (only parsing). -Notation inj_eq_rev := Nat2Z.inj (only parsing). -Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (only parsing). -Notation inj_le_iff := Nat2Z.inj_le (only parsing). -Notation inj_lt_iff := Nat2Z.inj_lt (only parsing). -Notation inj_ge_iff := Nat2Z.inj_ge (only parsing). -Notation inj_gt_iff := Nat2Z.inj_gt (only parsing). -Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (only parsing). -Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (only parsing). -Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (only parsing). -Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (only parsing). -Notation inj_plus := Nat2Z.inj_add (only parsing). -Notation inj_mult := Nat2Z.inj_mul (only parsing). -Notation inj_minus1 := Nat2Z.inj_sub (only parsing). -Notation inj_minus := Nat2Z.inj_sub_max (only parsing). -Notation inj_min := Nat2Z.inj_min (only parsing). -Notation inj_max := Nat2Z.inj_max (only parsing). - -Notation Z_of_nat_of_P := positive_nat_Z (only parsing). +Notation inj_0 := Nat2Z.inj_0 (compat "8.3"). +Notation inj_S := Nat2Z.inj_succ (compat "8.3"). +Notation inj_compare := Nat2Z.inj_compare (compat "8.3"). +Notation inj_eq_rev := Nat2Z.inj (compat "8.3"). +Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (compat "8.3"). +Notation inj_le_iff := Nat2Z.inj_le (compat "8.3"). +Notation inj_lt_iff := Nat2Z.inj_lt (compat "8.3"). +Notation inj_ge_iff := Nat2Z.inj_ge (compat "8.3"). +Notation inj_gt_iff := Nat2Z.inj_gt (compat "8.3"). +Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (compat "8.3"). +Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (compat "8.3"). +Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (compat "8.3"). +Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (compat "8.3"). +Notation inj_plus := Nat2Z.inj_add (compat "8.3"). +Notation inj_mult := Nat2Z.inj_mul (compat "8.3"). +Notation inj_minus1 := Nat2Z.inj_sub (compat "8.3"). +Notation inj_minus := Nat2Z.inj_sub_max (compat "8.3"). +Notation inj_min := Nat2Z.inj_min (compat "8.3"). +Notation inj_max := Nat2Z.inj_max (compat "8.3"). + +Notation Z_of_nat_of_P := positive_nat_Z (compat "8.3"). Notation Zpos_eq_Z_of_nat_o_nat_of_P := - (fun p => sym_eq (positive_nat_Z p)) (only parsing). - -Notation Z_of_nat_of_N := N_nat_Z (only parsing). -Notation Z_of_N_of_nat := nat_N_Z (only parsing). - -Notation Z_of_N_eq := (f_equal Z.of_N) (only parsing). -Notation Z_of_N_eq_rev := N2Z.inj (only parsing). -Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (only parsing). -Notation Z_of_N_compare := N2Z.inj_compare (only parsing). -Notation Z_of_N_le_iff := N2Z.inj_le (only parsing). -Notation Z_of_N_lt_iff := N2Z.inj_lt (only parsing). -Notation Z_of_N_ge_iff := N2Z.inj_ge (only parsing). -Notation Z_of_N_gt_iff := N2Z.inj_gt (only parsing). -Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (only parsing). -Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (only parsing). -Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (only parsing). -Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (only parsing). -Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (only parsing). -Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (only parsing). -Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (only parsing). -Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (only parsing). -Notation Z_of_N_pos := N2Z.inj_pos (only parsing). -Notation Z_of_N_abs := N2Z.inj_abs_N (only parsing). -Notation Z_of_N_le_0 := N2Z.is_nonneg (only parsing). -Notation Z_of_N_plus := N2Z.inj_add (only parsing). -Notation Z_of_N_mult := N2Z.inj_mul (only parsing). -Notation Z_of_N_minus := N2Z.inj_sub_max (only parsing). -Notation Z_of_N_succ := N2Z.inj_succ (only parsing). -Notation Z_of_N_min := N2Z.inj_min (only parsing). -Notation Z_of_N_max := N2Z.inj_max (only parsing). -Notation Zabs_of_N := Zabs2N.id (only parsing). -Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (only parsing). -Notation Zabs_N_succ := Zabs2N.inj_succ (only parsing). -Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (only parsing). -Notation Zabs_N_plus := Zabs2N.inj_add (only parsing). -Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (only parsing). -Notation Zabs_N_mult := Zabs2N.inj_mul (only parsing). + (fun p => sym_eq (positive_nat_Z p)) (compat "8.3"). + +Notation Z_of_nat_of_N := N_nat_Z (compat "8.3"). +Notation Z_of_N_of_nat := nat_N_Z (compat "8.3"). + +Notation Z_of_N_eq := (f_equal Z.of_N) (compat "8.3"). +Notation Z_of_N_eq_rev := N2Z.inj (compat "8.3"). +Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (compat "8.3"). +Notation Z_of_N_compare := N2Z.inj_compare (compat "8.3"). +Notation Z_of_N_le_iff := N2Z.inj_le (compat "8.3"). +Notation Z_of_N_lt_iff := N2Z.inj_lt (compat "8.3"). +Notation Z_of_N_ge_iff := N2Z.inj_ge (compat "8.3"). +Notation Z_of_N_gt_iff := N2Z.inj_gt (compat "8.3"). +Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (compat "8.3"). +Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (compat "8.3"). +Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (compat "8.3"). +Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (compat "8.3"). +Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (compat "8.3"). +Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (compat "8.3"). +Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (compat "8.3"). +Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (compat "8.3"). +Notation Z_of_N_pos := N2Z.inj_pos (compat "8.3"). +Notation Z_of_N_abs := N2Z.inj_abs_N (compat "8.3"). +Notation Z_of_N_le_0 := N2Z.is_nonneg (compat "8.3"). +Notation Z_of_N_plus := N2Z.inj_add (compat "8.3"). +Notation Z_of_N_mult := N2Z.inj_mul (compat "8.3"). +Notation Z_of_N_minus := N2Z.inj_sub_max (compat "8.3"). +Notation Z_of_N_succ := N2Z.inj_succ (compat "8.3"). +Notation Z_of_N_min := N2Z.inj_min (compat "8.3"). +Notation Z_of_N_max := N2Z.inj_max (compat "8.3"). +Notation Zabs_of_N := Zabs2N.id (compat "8.3"). +Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (compat "8.3"). +Notation Zabs_N_succ := Zabs2N.inj_succ (compat "8.3"). +Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (compat "8.3"). +Notation Zabs_N_plus := Zabs2N.inj_add (compat "8.3"). +Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (compat "8.3"). +Notation Zabs_N_mult := Zabs2N.inj_mul (compat "8.3"). Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0. Proof. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 814b67322..00019b1a3 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -25,20 +25,20 @@ Open Scope Z_scope. - properties of the efficient [Z.gcd] function *) -Notation Zgcd := Z.gcd (only parsing). -Notation Zggcd := Z.ggcd (only parsing). -Notation Zggcd_gcd := Z.ggcd_gcd (only parsing). -Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing). -Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing). -Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing). -Notation Zgcd_greatest := Z.gcd_greatest (only parsing). -Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing). -Notation Zggcd_opp := Z.ggcd_opp (only parsing). +Notation Zgcd := Z.gcd (compat "8.3"). +Notation Zggcd := Z.ggcd (compat "8.3"). +Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.3"). +Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.3"). +Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.3"). +Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.3"). +Notation Zgcd_greatest := Z.gcd_greatest (compat "8.3"). +Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.3"). +Notation Zggcd_opp := Z.ggcd_opp (compat "8.3"). (** The former specialized inductive predicate [Zdivide] is now a generic existential predicate. *) -Notation Zdivide := Z.divide (only parsing). +Notation Zdivide := Z.divide (compat "8.3"). (** Its former constructor is now a pseudo-constructor. *) @@ -46,17 +46,17 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H. (** Results concerning divisibility*) -Notation Zdivide_refl := Z.divide_refl (only parsing). -Notation Zone_divide := Z.divide_1_l (only parsing). -Notation Zdivide_0 := Z.divide_0_r (only parsing). -Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing). -Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing). -Notation Zdivide_plus_r := Z.divide_add_r (only parsing). -Notation Zdivide_minus_l := Z.divide_sub_r (only parsing). -Notation Zdivide_mult_l := Z.divide_mul_l (only parsing). -Notation Zdivide_mult_r := Z.divide_mul_r (only parsing). -Notation Zdivide_factor_r := Z.divide_factor_l (only parsing). -Notation Zdivide_factor_l := Z.divide_factor_r (only parsing). +Notation Zdivide_refl := Z.divide_refl (compat "8.3"). +Notation Zone_divide := Z.divide_1_l (compat "8.3"). +Notation Zdivide_0 := Z.divide_0_r (compat "8.3"). +Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (compat "8.3"). +Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (compat "8.3"). +Notation Zdivide_plus_r := Z.divide_add_r (compat "8.3"). +Notation Zdivide_minus_l := Z.divide_sub_r (compat "8.3"). +Notation Zdivide_mult_l := Z.divide_mul_l (compat "8.3"). +Notation Zdivide_mult_r := Z.divide_mul_r (compat "8.3"). +Notation Zdivide_factor_r := Z.divide_factor_l (compat "8.3"). +Notation Zdivide_factor_l := Z.divide_factor_r (compat "8.3"). Lemma Zdivide_opp_r a b : (a | b) -> (a | - b). Proof. apply Z.divide_opp_r. Qed. @@ -91,12 +91,12 @@ Qed. (** Only [1] and [-1] divide [1]. *) -Notation Zdivide_1 := Z.divide_1_r (only parsing). +Notation Zdivide_1 := Z.divide_1_r (compat "8.3"). (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) -Notation Zdivide_antisym := Z.divide_antisym (only parsing). -Notation Zdivide_trans := Z.divide_trans (only parsing). +Notation Zdivide_antisym := Z.divide_antisym (compat "8.3"). +Notation Zdivide_trans := Z.divide_trans (compat "8.3"). (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) @@ -742,7 +742,7 @@ Qed. (** we now prove that [Z.gcd] is indeed a gcd in the sense of [Zis_gcd]. *) -Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing). +Notation Zgcd_is_pos := Z.gcd_nonneg (compat "8.3"). Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b). Proof. @@ -775,8 +775,8 @@ Proof. subst. now case (Z.gcd a b). Qed. -Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing). -Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing). +Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3"). +Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (compat "8.3"). Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Z.gcd a b -> @@ -806,16 +806,16 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Notation Zgcd_comm := Z.gcd_comm (only parsing). +Notation Zgcd_comm := Z.gcd_comm (compat "8.3"). Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). Proof. symmetry. apply Z.gcd_assoc. Qed. -Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing). -Notation Zgcd_0 := Z.gcd_0_r (only parsing). -Notation Zgcd_1 := Z.gcd_1_r (only parsing). +Notation Zgcd_Zabs := Z.gcd_abs_l (compat "8.3"). +Notation Zgcd_0 := Z.gcd_0_r (compat "8.3"). +Notation Zgcd_1 := Z.gcd_1_r (compat "8.3"). Hint Resolve Zgcd_0 Zgcd_1 : zarith. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index a8cd69bb3..d22e2d57c 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -38,9 +38,9 @@ Qed. (**********************************************************************) (** * Decidability of equality and order on Z *) -Notation dec_eq := Z.eq_decidable (only parsing). -Notation dec_Zle := Z.le_decidable (only parsing). -Notation dec_Zlt := Z.lt_decidable (only parsing). +Notation dec_eq := Z.eq_decidable (compat "8.3"). +Notation dec_Zle := Z.le_decidable (compat "8.3"). +Notation dec_Zlt := Z.lt_decidable (compat "8.3"). Theorem dec_Zne n m : decidable (Zne n m). Proof. @@ -64,12 +64,12 @@ Qed. (** * Relating strict and large orders *) -Notation Zgt_lt := Z.gt_lt (only parsing). -Notation Zlt_gt := Z.lt_gt (only parsing). -Notation Zge_le := Z.ge_le (only parsing). -Notation Zle_ge := Z.le_ge (only parsing). -Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). -Notation Zge_iff_le := Z.ge_le_iff (only parsing). +Notation Zgt_lt := Z.gt_lt (compat "8.3"). +Notation Zlt_gt := Z.lt_gt (compat "8.3"). +Notation Zge_le := Z.ge_le (compat "8.3"). +Notation Zle_ge := Z.le_ge (compat "8.3"). +Notation Zgt_iff_lt := Z.gt_lt_iff (compat "8.3"). +Notation Zge_iff_le := Z.ge_le_iff (compat "8.3"). Lemma Zle_not_lt n m : n <= m -> ~ m < n. Proof. @@ -121,18 +121,18 @@ Qed. (** Reflexivity *) -Notation Zle_refl := Z.le_refl (only parsing). -Notation Zeq_le := Z.eq_le_incl (only parsing). +Notation Zle_refl := Z.le_refl (compat "8.3"). +Notation Zeq_le := Z.eq_le_incl (compat "8.3"). Hint Resolve Z.le_refl: zarith. (** Antisymmetry *) -Notation Zle_antisym := Z.le_antisymm (only parsing). +Notation Zle_antisym := Z.le_antisymm (compat "8.3"). (** Asymmetry *) -Notation Zlt_asym := Z.lt_asymm (only parsing). +Notation Zlt_asym := Z.lt_asymm (compat "8.3"). Lemma Zgt_asym n m : n > m -> ~ m > n. Proof. @@ -141,8 +141,8 @@ Qed. (** Irreflexivity *) -Notation Zlt_irrefl := Z.lt_irrefl (only parsing). -Notation Zlt_not_eq := Z.lt_neq (only parsing). +Notation Zlt_irrefl := Z.lt_irrefl (compat "8.3"). +Notation Zlt_not_eq := Z.lt_neq (compat "8.3"). Lemma Zgt_irrefl n : ~ n > n. Proof. @@ -151,8 +151,8 @@ Qed. (** Large = strict or equal *) -Notation Zlt_le_weak := Z.lt_le_incl (only parsing). -Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing). +Notation Zlt_le_weak := Z.lt_le_incl (compat "8.3"). +Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (compat "8.3"). Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m. Proof. @@ -161,19 +161,19 @@ Qed. (** Dichotomy *) -Notation Zle_or_lt := Z.le_gt_cases (only parsing). +Notation Zle_or_lt := Z.le_gt_cases (compat "8.3"). (** Transitivity of strict orders *) -Notation Zlt_trans := Z.lt_trans (only parsing). +Notation Zlt_trans := Z.lt_trans (compat "8.3"). Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p. Proof Zcompare_Gt_trans. (** Mixed transitivity *) -Notation Zlt_le_trans := Z.lt_le_trans (only parsing). -Notation Zle_lt_trans := Z.le_lt_trans (only parsing). +Notation Zlt_le_trans := Z.lt_le_trans (compat "8.3"). +Notation Zle_lt_trans := Z.le_lt_trans (compat "8.3"). Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p. Proof. @@ -187,7 +187,7 @@ Qed. (** Transitivity of large orders *) -Notation Zle_trans := Z.le_trans (only parsing). +Notation Zle_trans := Z.le_trans (compat "8.3"). Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p. Proof. @@ -238,8 +238,8 @@ Qed. (** Special base instances of order *) -Notation Zlt_succ := Z.lt_succ_diag_r (only parsing). -Notation Zlt_pred := Z.lt_pred_l (only parsing). +Notation Zlt_succ := Z.lt_succ_diag_r (compat "8.3"). +Notation Zlt_pred := Z.lt_pred_l (compat "8.3"). Lemma Zgt_succ n : Z.succ n > n. Proof. @@ -253,8 +253,8 @@ Qed. (** Relating strict and large order using successor or predecessor *) -Notation Zlt_succ_r := Z.lt_succ_r (only parsing). -Notation Zle_succ_l := Z.le_succ_l (only parsing). +Notation Zlt_succ_r := Z.lt_succ_r (compat "8.3"). +Notation Zle_succ_l := Z.le_succ_l (compat "8.3"). Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m. Proof. @@ -293,10 +293,10 @@ Qed. (** Weakening order *) -Notation Zle_succ := Z.le_succ_diag_r (only parsing). -Notation Zle_pred := Z.le_pred_l (only parsing). -Notation Zlt_lt_succ := Z.lt_lt_succ_r (only parsing). -Notation Zle_le_succ := Z.le_le_succ_r (only parsing). +Notation Zle_succ := Z.le_succ_diag_r (compat "8.3"). +Notation Zle_pred := Z.le_pred_l (compat "8.3"). +Notation Zlt_lt_succ := Z.lt_lt_succ_r (compat "8.3"). +Notation Zle_le_succ := Z.le_le_succ_r (compat "8.3"). Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m. Proof. @@ -332,8 +332,8 @@ Qed. (** Special cases of ordered integers *) -Notation Zlt_0_1 := Z.lt_0_1 (only parsing). -Notation Zle_0_1 := Z.le_0_1 (only parsing). +Notation Zlt_0_1 := Z.lt_0_1 (compat "8.3"). +Notation Zle_0_1 := Z.le_0_1 (compat "8.3"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. @@ -373,10 +373,10 @@ Qed. (** ** Addition *) (** Compatibility of addition wrt to order *) -Notation Zplus_lt_le_compat := Z.add_lt_le_mono (only parsing). -Notation Zplus_le_lt_compat := Z.add_le_lt_mono (only parsing). -Notation Zplus_le_compat := Z.add_le_mono (only parsing). -Notation Zplus_lt_compat := Z.add_lt_mono (only parsing). +Notation Zplus_lt_le_compat := Z.add_lt_le_mono (compat "8.3"). +Notation Zplus_le_lt_compat := Z.add_le_lt_mono (compat "8.3"). +Notation Zplus_le_compat := Z.add_le_mono (compat "8.3"). +Notation Zplus_lt_compat := Z.add_lt_mono (compat "8.3"). Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m. Proof. @@ -410,7 +410,7 @@ Qed. (** Compatibility of addition wrt to being positive *) -Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing). +Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (compat "8.3"). (** Simplification of addition wrt to order *) @@ -568,9 +568,9 @@ Qed. (** Compatibility of multiplication by a positive wrt to being positive *) -Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (only parsing). -Notation Zmult_lt_0_compat := Z.mul_pos_pos (only parsing). -Notation Zmult_lt_O_compat := Z.mul_pos_pos (only parsing). +Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (compat "8.3"). +Notation Zmult_lt_0_compat := Z.mul_pos_pos (compat "8.3"). +Notation Zmult_lt_O_compat := Z.mul_pos_pos (compat "8.3"). Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0. Proof. @@ -622,9 +622,9 @@ Qed. (** * Equivalence between inequalities *) -Notation Zle_plus_swap := Z.le_add_le_sub_r (only parsing). -Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (only parsing). -Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (only parsing). +Notation Zle_plus_swap := Z.le_add_le_sub_r (compat "8.3"). +Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (compat "8.3"). +Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (compat "8.3"). Lemma Zeq_plus_swap n m p : n + p = m <-> n = m - p. Proof. diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 6f1ebc061..4fe411584 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -14,12 +14,12 @@ Local Open Scope Z_scope. (** Nota : this file is mostly deprecated. The definition of [Z.pow] and its usual properties are now provided by module [BinInt.Z]. *) -Notation Zpower_pos := Z.pow_pos (only parsing). -Notation Zpower := Z.pow (only parsing). -Notation Zpower_0_r := Z.pow_0_r (only parsing). -Notation Zpower_succ_r := Z.pow_succ_r (only parsing). -Notation Zpower_neg_r := Z.pow_neg_r (only parsing). -Notation Zpower_Ppow := Z.pow_Zpos (only parsing). +Notation Zpower_pos := Z.pow_pos (compat "8.3"). +Notation Zpower := Z.pow (compat "8.3"). +Notation Zpower_0_r := Z.pow_0_r (compat "8.3"). +Notation Zpower_succ_r := Z.pow_succ_r (compat "8.3"). +Notation Zpower_neg_r := Z.pow_neg_r (compat "8.3"). +Notation Zpower_Ppow := Z.pow_Zpos (compat "8.3"). Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow. Proof. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 27e3def4e..5d025322b 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -29,17 +29,17 @@ Proof. now apply (Z.pow_0_l (Zpos p)). Qed. Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p. Proof. intros. now apply (Z.pow_pos_nonneg x (Zpos p)). Qed. -Notation Zpower_1_r := Z.pow_1_r (only parsing). -Notation Zpower_1_l := Z.pow_1_l (only parsing). -Notation Zpower_0_l := Z.pow_0_l' (only parsing). -Notation Zpower_0_r := Z.pow_0_r (only parsing). -Notation Zpower_2 := Z.pow_2_r (only parsing). -Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing). -Notation Zpower_ge_0 := Z.pow_nonneg (only parsing). -Notation Zpower_Zabs := Z.abs_pow (only parsing). -Notation Zpower_Zsucc := Z.pow_succ_r (only parsing). -Notation Zpower_mult := Z.pow_mul_r (only parsing). -Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing). +Notation Zpower_1_r := Z.pow_1_r (compat "8.3"). +Notation Zpower_1_l := Z.pow_1_l (compat "8.3"). +Notation Zpower_0_l := Z.pow_0_l' (compat "8.3"). +Notation Zpower_0_r := Z.pow_0_r (compat "8.3"). +Notation Zpower_2 := Z.pow_2_r (compat "8.3"). +Notation Zpower_gt_0 := Z.pow_pos_nonneg (compat "8.3"). +Notation Zpower_ge_0 := Z.pow_nonneg (compat "8.3"). +Notation Zpower_Zabs := Z.abs_pow (compat "8.3"). +Notation Zpower_Zsucc := Z.pow_succ_r (compat "8.3"). +Notation Zpower_mult := Z.pow_mul_r (compat "8.3"). +Notation Zpower_le_monotone2 := Z.pow_le_mono_r (compat "8.3"). Theorem Zpower_le_monotone a b c : 0 < a -> 0 <= b <= c -> a^b <= a^c. @@ -233,7 +233,7 @@ Qed. (** * Zsquare: a direct definition of [z^2] *) -Notation Psquare := Pos.square (only parsing). -Notation Zsquare := Z.square (only parsing). -Notation Psquare_correct := Pos.square_spec (only parsing). -Notation Zsquare_correct := Z.square_spec (only parsing). +Notation Psquare := Pos.square (compat "8.3"). +Notation Zsquare := Z.square (compat "8.3"). +Notation Psquare_correct := Pos.square_spec (compat "8.3"). +Notation Zsquare_correct := Z.square_spec (compat "8.3"). diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 9a95669f5..5b79fbce8 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -46,7 +46,7 @@ Qed. has been chosen to be [a], so this equation holds even for [b=0]. *) -Notation Z_quot_rem_eq := Z.quot_rem' (only parsing). +Notation Z_quot_rem_eq := Z.quot_rem' (compat "8.3"). (** Then, the inequalities constraining the remainder: The remainder is bounded by the divisor, in term of absolute values *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 08cbe0640..652d0f7c6 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -136,3 +136,11 @@ let init_ocaml_path () = [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; [ "grammar" ]; [ "ide" ] ] + +let get_compat_version = function + | "8.3" -> Flags.V8_3 + | "8.2" -> Flags.V8_2 + | ("8.1" | "8.0") as s -> + msg_warning (strbrk ("Compatibility with version "^s^" not supported.")); + Flags.V8_2 + | s -> Errors.error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 43b1556d5..4461f721d 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -22,3 +22,5 @@ val init_load_path : unit -> unit val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit + +val get_compat_version : string -> Flags.compat_version diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6e5019adb..1a6867a51 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -125,13 +125,6 @@ let compile_files () = Vernac.compile v f) (List.rev !compile_list) -let set_compat_version = function - | "8.3" -> compat_version := Some V8_3 - | "8.2" -> compat_version := Some V8_2 - | "8.1" -> msg_warning (strbrk "Compatibility with version 8.1 not supported.") - | "8.0" -> msg_warning (strbrk "Compatibility with version 8.0 not supported.") - | s -> error ("Unknown compatibility version \""^s^"\".") - (*s options for the virtual machine *) let boxed_val = ref false @@ -158,6 +151,9 @@ let warning s = msg_warning (strbrk s) let ide_slave = ref false let filter_opts = ref false +let verb_compat_ntn = ref false +let no_compat_ntn = ref false + let parse_args arglist = let glob_opt = ref false in let rec parse = function @@ -249,9 +245,13 @@ let parse_args arglist = | "-debug" :: rem -> set_debug (); parse rem - | "-compat" :: v :: rem -> set_compat_version v; parse rem + | "-compat" :: v :: rem -> + Flags.compat_version := get_compat_version v; parse rem | "-compat" :: [] -> usage () + | "-verb-compat-notations" :: rem -> verb_compat_ntn := true; parse rem + | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); @@ -342,6 +342,9 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + (* Be careful to set these variables after the inputstate *) + Syntax_def.set_verbose_compat_notations !verb_compat_ntn; + Syntax_def.set_compat_notations (not !no_compat_ntn); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index fee4fef18..52722c9f5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -770,7 +770,7 @@ let interp_modifiers modl = | SetAssoc a :: l -> if assoc <> None then error"An associativity is given more than once."; interp (Some a) level etyps format l - | SetOnlyParsing :: l -> + | SetOnlyParsing _ :: l -> onlyparsing := true; interp assoc level etyps format l | SetFormat s :: l -> @@ -783,8 +783,13 @@ let check_infix_modifiers modifiers = if t <> [] then error "Explicit entry level or type unexpected in infix notation." -let no_syntax_modifiers modifiers = - modifiers = [] or modifiers = [SetOnlyParsing] +let no_syntax_modifiers = function + | [] | [SetOnlyParsing _] -> true + | _ -> false + +let is_only_parsing = function + | [SetOnlyParsing _] -> true + | _ -> false (* Compute precedences from modifiers (or find default ones) *) @@ -1131,7 +1136,7 @@ let add_notation local c ((loc,df),modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) - let onlyparse = modifiers=[SetOnlyParsing] in + let onlyparse = is_only_parsing modifiers in try add_notation_interpretation_core local df c sc onlyparse with NoSyntaxRule -> (* Try to determine a default syntax rule *) @@ -1209,6 +1214,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse = let vars,pat = interp_notation_constr i_vars [] c in List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat in - let onlyparse = onlyparse or is_not_printable pat in + let onlyparse = match onlyparse with + | None when (is_not_printable pat) -> Some Flags.Current + | p -> p + in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index f34b0ccae..22b16be23 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -52,7 +52,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : identifier -> identifier list * constr_expr -> - bool -> bool -> unit + bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index dcf11354b..e1b70b52e 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -32,6 +32,8 @@ let print_usage_channel co command = \n -nois start with an empty state\ \n -outputstate f write state in file f.coq\ \n -compat X.Y provides compatibility support for Coq version X.Y\ +\n -verb-compat-notations be warned when using compatibility notations\ +\n -no-compat-notations get an error when using compatibility notations\ \n\ \n -load-ml-object f load ML object file f\ \n -load-ml-source f load ML file f\ |