diff options
97 files changed, 1148 insertions, 1156 deletions
@@ -111,6 +111,12 @@ Standard Library facts about them, and conversions between decimal numbers and nat, positive, N, Z, and string. +- Some deprecated aliases are now emitting warnings when used. + +Compatibility support + +- Support for compatibility with versions before 8.6 was dropped. + Changes from 8.7.1 to 8.7.2 =========================== diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index bb7a963aa..2ddf927d9 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -36,6 +36,10 @@ let print_idkey idk = print_string ")" | VarKey id -> print_string (Id.to_string id) | RelKey i -> print_string "~";print_int i + | EvarKey evk -> + print_string "Evar("; + print_int (Evar.repr evk); + print_string ")" let rec ppzipper z = match z with diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 95e541f81..a2739e457 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -596,7 +596,6 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq85.v theories/Compat/Coq86.v theories/Compat/Coq87.v </dd> diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 98e507309..abca1307f 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -88,12 +88,11 @@ let pr_compat_warning (kn, def, v) = | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in - let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in - pr_syndef kn ++ pp_def ++ since + pr_syndef kn ++ pp_def let warn_compatibility_notation = CWarnings.(create ~name:"compatibility-notation" - ~category:"deprecated" ~default:Disabled pr_compat_warning) + ~category:"deprecated" ~default:Enabled pr_compat_warning) let verbose_compat kn def = function | Some v when Flags.version_strictly_greater v -> diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 586ef1709..6ed1ba539 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -180,6 +180,7 @@ type fv_elem = | FVnamed of Id.t | FVrel of int | FVuniv_var of int + | FVevar of Evar.t type fv = fv_elem array @@ -194,12 +195,15 @@ type t = fv_elem let compare e1 e2 = match e1, e2 with | FVnamed id1, FVnamed id2 -> Id.compare id1 id2 -| FVnamed _, _ -> -1 +| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 | FVrel _, FVnamed _ -> 1 | FVrel r1, FVrel r2 -> Int.compare r1 r2 -| FVrel _, FVuniv_var _ -> -1 +| FVrel _, (FVuniv_var _ | FVevar _) -> -1 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var i1, _ -> 1 +| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var i1, FVevar _ -> -1 +| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 +| FVevar e1, FVevar e2 -> Evar.compare e1 e2 end @@ -252,6 +256,7 @@ let pp_fv_elem = function | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")" | FVrel i -> str "Rel(" ++ int i ++ str ")" | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")" + | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")" let rec pp_instr i = match i with diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 71dd65186..11e07c00e 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -137,6 +137,7 @@ type fv_elem = FVnamed of Id.t | FVrel of int | FVuniv_var of int +| FVevar of Evar.t type fv = fv_elem array diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0d7619e9f..10f82438c 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -257,6 +257,15 @@ let pos_universe_var i r sz = r.in_env := push_fv db env; Kenvacc(r.offset + pos) +let pos_evar evk r = + let env = !(r.in_env) in + let cid = FVevar evk in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -427,6 +436,7 @@ let compile_fv_elem reloc fv sz cont = | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont | FVuniv_var i -> pos_universe_var i reloc sz :: cont + | FVevar evk -> pos_evar evk reloc :: cont let rec compile_fv reloc l sz cont = match l with @@ -471,6 +481,12 @@ let rec compile_lam env reloc lam sz cont = | Lvar id -> pos_named id reloc :: cont + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem reloc (FVevar evk) sz cont + else + comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont | Lind (ind,u) -> diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 2d9ec6050..c6f63872b 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -20,6 +20,7 @@ type uint = and lambda = | Lrel of Name.t * int | Lvar of Id.t + | Levar of Evar.t * lambda array | Lprod of lambda * lambda | Llam of Name.t array * lambda | Llet of Name.t * lambda * lambda diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 636ed3510..7b637c20e 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -29,6 +29,9 @@ let rec pp_lam lam = match lam with | Lrel (id,n) -> pp_rel id n | Lvar id -> Id.print id + | Levar (evk, args) -> + hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") | Lprod(dom,codom) -> hov 1 (str "forall(" ++ pp_lam dom ++ @@ -148,6 +151,9 @@ let shift subst = subs_shft (1, subst) let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Levar (evk, args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Levar (evk, args') | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -344,6 +350,8 @@ let rec occurrence k kind lam = if kind then false else raise Not_found else kind | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Levar (_, args) -> + occurrence_args k kind args | Lprod(dom, codom) -> occurrence k (occurrence k kind dom) codom | Llam(ids,body) -> @@ -600,7 +608,9 @@ open Renv let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta") - | Evar _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr : Evar") + | Evar (evk, args) -> + let args = lambda_of_args env 0 args in + Levar (evk, args) | Cast (c, _, _) -> lambda_of_constr env c diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 236d83576..a693e62a6 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -150,6 +150,7 @@ and slot_for_fv env fv = env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end + | FVevar evk -> val_of_evar evk | FVuniv_var idu -> assert false diff --git a/kernel/vars.ml b/kernel/vars.ml index b3b3eff62..56d3f11b9 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -310,6 +310,3 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx - -type id_key = Constant.t tableKey -let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index b74d25260..3d3a26e90 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -137,6 +137,3 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t - -type id_key = Constant.t tableKey -val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index ad9aa4267..f11803b67 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -115,7 +115,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> - if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then + if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Asort s1, Asort s2 -> diff --git a/kernel/vm.ml b/kernel/vm.ml index f0bae98dc..a1b0c697c 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -28,7 +28,6 @@ let popstop_code i = let stop = popstop_code 0 - (************************************************) (* Abstract machine *****************************) (************************************************) @@ -70,7 +69,6 @@ let apply_varray vf varray = interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2a784fdf4..a286d2551 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -118,8 +118,21 @@ type vswitch = { (* Do not edit this type without editing C code, especially "coq_values.h" *) +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +let eq_id_key k1 k2 = match k1, k2 with +| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 +| VarKey id1, VarKey id2 -> Id.equal id1 id2 +| RelKey n1, RelKey n2 -> Int.equal n1 n2 +| EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2 +| _ -> false + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive | Asort of Sorts.t @@ -303,13 +316,14 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal + type t = id_key + let equal = eq_id_key open Hashset.Combine let hash = function | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) + | EvarKey evk -> combinesmall 4 (Evar.hash evk) end module KeyTable = Hashtbl.Make(IdKeyHash) @@ -329,6 +343,8 @@ let val_of_named id = val_of_idkey (VarKey id) let val_of_constant c = val_of_idkey (ConstKey c) +let val_of_evar evk = val_of_idkey (EvarKey evk) + external val_of_annot_switch : annot_switch -> values = "%identity" (*************************************************) diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 570e3606a..86debd5d5 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -54,8 +54,16 @@ val fun_code : vfun -> tcode val fix_code : vfix -> tcode val cofix_upd_code : to_update -> tcode +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +val eq_id_key : id_key -> id_key -> bool + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive | Asort of Sorts.t @@ -91,6 +99,7 @@ val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values val val_of_constant : Constant.t -> values +val val_of_evar : Evar.t -> values val val_of_proj : Constant.t -> values -> values val val_of_atom : atom -> values diff --git a/lib/flags.ml b/lib/flags.ml index 5da131020..12ed2a450 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -67,17 +67,11 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current +type compat_version = V8_6 | V8_7 | Current let compat_version = ref Current let version_compare v1 v2 = match v1, v2 with - | VOld, VOld -> 0 - | VOld, _ -> -1 - | _, VOld -> 1 - | V8_5, V8_5 -> 0 - | V8_5, _ -> -1 - | _, V8_5 -> 1 | V8_6, V8_6 -> 0 | V8_6, _ -> -1 | _, V8_6 -> 1 @@ -90,8 +84,6 @@ let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function - | VOld -> "old" - | V8_5 -> "8.5" | V8_6 -> "8.6" | V8_7 -> "8.7" | Current -> "current" diff --git a/lib/flags.mli b/lib/flags.mli index bc07dec80..148b2ca5e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -43,7 +43,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current +type compat_version = V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 52a6fe16c..d7e3751fd 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -384,16 +384,6 @@ let comments = ref [] let current_comment = Buffer.create 8192 let between_commands = ref true -let rec split_comments comacc acc pos = function - [] -> comments := List.rev acc; comacc - | ((b,e),c as com)::coms -> - (* Take all comments that terminates before pos, or begin exactly - at pos (used to print comments attached after an expression) *) - if e<=pos || pos=b then split_comments (c::comacc) acc pos coms - else split_comments comacc (com::acc) pos coms - -let extract_comments pos = split_comments [] [] pos !comments - (* The state of the lexer visible from outside *) type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source @@ -410,6 +400,8 @@ let release_lexer_state = get_lexer_state let drop_lexer_state () = set_lexer_state (init_lexer_state Loc.ToplevelInput) +let get_comment_state (_,_,_,c,_) = c + let real_push_char c = Buffer.add_char current_comment c (* Add a char if it is between two commands, if it is a newline or diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 5f4e10f14..2d35571f1 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -55,7 +55,4 @@ val get_lexer_state : unit -> lexer_state val release_lexer_state : unit -> lexer_state [@@ocaml.deprecated "Use get_lexer_state"] val drop_lexer_state : unit -> unit - -(* Retrieve the comments lexed at a given location of the stream - currently being processeed *) -val extract_comments : int -> string list +val get_comment_state : lexer_state -> ((int * int) * string) list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 93e534e0b..4d6741ff5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -56,9 +56,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function | "8.8" -> Current | "8.7" -> V8_7 | "8.6" -> V8_6 - | "8.5" -> V8_5 - | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> - if allow_old then VOld else + | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") | s -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7a51908d9..fec26f941 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -88,7 +88,9 @@ module type S = val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit - val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b + + val comment_state : coq_parsable -> ((int * int) * string) list + val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a @@ -105,6 +107,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list + type coq_parsable = parsable * CLexer.lexer_state ref let parsable ?(file=Loc.ToplevelInput) c = @@ -129,15 +132,8 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in Loc.raise ~loc e - let with_parsable (p,state) f x = - CLexer.set_lexer_state !state; - try - let a = f x in - state := CLexer.get_lexer_state (); - a - with e -> - CLexer.drop_lexer_state (); - raise e + let comment_state (p,state) = + CLexer.get_comment_state !state let entry_print ft x = Entry.print ft x diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f36250176..1b330aa04 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -78,7 +78,9 @@ module type S = val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit - val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b + + (* Get comment parsing information from the Lexer *) + val comment_state : coq_parsable -> ((int * int) * string) list (* Apparently not used *) val srules' : production_rule list -> symbol diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 1f3a9c124..f77f7c4fa 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -443,14 +443,14 @@ Section Tag. Variables (I : Type) (i : I) (T_ U_ : I -> Type). -Definition tag := projS1. -Definition tagged : forall w, T_(tag w) := @projS2 I [eta T_]. -Definition Tagged x := @existS I [eta T_] i x. +Definition tag := projT1. +Definition tagged : forall w, T_(tag w) := @projT2 I [eta T_]. +Definition Tagged x := @existT I [eta T_] i x. Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 _ _ i _ _ := w in i. Definition tagged2 w : T_(tag2 w) := let: existT2 _ _ _ x _ := w in x. Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ _ _ y := w in y. -Definition Tagged2 x y := @existS2 I [eta T_] [eta U_] i x y. +Definition Tagged2 x y := @existT2 I [eta T_] [eta U_] i x y. End Tag. diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 79d255b0b..4363fc7cc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -923,7 +923,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in - let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + let fsign = if Flags.version_strictly_greater Flags.V8_6 then Context.Rel.map (whd_betaiota !evdref) fsign else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = @@ -1036,7 +1036,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in let cs_args = - if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + if Flags.version_strictly_greater Flags.V8_6 then Context.Rel.map (whd_betaiota !evdref) cs_args else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e1720ec95..6106b6ef6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -193,7 +193,7 @@ let pose_all_metas_as_evars env evd t = let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let ty = - if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + if Flags.version_strictly_greater Flags.V8_6 then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in @@ -1304,12 +1304,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - if Flags.version_less_or_equal Flags.V8_5 then - (* We used to force solving unrelated problems at arbitrary times *) - Evarconv.solve_unif_constraints_with_heuristics env evd - else (* solve_simple_eqn calls reconsider_unif_constraints itself *) - evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 6b7ea2996..eb174936c 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -200,7 +200,26 @@ and nf_univ_args ~nb_univs mk env sigma stk = let (t,ty) = mk u in nf_stk ~from:nb_univs env sigma t ty stk -and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = +and nf_evar env sigma evk stk = + let evi = try Evd.find sigma evk with Not_found -> assert false in + let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in + let concl = Evd.evar_concl evi in + if List.is_empty hyps then + nf_stk env sigma (mkEvar (evk, [||])) concl stk + else match stk with + | Zapp args :: stk -> + (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that + really an invariant? *) + let fold accu d = Term.mkNamedProd_or_LetIn d accu in + let t = List.fold_left fold concl hyps in + let t, args = nf_args env sigma args t in + let inst, args = Array.chop (List.length hyps) args in + let c = mkApp (mkEvar (evk, inst), args) in + nf_stk env sigma c t stk + | _ -> + CErrors.anomaly (Pp.str "Argument size mismatch when decompiling an evar") + +and constr_type_of_idkey env sigma (idkey : Vmvalues.id_key) stk = match idkey with | ConstKey cst -> let cbody = Environ.lookup_constant cst env in @@ -218,6 +237,8 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = let n = (nb_rel env - i) in let ty = RelDecl.get_type (lookup_rel n env) in nf_stk env sigma (mkRel n) (lift n ty) stk + | EvarKey evk -> + nf_evar env sigma evk stk and nf_stk ?from:(from=0) env sigma c t stk = match stk with @@ -355,8 +376,8 @@ and nf_cofix env sigma cf = mkCoFix (init,(name,cft,cfb)) let cbv_vm env sigma c t = - if Termops.occur_meta_or_existential sigma c then - CErrors.user_err Pp.(str "vm_compute does not support existential variables."); + if Termops.occur_meta sigma c then + CErrors.user_err Pp.(str "vm_compute does not support metas."); (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr sigma c in let t = EConstr.to_constr sigma t in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index dedad1990..da1fe6d3d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -149,7 +149,7 @@ let tag_var = tag Tag.variable str "`" ++ str hd ++ c ++ str tl let pr_com_at n = - if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) + if !Flags.beautify && not (Int.equal n 0) then comment (Pputils.extract_comments n) else mt() let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp) diff --git a/printing/pputils.ml b/printing/pputils.ml index e779fc5fc..3d72c8da3 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -13,14 +13,26 @@ open Misctypes open Locus open Genredexpr +let beautify_comments = ref [] + +let rec split_comments comacc acc pos = function + | [] -> beautify_comments := List.rev acc; comacc + | ((b,e),c as com)::coms -> + (* Take all comments that terminates before pos, or begin exactly + at pos (used to print comments attached after an expression) *) + if e<=pos || pos=b then split_comments (c::comacc) acc pos coms + else split_comments comacc (com::acc) pos coms + +let extract_comments pos = split_comments [] [] pos !beautify_comments + let pr_located pr (loc, x) = match loc with | Some loc when !Flags.beautify -> let (b, e) = Loc.unloc loc in (* Side-effect: order matters *) - let before = Pp.comment (CLexer.extract_comments b) in + let before = Pp.comment (extract_comments b) in let x = pr x in - let after = Pp.comment (CLexer.extract_comments e) in + let after = Pp.comment (extract_comments e) in before ++ x ++ after | _ -> pr x diff --git a/printing/pputils.mli b/printing/pputils.mli index ec5c32fc4..483bd0ae3 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -37,3 +37,9 @@ val pr_red_expr_env : Environ.env -> Evd.evar_map -> val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t + +(* The comments interface is imperative due to the printer not + threading it, this could be solved using a better data + structure. *) +val beautify_comments : ((int * int) * string) list ref +val extract_comments : int -> string list diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 467754a84..3386f972e 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -44,8 +44,6 @@ let absurd c = absurd c (* Contradiction *) -let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 - (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function @@ -71,9 +69,7 @@ let contradiction_context = simplest_elim (mkVar id) else match EConstr.kind sigma typ with | Prod (na,t,u) when is_empty_type sigma u -> - let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t - else None in + let is_unit_or_eq = match_with_unit_or_eq_type sigma t in Tacticals.New.tclORELSE (match is_unit_or_eq with | Some _ -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 32563d9ff..96a53a8b1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,7 +84,7 @@ let _ = let injection_in_context = ref false let use_injection_in_context = function - | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5 + | None -> !injection_in_context | Some flags -> flags.injection_in_context let _ = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4b0b11e42..fbbdfe735 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5122,16 +5122,10 @@ module New = struct open Locus let reduce_after_refine = - let onhyps = - (** We reduced everywhere in the hyps before 8.6 *) - if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0 - then None - else Some [] - in reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; rZeta=false;rDelta=false;rConst=[]}) - {onhyps; concl_occs=AllOccurrences } + {onhyps = Some []; concl_occs = AllOccurrences } let refine ~typecheck c = Refine.refine ~typecheck c <*> diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v deleted file mode 100644 index 64a93aeb0..000000000 --- a/test-suite/bugs/closed/2850.v +++ /dev/null @@ -1,2 +0,0 @@ -Definition id {A} (x : A) := x. -Fail Compute id. diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index c3c97d3f5..0d347b262 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -1,5 +1,4 @@ Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. Module A. Import Coq.Lists.List Coq.Vectors.Vector. @@ -21,12 +20,10 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. -Import Coq.Compat.Coq85. Locate Module VectorNotations. Import VectorDef.VectorNotations. @@ -35,11 +32,3 @@ Check []%mylist : mylist _. Check [ ]%mylist : mylist _. Check [ ]%list : list _. End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v deleted file mode 100644 index bbb34f465..000000000 --- a/test-suite/bugs/closed/4785_compat_85.v +++ /dev/null @@ -1,46 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.5") -*- *) -Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. - -Module A. -Import Coq.Lists.List Coq.Vectors.Vector. -Import ListNotations. -Check [ ]%list : list _. -Import VectorNotations ListNotations. -Delimit Scope vector_scope with vector. -Check [ ]%vector : Vector.t _ _. -Check []%vector : Vector.t _ _. -Check [ ]%list : list _. -Fail Check []%list : list _. - -Goal True. - idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) -Abort. - -Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Arguments mynil {_}, _. -Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x nil) : mylist_scope. -Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. - -Import Coq.Compat.Coq85. -Locate Module VectorNotations. -Import VectorDef.VectorNotations. - -Check []%vector : Vector.t _ _. -Check []%mylist : mylist _. -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v index dbc3d46fc..6f2bcb968 100644 --- a/test-suite/bugs/closed/4798.v +++ b/test-suite/bugs/closed/4798.v @@ -1,3 +1,3 @@ Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.4"). +Notation "|" := 1 (compat "8.6"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v index 3be36d847..39299883a 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -1,6 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. -Require Import Coq.Compat.Coq85. Fixpoint tuple' T n : Type := match n with diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index 08918981a..a498db3e8 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -26,6 +26,7 @@ About bar. Print bar. About Peano. (* Module *) +Set Warnings "-deprecated". About existS2. (* Notation *) Arguments eq_refl {A} {x}, {A} x. diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v new file mode 100644 index 000000000..2c8b099ef --- /dev/null +++ b/test-suite/success/vm_evars.v @@ -0,0 +1,23 @@ +Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) := +match n with +| 0 => x +| S n => iter n f (f x) +end. + +Goal nat -> True. +Proof. +intros n. +evar (f : nat -> nat). +cut (iter 10 f 0 = 0). +vm_compute. +intros; constructor. +instantiate (f := (fun x => x)). +reflexivity. +Qed. + +Goal exists x, x = 5 + 5. +Proof. + eexists. + vm_compute. + reflexivity. +Qed. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 1e3237d10..b7235b669 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -133,11 +133,11 @@ Qed. See now [Nat.compare] and its properties. In scope [nat_scope], the notation for [Nat.compare] is "?=" *) -Notation nat_compare := Nat.compare (compat "8.4"). +Notation nat_compare := Nat.compare (compat "8.6"). -Notation nat_compare_spec := Nat.compare_spec (compat "8.4"). -Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4"). -Notation nat_compare_S := Nat.compare_succ (compat "8.4"). +Notation nat_compare_spec := Nat.compare_spec (compat "8.6"). +Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.6"). +Notation nat_compare_S := Nat.compare_succ (only parsing). Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt. Proof. @@ -198,9 +198,9 @@ Qed. See now [Nat.leb] and its properties. In scope [nat_scope], the notation for [Nat.leb] is "<=?" *) -Notation leb := Nat.leb (compat "8.4"). +Notation leb := Nat.leb (only parsing). -Notation leb_iff := Nat.leb_le (compat "8.4"). +Notation leb_iff := Nat.leb_le (only parsing). Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n. Proof. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index ecb9a5706..725d65d82 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -18,7 +18,7 @@ Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Notation div2 := Nat.div2 (compat "8.4"). +Notation div2 := Nat.div2 (only parsing). (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) @@ -84,7 +84,7 @@ Qed. (** Properties related to the double ([2n]) *) -Notation double := Nat.double (compat "8.4"). +Notation double := Nat.double (only parsing). Hint Unfold double Nat.double: arith. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 722615428..a4f2d30bd 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -69,10 +69,10 @@ Defined. We reuse the one already defined in module [Nat]. In scope [nat_scope], the notation "=?" can be used. *) -Notation beq_nat := Nat.eqb (compat "8.4"). +Notation beq_nat := Nat.eqb (only parsing). -Notation beq_nat_true_iff := Nat.eqb_eq (compat "8.4"). -Notation beq_nat_false_iff := Nat.eqb_neq (compat "8.4"). +Notation beq_nat_true_iff := Nat.eqb_eq (only parsing). +Notation beq_nat_false_iff := Nat.eqb_neq (only parsing). Lemma beq_nat_refl n : true = (n =? n). Proof. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index d95b05770..9fcce4520 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -26,17 +26,17 @@ Local Open Scope nat_scope. (** * [le] is an order on [nat] *) -Notation le_refl := Nat.le_refl (compat "8.4"). -Notation le_trans := Nat.le_trans (compat "8.4"). -Notation le_antisym := Nat.le_antisymm (compat "8.4"). +Notation le_refl := Nat.le_refl (only parsing). +Notation le_trans := Nat.le_trans (only parsing). +Notation le_antisym := Nat.le_antisymm (only parsing). Hint Resolve le_trans: arith. Hint Immediate le_antisym: arith. (** * Properties of [le] w.r.t 0 *) -Notation le_0_n := Nat.le_0_l (compat "8.4"). (* 0 <= n *) -Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4"). (* ~ S n <= 0 *) +Notation le_0_n := Nat.le_0_l (only parsing). (* 0 <= n *) +Notation le_Sn_0 := Nat.nle_succ_0 (only parsing). (* ~ S n <= 0 *) Lemma le_n_0_eq n : n <= 0 -> 0 = n. Proof. @@ -53,8 +53,8 @@ Proof Peano.le_n_S. Theorem le_S_n : forall n m, S n <= S m -> n <= m. Proof Peano.le_S_n. -Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *) -Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *) +Notation le_n_Sn := Nat.le_succ_diag_r (only parsing). (* n <= S n *) +Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *) Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof Nat.lt_le_incl. @@ -65,8 +65,8 @@ Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith. (** * Properties of [le] w.r.t predecessor *) -Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *) -Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *) +Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *) +Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *) Hint Resolve le_pred_n: arith. diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 2c2bea4a6..7c3badce1 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -23,7 +23,7 @@ Local Open Scope nat_scope. (** * Irreflexivity *) -Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *) +Notation lt_irrefl := Nat.lt_irrefl (only parsing). (* ~ x < x *) Hint Resolve lt_irrefl: arith. @@ -62,12 +62,12 @@ Hint Immediate le_not_lt lt_not_le: arith. (** * Asymmetry *) -Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *) +Notation lt_asym := Nat.lt_asymm (only parsing). (* n<m -> ~m<n *) (** * Order and 0 *) -Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *) -Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *) +Notation lt_0_Sn := Nat.lt_0_succ (only parsing). (* 0 < S n *) +Notation lt_n_0 := Nat.nlt_0_r (only parsing). (* ~ n < 0 *) Theorem neq_0_lt n : 0 <> n -> 0 < n. Proof. @@ -84,8 +84,8 @@ Hint Immediate neq_0_lt lt_0_neq: arith. (** * Order and successor *) -Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *) -Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *) +Notation lt_n_Sn := Nat.lt_succ_diag_r (only parsing). (* n < S n *) +Notation lt_S := Nat.lt_lt_succ_r (only parsing). (* n < m -> n < S m *) Theorem lt_n_S n m : n < m -> S n < S m. Proof. @@ -127,28 +127,28 @@ Hint Resolve lt_pred_n_n: arith. (** * Transitivity properties *) -Notation lt_trans := Nat.lt_trans (compat "8.4"). -Notation lt_le_trans := Nat.lt_le_trans (compat "8.4"). -Notation le_lt_trans := Nat.le_lt_trans (compat "8.4"). +Notation lt_trans := Nat.lt_trans (only parsing). +Notation lt_le_trans := Nat.lt_le_trans (only parsing). +Notation le_lt_trans := Nat.le_lt_trans (only parsing). Hint Resolve lt_trans lt_le_trans le_lt_trans: arith. (** * Large = strict or equal *) -Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4"). +Notation le_lt_or_eq_iff := Nat.lt_eq_cases (only parsing). Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m. Proof. apply Nat.lt_eq_cases. Qed. -Notation lt_le_weak := Nat.lt_le_incl (compat "8.4"). +Notation lt_le_weak := Nat.lt_le_incl (only parsing). Hint Immediate lt_le_weak: arith. (** * Dichotomy *) -Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *) +Notation le_or_lt := Nat.le_gt_cases (only parsing). (* n <= m \/ m < n *) Theorem nat_total_order n m : n <> m -> n < m \/ m < n. Proof. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 950f985d4..ffa1e048c 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -46,7 +46,7 @@ Qed. (** * Diagonal *) -Notation minus_diag := Nat.sub_diag (compat "8.4"). (* n - n = 0 *) +Notation minus_diag := Nat.sub_diag (only parsing). (* n - n = 0 *) Lemma minus_diag_reverse n : 0 = n - n. Proof. @@ -87,13 +87,13 @@ Qed. (** * Relation with order *) Notation minus_le_compat_r := - Nat.sub_le_mono_r (compat "8.4"). (* n <= m -> n - p <= m - p. *) + Nat.sub_le_mono_r (only parsing). (* n <= m -> n - p <= m - p. *) Notation minus_le_compat_l := - Nat.sub_le_mono_l (compat "8.4"). (* n <= m -> p - m <= p - n. *) + Nat.sub_le_mono_l (only parsing). (* n <= m -> p - m <= p - n. *) -Notation le_minus := Nat.le_sub_l (compat "8.4"). (* n - m <= n *) -Notation lt_minus := Nat.sub_lt (compat "8.4"). (* m <= n -> 0 < m -> n-m < n *) +Notation le_minus := Nat.le_sub_l (only parsing). (* n - m <= n *) +Notation lt_minus := Nat.sub_lt (only parsing). (* m <= n -> 0 < m -> n-m < n *) Lemma lt_O_minus_lt n m : 0 < n - m -> m < n. Proof. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index e4084ba47..4b13e145a 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -23,35 +23,35 @@ Local Open Scope nat_scope. (** ** Zero property *) -Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *) -Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *) +Notation mult_0_l := Nat.mul_0_l (only parsing). (* 0 * n = 0 *) +Notation mult_0_r := Nat.mul_0_r (only parsing). (* n * 0 = 0 *) (** ** 1 is neutral *) -Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *) -Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *) +Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *) +Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *) Hint Resolve mult_1_l mult_1_r: arith. (** ** Commutativity *) -Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *) +Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *) Hint Resolve mult_comm: arith. (** ** Distributivity *) Notation mult_plus_distr_r := - Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *) + Nat.mul_add_distr_r (only parsing). (* (n+m)*p = n*p + m*p *) Notation mult_plus_distr_l := - Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *) + Nat.mul_add_distr_l (only parsing). (* n*(m+p) = n*m + n*p *) Notation mult_minus_distr_r := - Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *) + Nat.mul_sub_distr_r (only parsing). (* (n-m)*p = n*p - m*p *) Notation mult_minus_distr_l := - Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *) + Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *) Hint Resolve mult_plus_distr_r: arith. Hint Resolve mult_minus_distr_r: arith. @@ -59,7 +59,7 @@ Hint Resolve mult_minus_distr_l: arith. (** ** Associativity *) -Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *) +Notation mult_assoc := Nat.mul_assoc (only parsing). (* n*(m*p)=n*m*p *) Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p). Proof. @@ -83,8 +83,8 @@ Qed. (** ** Multiplication and successor *) -Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *) -Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *) +Notation mult_succ_l := Nat.mul_succ_l (only parsing). (* S n * m = n * m + m *) +Notation mult_succ_r := Nat.mul_succ_r (only parsing). (* n * S m = n * m + n *) (** * Compatibility with orders *) diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 247ea20a8..9ed08f1b1 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -19,7 +19,7 @@ Proof. - left; exists n; auto. Defined. -Notation eq_nat_dec := Nat.eq_dec (compat "8.4"). +Notation eq_nat_dec := Nat.eq_dec (only parsing). Hint Resolve O_or_S eq_nat_dec: arith. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 600e5e518..3e44bbfe5 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -27,12 +27,12 @@ Local Open Scope nat_scope. (** * Neutrality of 0, commutativity, associativity *) -Notation plus_0_l := Nat.add_0_l (compat "8.4"). -Notation plus_0_r := Nat.add_0_r (compat "8.4"). -Notation plus_comm := Nat.add_comm (compat "8.4"). -Notation plus_assoc := Nat.add_assoc (compat "8.4"). +Notation plus_0_l := Nat.add_0_l (only parsing). +Notation plus_0_r := Nat.add_0_r (only parsing). +Notation plus_comm := Nat.add_comm (only parsing). +Notation plus_assoc := Nat.add_assoc (only parsing). -Notation plus_permute := Nat.add_shuffle3 (compat "8.4"). +Notation plus_permute := Nat.add_shuffle3 (only parsing). Definition plus_Snm_nSm : forall n m, S n + m = n + S m := Peano.plus_n_Sm. @@ -138,7 +138,7 @@ Defined. (** * Derived properties *) -Notation plus_permute_2_in_4 := Nat.add_shuffle1 (compat "8.4"). +Notation plus_permute_2_in_4 := Nat.add_shuffle1 (only parsing). (** * Tail-recursive plus *) diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v deleted file mode 100644 index 56a9130d1..000000000 --- a/theories/Compat/Coq85.v +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Compatibility file for making Coq act similar to Coq v8.5 *) - -(** Any compatibility changes to make future versions of Coq behave like Coq 8.6 - are likely needed to make them behave like Coq 8.5. *) -Require Export Coq.Compat.Coq86. - -(** We use some deprecated options in this file, so we disable the - corresponding warning, to silence the build of this file. *) -Local Set Warnings "-deprecated-option". - -(* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not - behave as "intros [H|H]" but leave instead hypotheses quantified in - the goal, here producing subgoals A->C and B->C. *) - -Global Unset Bracketing Last Introduction Pattern. -Global Unset Regular Subst Tactic. -Global Unset Structural Injection. -Global Unset Shrink Abstract. -Global Unset Shrink Obligations. -Global Set Refolding Reduction. - -(** The resolution algorithm for type classes has changed. *) -Global Set Typeclasses Legacy Resolution. -Global Set Typeclasses Limit Intros. -Global Unset Typeclasses Filtered Unification. - -(** Allow silently letting unification constraints float after a "." *) -Global Unset Solve Unification Constraints. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 3c5690a72..5ae22c497 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -24,7 +24,7 @@ Hint Extern 1 (Equivalence _) => constructor; congruence. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). -Notation option_map := option_map (compat "8.4"). +Notation option_map := option_map (compat "8.6"). Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -440,7 +440,7 @@ destruct (eq_dec x y); auto. Qed. Lemma map_o : forall m x (f:elt->elt'), - find x (map f m) = option_map f (find x m). + find x (map f m) = Datatypes.option_map f (find x m). Proof. intros. generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x) @@ -473,7 +473,7 @@ Qed. Lemma mapi_o : forall m x (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> - find x (mapi f m) = option_map (f x) (find x m). + find x (mapi f m) = Datatypes.option_map (f x) (find x m). Proof. intros. generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 22e10e2e4..84ec90785 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -359,14 +359,14 @@ Definition idProp : IDProp := fun A x => x. (* Compatibility *) -Notation prodT := prod (compat "8.2"). -Notation pairT := pair (compat "8.2"). -Notation prodT_rect := prod_rect (compat "8.2"). -Notation prodT_rec := prod_rec (compat "8.2"). -Notation prodT_ind := prod_ind (compat "8.2"). -Notation fstT := fst (compat "8.2"). -Notation sndT := snd (compat "8.2"). -Notation prodT_uncurry := prod_uncurry (compat "8.2"). -Notation prodT_curry := prod_curry (compat "8.2"). +Notation prodT := prod (only parsing). +Notation pairT := pair (only parsing). +Notation prodT_rect := prod_rect (only parsing). +Notation prodT_rec := prod_rec (only parsing). +Notation prodT_ind := prod_ind (only parsing). +Notation fstT := fst (only parsing). +Notation sndT := snd (only parsing). +Notation prodT_uncurry := prod_uncurry (only parsing). +Notation prodT_curry := prod_curry (only parsing). (* end hide *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 053ed601f..2209d13ff 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -549,14 +549,14 @@ Qed. (* Aliases *) -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"). +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). Hint Immediate eq_sym not_eq_sym: core. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 567d2c15c..3244fa14c 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -66,7 +66,7 @@ Defined. Hint Immediate identity_sym not_identity_sym: core. -Notation refl_id := identity_refl (compat "8.3"). -Notation sym_id := identity_sym (compat "8.3"). -Notation trans_id := identity_trans (compat "8.3"). -Notation sym_not_id := not_identity_sym (compat "8.3"). +Notation refl_id := identity_refl (only parsing). +Notation sym_id := identity_sym (only parsing). +Notation trans_id := identity_trans (only parsing). +Notation sym_not_id := not_identity_sym (only parsing). diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 571d2f2dd..857913c3e 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -37,7 +37,7 @@ Hint Resolve f_equal_nat: core. (** The predecessor function *) -Notation pred := Nat.pred (compat "8.4"). +Notation pred := Nat.pred (only parsing). Definition f_equal_pred := f_equal pred. @@ -79,7 +79,7 @@ Hint Resolve n_Sn: core. (** Addition *) -Notation plus := Nat.add (compat "8.4"). +Notation plus := Nat.add (only parsing). Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. @@ -110,12 +110,12 @@ Qed. (** Standard associated names *) -Notation plus_0_r_reverse := plus_n_O (compat "8.2"). -Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2"). +Notation plus_0_r_reverse := plus_n_O (only parsing). +Notation plus_succ_r_reverse := plus_n_Sm (only parsing). (** Multiplication *) -Notation mult := Nat.mul (compat "8.4"). +Notation mult := Nat.mul (only parsing). Infix "*" := Nat.mul : nat_scope. Definition f_equal2_mult := f_equal2 mult. @@ -137,12 +137,12 @@ Hint Resolve mult_n_Sm: core. (** Standard associated names *) -Notation mult_0_r_reverse := mult_n_O (compat "8.2"). -Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2"). +Notation mult_0_r_reverse := mult_n_O (only parsing). +Notation mult_succ_r_reverse := mult_n_Sm (only parsing). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) -Notation minus := Nat.sub (compat "8.4"). +Notation minus := Nat.sub (only parsing). Infix "-" := Nat.sub : nat_scope. (** Definition of the usual orders, the basic properties of [le] and [lt] @@ -219,8 +219,8 @@ Qed. (** Maximum and minimum : definitions and specifications *) -Notation max := Nat.max (compat "8.4"). -Notation min := Nat.min (compat "8.4"). +Notation max := Nat.max (only parsing). +Notation min := Nat.min (only parsing). Lemma max_l n m : m <= n -> Nat.max n m = n. Proof. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 47e8a7558..e9d6a1597 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -742,16 +742,16 @@ Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) -Notation sigS := sigT (compat "8.2"). -Notation existS := existT (compat "8.2"). -Notation sigS_rect := sigT_rect (compat "8.2"). -Notation sigS_rec := sigT_rec (compat "8.2"). -Notation sigS_ind := sigT_ind (compat "8.2"). -Notation projS1 := projT1 (compat "8.2"). -Notation projS2 := projT2 (compat "8.2"). - -Notation sigS2 := sigT2 (compat "8.2"). -Notation existS2 := existT2 (compat "8.2"). -Notation sigS2_rect := sigT2_rect (compat "8.2"). -Notation sigS2_rec := sigT2_rec (compat "8.2"). -Notation sigS2_ind := sigT2_ind (compat "8.2"). +Notation sigS := sigT (compat "8.6"). +Notation existS := existT (compat "8.6"). +Notation sigS_rect := sigT_rect (compat "8.6"). +Notation sigS_rec := sigT_rec (compat "8.6"). +Notation sigS_ind := sigT_ind (compat "8.6"). +Notation projS1 := projT1 (compat "8.6"). +Notation projS2 := projT2 (compat "8.6"). + +Notation sigS2 := sigT2 (compat "8.6"). +Notation existS2 := existT2 (compat "8.6"). +Notation sigS2_rect := sigT2_rect (compat "8.6"). +Notation sigS2_rec := sigT2_rec (compat "8.6"). +Notation sigS2_ind := sigT2_ind (compat "8.6"). diff --git a/theories/Lists/List.v b/theories/Lists/List.v index eae2c52de..301528598 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -27,7 +27,6 @@ Module ListNotations. Notation "[ ]" := nil (format "[ ]") : list_scope. Notation "[ x ]" := (cons x nil) : list_scope. Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope. -Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope. End ListNotations. Import ListNotations. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 78ec8ff24..e9b90b52c 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1308,11 +1308,11 @@ Qed. (**********************************************************************) (** * Compatibility notations *) Notation description_rel_choice_imp_funct_choice := - functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + functional_rel_reification_and_rel_choice_imp_fun_choice (only parsing). -Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (only parsing). Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := - fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). + fun_choice_iff_rel_choice_and_functional_rel_reification (only parsing). -Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (only parsing). diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index c9dca432a..af7fcb3fe 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -123,7 +123,7 @@ Proof. apply eq_dep_intro. Qed. -Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.2"). (* Compatibility *) +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.6"). (* Compatibility *) Lemma eq_dep_eq_sigT : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 75a8bfdb3..fcee77b82 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -956,95 +956,94 @@ Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope. (** Compatibility notations *) -(*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 := N.pos (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"). +Notation Ndiscr := N.discr (compat "8.6"). +Notation Ndouble_plus_one := N.succ_double (only parsing). +Notation Ndouble := N.double (compat "8.6"). +Notation Nsucc := N.succ (compat "8.6"). +Notation Npred := N.pred (compat "8.6"). +Notation Nsucc_pos := N.succ_pos (compat "8.6"). +Notation Ppred_N := Pos.pred_N (compat "8.6"). +Notation Nplus := N.add (only parsing). +Notation Nminus := N.sub (only parsing). +Notation Nmult := N.mul (only parsing). +Notation Neqb := N.eqb (compat "8.6"). +Notation Ncompare := N.compare (compat "8.6"). +Notation Nlt := N.lt (compat "8.6"). +Notation Ngt := N.gt (compat "8.6"). +Notation Nle := N.le (compat "8.6"). +Notation Nge := N.ge (compat "8.6"). +Notation Nmin := N.min (compat "8.6"). +Notation Nmax := N.max (compat "8.6"). +Notation Ndiv2 := N.div2 (compat "8.6"). +Notation Neven := N.even (compat "8.6"). +Notation Nodd := N.odd (compat "8.6"). +Notation Npow := N.pow (compat "8.6"). +Notation Nlog2 := N.log2 (compat "8.6"). + +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 (compat "8.6"). +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 (compat "8.6"). +Notation Npred_minus := N.pred_sub (only parsing). +Notation Nsucc_pred := N.succ_pred (compat "8.6"). +Notation Ppred_N_spec := N.pos_pred_spec (only parsing). +Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.6"). +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 (compat "8.6"). +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 (compat "8.6"). +Notation Nle_0 := N.le_0_l (only parsing). +Notation Ncompare_refl := N.compare_refl (compat "8.6"). +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 (compat "8.6"). +Notation Nlt_trans := N.lt_trans (compat "8.6"). +Notation Nle_lteq := N.lt_eq_cases (only parsing). +Notation Nlt_succ_r := N.lt_succ_r (compat "8.6"). +Notation Nle_trans := N.le_trans (compat "8.6"). +Notation Nle_succ_l := N.le_succ_l (compat "8.6"). +Notation Ncompare_spec := N.compare_spec (compat "8.6"). +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 (compat "8.6"). +Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing). +Notation Npow_0_r := N.pow_0_r (compat "8.6"). +Notation Npow_succ_r := N.pow_succ_r (compat "8.6"). +Notation Nlog2_spec := N.log2_spec (compat "8.6"). +Notation Nlog2_nonpos := N.log2_nonpos (compat "8.6"). +Notation Neven_spec := N.even_spec (compat "8.6"). +Notation Nodd_spec := N.odd_spec (compat "8.6"). +Notation Nlt_not_eq := N.lt_neq (only parsing). +Notation Ngt_Nlt := N.gt_lt (only parsing). (** More complex compatibility facts, expressed as lemmas (to preserve scopes for instance) *) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 892bbe7cd..494a80f4a 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -20,11 +20,11 @@ Local Open Scope N_scope. (** Obsolete results about boolean comparisons over [N], kept for compatibility with IntMap and SMC. *) -Notation Peqb := Pos.eqb (compat "8.3"). -Notation Neqb := N.eqb (compat "8.3"). -Notation Peqb_correct := Pos.eqb_refl (compat "8.3"). -Notation Neqb_correct := N.eqb_refl (compat "8.3"). -Notation Neqb_comm := N.eqb_sym (compat "8.3"). +Notation Peqb := Pos.eqb (compat "8.6"). +Notation Neqb := N.eqb (compat "8.6"). +Notation Peqb_correct := Pos.eqb_refl (only parsing). +Notation Neqb_correct := N.eqb_refl (only parsing). +Notation Neqb_comm := N.eqb_sym (only parsing). Lemma Peqb_complete p p' : Pos.eqb p p' = true -> p = p'. Proof. now apply Pos.eqb_eq. Qed. @@ -274,7 +274,7 @@ Qed. (* Old results about [N.min] *) -Notation Nmin_choice := N.min_dec (compat "8.3"). +Notation Nmin_choice := N.min_dec (only parsing). Lemma Nmin_le_1 a b : Nleb (N.min a b) a = true. Proof. rewrite Nleb_Nle. apply N.le_min_l. Qed. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 9aadf985d..835f500a7 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -14,17 +14,17 @@ Local Open Scope N_scope. (** Compatibility names for some bitwise operations *) -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"). +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). (** Equivalence of bit-testing functions, either with index in [N] or in [nat]. *) @@ -249,7 +249,7 @@ Local Close Scope N_scope. (** Checking whether a number is odd, i.e. if its lower bit is set. *) -Notation Nbit0 := N.odd (compat "8.3"). +Notation Nbit0 := N.odd (only parsing). Definition Nodd (n:N) := N.odd n = true. Definition Neven (n:N) := N.odd n = false. @@ -498,7 +498,7 @@ Qed. (** Number of digits in a number *) -Notation Nsize := N.size_nat (compat "8.3"). +Notation Nsize := N.size_nat (only parsing). (** conversions between N and bit vectors. *) diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 974e93994..6e2893a9b 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 (compat "8.3"). -Notation Ndiv := N.div (compat "8.3"). -Notation Nmod := N.modulo (compat "8.3"). +Notation Ndiv_eucl := N.div_eucl (compat "8.6"). +Notation Ndiv := N.div (compat "8.6"). +Notation Nmod := N.modulo (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"). +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 (compat "8.6"). diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 798ab2828..da66a16d6 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -208,30 +208,30 @@ Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) -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"). +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). diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index 97de41c20..61e86eab7 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 (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"). +Notation Nsqrtrem := N.sqrtrem (compat "8.6"). +Notation Nsqrt := N.sqrt (compat "8.6"). +Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.6"). +Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing). +Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.6"). diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 787ef81dc..c75138fbd 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -18,74 +18,74 @@ Module Nat <: NAxiomsSig := Nat. (** Compat notations for stuff that used to be at the beginning of NPeano. *) -Notation leb := Nat.leb (compat "8.4"). -Notation ltb := Nat.ltb (compat "8.4"). -Notation leb_le := Nat.leb_le (compat "8.4"). -Notation ltb_lt := Nat.ltb_lt (compat "8.4"). -Notation pow := Nat.pow (compat "8.4"). -Notation pow_0_r := Nat.pow_0_r (compat "8.4"). -Notation pow_succ_r := Nat.pow_succ_r (compat "8.4"). -Notation square := Nat.square (compat "8.4"). -Notation square_spec := Nat.square_spec (compat "8.4"). -Notation Even := Nat.Even (compat "8.4"). -Notation Odd := Nat.Odd (compat "8.4"). -Notation even := Nat.even (compat "8.4"). -Notation odd := Nat.odd (compat "8.4"). -Notation even_spec := Nat.even_spec (compat "8.4"). -Notation odd_spec := Nat.odd_spec (compat "8.4"). +Notation leb := Nat.leb (only parsing). +Notation ltb := Nat.ltb (only parsing). +Notation leb_le := Nat.leb_le (only parsing). +Notation ltb_lt := Nat.ltb_lt (only parsing). +Notation pow := Nat.pow (only parsing). +Notation pow_0_r := Nat.pow_0_r (only parsing). +Notation pow_succ_r := Nat.pow_succ_r (only parsing). +Notation square := Nat.square (only parsing). +Notation square_spec := Nat.square_spec (only parsing). +Notation Even := Nat.Even (only parsing). +Notation Odd := Nat.Odd (only parsing). +Notation even := Nat.even (only parsing). +Notation odd := Nat.odd (only parsing). +Notation even_spec := Nat.even_spec (only parsing). +Notation odd_spec := Nat.odd_spec (only parsing). Lemma Even_equiv n : Even n <-> Even.even n. Proof. symmetry. apply Even.even_equiv. Qed. Lemma Odd_equiv n : Odd n <-> Even.odd n. Proof. symmetry. apply Even.odd_equiv. Qed. -Notation divmod := Nat.divmod (compat "8.4"). -Notation div := Nat.div (compat "8.4"). -Notation modulo := Nat.modulo (compat "8.4"). -Notation divmod_spec := Nat.divmod_spec (compat "8.4"). -Notation div_mod := Nat.div_mod (compat "8.4"). -Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4"). -Notation sqrt_iter := Nat.sqrt_iter (compat "8.4"). -Notation sqrt := Nat.sqrt (compat "8.4"). -Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4"). -Notation sqrt_spec := Nat.sqrt_spec (compat "8.4"). -Notation log2_iter := Nat.log2_iter (compat "8.4"). -Notation log2 := Nat.log2 (compat "8.4"). -Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4"). -Notation log2_spec := Nat.log2_spec (compat "8.4"). -Notation log2_nonpos := Nat.log2_nonpos (compat "8.4"). -Notation gcd := Nat.gcd (compat "8.4"). -Notation divide := Nat.divide (compat "8.4"). -Notation gcd_divide := Nat.gcd_divide (compat "8.4"). -Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4"). -Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4"). -Notation gcd_greatest := Nat.gcd_greatest (compat "8.4"). -Notation testbit := Nat.testbit (compat "8.4"). -Notation shiftl := Nat.shiftl (compat "8.4"). -Notation shiftr := Nat.shiftr (compat "8.4"). -Notation bitwise := Nat.bitwise (compat "8.4"). -Notation land := Nat.land (compat "8.4"). -Notation lor := Nat.lor (compat "8.4"). -Notation ldiff := Nat.ldiff (compat "8.4"). -Notation lxor := Nat.lxor (compat "8.4"). -Notation double_twice := Nat.double_twice (compat "8.4"). -Notation testbit_0_l := Nat.testbit_0_l (compat "8.4"). -Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4"). -Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4"). -Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4"). -Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4"). -Notation shiftr_spec := Nat.shiftr_spec (compat "8.4"). -Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4"). -Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4"). -Notation div2_bitwise := Nat.div2_bitwise (compat "8.4"). -Notation odd_bitwise := Nat.odd_bitwise (compat "8.4"). -Notation div2_decr := Nat.div2_decr (compat "8.4"). -Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4"). -Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4"). -Notation land_spec := Nat.land_spec (compat "8.4"). -Notation ldiff_spec := Nat.ldiff_spec (compat "8.4"). -Notation lor_spec := Nat.lor_spec (compat "8.4"). -Notation lxor_spec := Nat.lxor_spec (compat "8.4"). +Notation divmod := Nat.divmod (only parsing). +Notation div := Nat.div (only parsing). +Notation modulo := Nat.modulo (only parsing). +Notation divmod_spec := Nat.divmod_spec (only parsing). +Notation div_mod := Nat.div_mod (only parsing). +Notation mod_bound_pos := Nat.mod_bound_pos (only parsing). +Notation sqrt_iter := Nat.sqrt_iter (only parsing). +Notation sqrt := Nat.sqrt (only parsing). +Notation sqrt_iter_spec := Nat.sqrt_iter_spec (only parsing). +Notation sqrt_spec := Nat.sqrt_spec (only parsing). +Notation log2_iter := Nat.log2_iter (only parsing). +Notation log2 := Nat.log2 (only parsing). +Notation log2_iter_spec := Nat.log2_iter_spec (only parsing). +Notation log2_spec := Nat.log2_spec (only parsing). +Notation log2_nonpos := Nat.log2_nonpos (only parsing). +Notation gcd := Nat.gcd (only parsing). +Notation divide := Nat.divide (only parsing). +Notation gcd_divide := Nat.gcd_divide (only parsing). +Notation gcd_divide_l := Nat.gcd_divide_l (only parsing). +Notation gcd_divide_r := Nat.gcd_divide_r (only parsing). +Notation gcd_greatest := Nat.gcd_greatest (only parsing). +Notation testbit := Nat.testbit (only parsing). +Notation shiftl := Nat.shiftl (only parsing). +Notation shiftr := Nat.shiftr (only parsing). +Notation bitwise := Nat.bitwise (only parsing). +Notation land := Nat.land (only parsing). +Notation lor := Nat.lor (only parsing). +Notation ldiff := Nat.ldiff (only parsing). +Notation lxor := Nat.lxor (only parsing). +Notation double_twice := Nat.double_twice (only parsing). +Notation testbit_0_l := Nat.testbit_0_l (only parsing). +Notation testbit_odd_0 := Nat.testbit_odd_0 (only parsing). +Notation testbit_even_0 := Nat.testbit_even_0 (only parsing). +Notation testbit_odd_succ := Nat.testbit_odd_succ (only parsing). +Notation testbit_even_succ := Nat.testbit_even_succ (only parsing). +Notation shiftr_spec := Nat.shiftr_spec (only parsing). +Notation shiftl_spec_high := Nat.shiftl_spec_high (only parsing). +Notation shiftl_spec_low := Nat.shiftl_spec_low (only parsing). +Notation div2_bitwise := Nat.div2_bitwise (only parsing). +Notation odd_bitwise := Nat.odd_bitwise (only parsing). +Notation div2_decr := Nat.div2_decr (only parsing). +Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (only parsing). +Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (only parsing). +Notation land_spec := Nat.land_spec (only parsing). +Notation ldiff_spec := Nat.ldiff_spec (only parsing). +Notation lor_spec := Nat.lor_spec (only parsing). +Notation lxor_spec := Nat.lxor_spec (only parsing). Infix "<=?" := Nat.leb (at level 70) : nat_scope. Infix "<?" := Nat.ltb (at level 70) : nat_scope. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index ff880eefa..3adc72e14 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1903,180 +1903,180 @@ Notation IsNul := Pos.IsNul (only parsing). Notation IsPos := Pos.IsPos (only parsing). Notation IsNeg := Pos.IsNeg (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 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 x y m := (Pos.compare_cont m x y) (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 := Pos.succ (compat "8.6"). +Notation Pplus := Pos.add (only parsing). +Notation Pplus_carry := Pos.add_carry (only parsing). +Notation Ppred := Pos.pred (compat "8.6"). +Notation Piter_op := Pos.iter_op (compat "8.6"). +Notation Piter_op_succ := Pos.iter_op_succ (compat "8.6"). +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 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 (compat "8.6"). +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 (compat "8.6"). +Notation Pdiv2 := Pos.div2 (compat "8.6"). +Notation Pdiv2_up := Pos.div2_up (compat "8.6"). +Notation Psize := Pos.size_nat (only parsing). +Notation Psize_pos := Pos.size (only parsing). +Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing). +Notation Plt := Pos.lt (compat "8.6"). +Notation Pgt := Pos.gt (compat "8.6"). +Notation Ple := Pos.le (compat "8.6"). +Notation Pge := Pos.ge (compat "8.6"). +Notation Pmin := Pos.min (compat "8.6"). +Notation Pmax := Pos.max (compat "8.6"). +Notation Peqb := Pos.eqb (compat "8.6"). +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 (compat "8.6"). Notation Psucc_o_double_minus_one_eq_xO := - Pos.succ_pred_double (compat "8.3"). + Pos.succ_pred_double (only parsing). Notation Pdouble_minus_one_o_succ_eq_xI := - Pos.pred_double_succ (compat "8.3"). -Notation xO_succ_permute := Pos.double_succ (compat "8.3"). + Pos.pred_double_succ (only parsing). +Notation xO_succ_permute := Pos.double_succ (only parsing). Notation double_moins_un_xO_discr := - 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"). + Pos.pred_double_xO_discr (only parsing). +Notation Psucc_not_one := Pos.succ_not_1 (only parsing). +Notation Ppred_succ := Pos.pred_succ (compat "8.6"). +Notation Psucc_pred := Pos.succ_pred_or (only parsing). +Notation Psucc_inj := Pos.succ_inj (compat "8.6"). +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 (compat "8.6"). +Notation Psquare_xI := Pos.square_xI (compat "8.6"). +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 (compat "8.6"). +Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.6"). +Notation Peqb_refl := Pos.eqb_refl (compat "8.6"). +Notation Peqb_eq := Pos.eqb_eq (compat "8.6"). +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 (compat "8.6"). +Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing). +Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.6"). +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 (compat "8.6"). +Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.6"). +Notation Plt_irrefl := Pos.lt_irrefl (compat "8.6"). +Notation Plt_trans := Pos.lt_trans (compat "8.6"). +Notation Plt_ind := Pos.lt_ind (compat "8.6"). +Notation Ple_lteq := Pos.le_lteq (compat "8.6"). +Notation Ple_refl := Pos.le_refl (compat "8.6"). +Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.6"). +Notation Plt_le_trans := Pos.lt_le_trans (compat "8.6"). +Notation Ple_trans := Pos.le_trans (compat "8.6"). +Notation Plt_succ_r := Pos.lt_succ_r (compat "8.6"). +Notation Ple_succ_l := Pos.le_succ_l (compat "8.6"). +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 (compat "8.6"). +Notation Ppred_mask := Pos.pred_mask (compat "8.6"). +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). (** 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 461967de8..6cbea8a3d 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -382,36 +382,36 @@ End SuccNat2Pos. (** For compatibility, old names and old-style lemmas *) -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"). +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). Lemma nat_of_P_minus_morphism p q : Pos.compare_cont Eq p q = Gt -> diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 5d055b547..959a7e5bd 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -11,8 +11,8 @@ Require Export QArith_base. Require Import Znumtheory. -Notation Z2P := Z.to_pos (compat "8.3"). -Notation Z2P_correct := Z2Pos.id (compat "8.3"). +Notation Z2P := Z.to_pos (only parsing). +Notation Z2P_correct := Z2Pos.id (only parsing). (** Simplification of fractions using [Z.gcd]. This version can compute within Coq. *) diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index bc82c3712..ab7fa15d2 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -2027,7 +2027,7 @@ Qed. Lemma R_rm : ring_morph 0%R 1%R Rplus Rmult Rminus Ropp eq - 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR. + 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR. Proof. constructor ; try easy. exact plus_IZR. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 17b3c5099..a50c7f952 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -609,7 +609,7 @@ Qed. Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z). Proof. - intros z; case z; unfold Zabs. + intros z; case z; unfold Z.abs. apply Rabs_R0. now intros p0; apply Rabs_pos_eq, (IZR_le 0). unfold IZR at 1. diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 4ad3339ec..c1b479b61 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -63,7 +63,7 @@ destruct (Rle_lt_dec l 0) as [Hl|Hl]. now apply Rinv_0_lt_compat. now apply Hnp. left. -set (N := Zabs_nat (up (/l) - 2)). +set (N := Z.abs_nat (up (/l) - 2)). assert (H1l: (1 <= /l)%R). rewrite <- Rinv_1. apply Rinv_le_contravar with (1 := Hl). @@ -75,7 +75,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). rewrite inj_Zabs_nat. replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R. apply (f_equal (fun v => IZR v + 1)%R). - apply Zabs_eq. + apply Z.abs_eq. apply Zle_minus_le_0. apply (Zlt_le_succ 1). apply lt_IZR. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 3c6afc7b2..9b004a6da 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -55,7 +55,7 @@ Module Nat_as_OT <: UsualOrderedType. Definition compare x y : Compare lt eq x y. Proof. - case_eq (nat_compare x y); intro. + case_eq (Nat.compare x y); intro. - apply EQ. now apply nat_compare_eq. - apply LT. now apply nat_compare_Lt_lt. - apply GT. now apply nat_compare_Gt_gt. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index c49451776..a21b9ca98 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -305,12 +305,10 @@ End VECTORLIST. Module VectorNotations. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. -Notation "[]" := [] (compat "8.5") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) : vector_scope. Notation "[ x ]" := (x :: []) : vector_scope. Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope. -Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope. Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. Open Scope vector_scope. End VectorNotations. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index e6fd0f22e..e7dd8aebb 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1565,94 +1565,94 @@ End Z2Pos. (** Compatibility Notations *) -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_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 := Pos2Z.inj_xI (compat "8.3"). -Notation Zpos_xO := Pos2Z.inj_xO (compat "8.3"). -Notation Zneg_xI := Pos2Z.neg_xI (compat "8.3"). -Notation Zneg_xO := Pos2Z.neg_xO (compat "8.3"). -Notation Zopp_neg := Pos2Z.opp_neg (compat "8.3"). -Notation Zpos_succ_morphism := Pos2Z.inj_succ (compat "8.3"). -Notation Zpos_mult_morphism := Pos2Z.inj_mul (compat "8.3"). -Notation Zpos_minus_morphism := Pos2Z.inj_sub (compat "8.3"). -Notation Zpos_eq_rev := Pos2Z.inj (compat "8.3"). -Notation Zpos_plus_distr := Pos2Z.inj_add (compat "8.3"). -Notation Zneg_plus_distr := Pos2Z.add_neg_neg (compat "8.3"). +Notation Zdouble_plus_one := Z.succ_double (only parsing). +Notation Zdouble_minus_one := Z.pred_double (only parsing). +Notation Zdouble := Z.double (compat "8.6"). +Notation ZPminus := Z.pos_sub (only parsing). +Notation Zsucc' := Z.succ (compat "8.6"). +Notation Zpred' := Z.pred (compat "8.6"). +Notation Zplus' := Z.add (compat "8.6"). +Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) +Notation Zopp := Z.opp (compat "8.6"). +Notation Zsucc := Z.succ (compat "8.6"). +Notation Zpred := Z.pred (compat "8.6"). +Notation Zminus := Z.sub (only parsing). +Notation Zmult := Z.mul (only parsing). +Notation Zcompare := Z.compare (compat "8.6"). +Notation Zsgn := Z.sgn (compat "8.6"). +Notation Zle := Z.le (compat "8.6"). +Notation Zge := Z.ge (compat "8.6"). +Notation Zlt := Z.lt (compat "8.6"). +Notation Zgt := Z.gt (compat "8.6"). +Notation Zmax := Z.max (compat "8.6"). +Notation Zmin := Z.min (compat "8.6"). +Notation Zabs := Z.abs (compat "8.6"). +Notation Zabs_nat := Z.abs_nat (compat "8.6"). +Notation Zabs_N := Z.abs_N (compat "8.6"). +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 (compat "8.6"). +Notation Zopp_involutive := Z.opp_involutive (compat "8.6"). +Notation Zopp_inj := Z.opp_inj (compat "8.6"). +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 (compat "8.6"). +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 (compat "8.6"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.6"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.6"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.6"). +Notation Zpred'_inj := Z.pred_inj (compat "8.6"). +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 := Pos2Z.inj_xI (only parsing). +Notation Zpos_xO := Pos2Z.inj_xO (only parsing). +Notation Zneg_xI := Pos2Z.neg_xI (only parsing). +Notation Zneg_xO := Pos2Z.neg_xO (only parsing). +Notation Zopp_neg := Pos2Z.opp_neg (only parsing). +Notation Zpos_succ_morphism := Pos2Z.inj_succ (only parsing). +Notation Zpos_mult_morphism := Pos2Z.inj_mul (only parsing). +Notation Zpos_minus_morphism := Pos2Z.inj_sub (only parsing). +Notation Zpos_eq_rev := Pos2Z.inj (only parsing). +Notation Zpos_plus_distr := Pos2Z.inj_add (only parsing). +Notation Zneg_plus_distr := Pos2Z.add_neg_neg (only parsing). Notation Z := Z (only parsing). Notation Z_rect := Z_rect (only parsing). diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 72021f2e4..696016e5b 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -452,7 +452,7 @@ Module Z_as_Int <: Int. Proof. reflexivity. Qed. (** Compatibility notations for Coq v8.4 *) - Notation plus := add (compat "8.4"). - Notation minus := sub (compat "8.4"). - Notation mult := mul (compat "8.4"). + Notation plus := add (only parsing). + Notation minus := sub (only parsing). + Notation mult := mul (only parsing). End Z_as_Int. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 0ee233a35..e1a943e56 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -32,7 +32,7 @@ Lemma Zcompare_rec (P:Set) (n m:Z) : ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. Proof. apply Zcompare_rect. Defined. -Notation Z_eq_dec := Z.eq_dec (compat "8.3"). +Notation Z_eq_dec := Z.eq_dec (compat "8.6"). Section decidability. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index d4a46930a..440a55823 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 (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"). +Notation Zabs_eq := Z.abs_eq (compat "8.6"). +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 (compat "8.6"). +Notation Zabs_eq_case := Z.abs_eq_cases (only parsing). +Notation Zabs_triangle := Z.abs_triangle (compat "8.6"). +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 (compat "8.6"). (** * 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 (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"). +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). (** A characterization of the sign function: *) @@ -86,13 +86,13 @@ Qed. (** Compatibility *) -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"). +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). 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 407aef3b6..eeb6c18a7 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 (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"). +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). (** 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 (compat "8.3"). +Notation Zle_bool_refl := Z.leb_refl (only parsing). 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 f823c41a2..69e3e9a6a 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -181,18 +181,18 @@ Qed. (** Compatibility notations *) -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"). +Notation Zcompare_refl := Z.compare_refl (compat "8.6"). +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 (compat "8.6"). +Notation Zmin_l := Z.min_l (compat "8.6"). +Notation Zmin_r := Z.min_r (compat "8.6"). +Notation Zmax_l := Z.max_l (compat "8.6"). +Notation Zmax_r := Z.max_r (compat "8.6"). +Notation Zabs_eq := Z.abs_eq (compat "8.6"). +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). (** Not kept: Zcompare_egal_dec *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index fa1ddf56f..8c4c9d301 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 (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"). +Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing). +Notation Zdiv_eucl := Z.div_eucl (compat "8.6"). +Notation Zdiv := Z.div (compat "8.6"). +Notation Zmod := Z.modulo (only parsing). + +Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.6"). +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). (** * Main division theorems *) diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 42a6a8ee3..44b4a0083 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 (compat "8.3"). -Notation Zodd_bool := Z.odd (compat "8.3"). +Notation Zeven_bool := Z.even (only parsing). +Notation Zodd_bool := Z.odd (only parsing). 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 (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"). +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). (******************************************************************) (** * Definition of [Z.quot2], [Z.div2] and properties wrt [Zeven] and [Zodd] *) -Notation Zdiv2 := Z.div2 (compat "8.3"). -Notation Zquot2 := Z.quot2 (compat "8.3"). +Notation Zdiv2 := Z.div2 (compat "8.6"). +Notation Zquot2 := Z.quot2 (compat "8.6"). (** Properties of [Z.div2] *) diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index b52da8563..36d8451f8 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -16,32 +16,32 @@ Local Open Scope Z_scope. (** Exact compatibility *) -Notation Zmax_case := Z.max_case (compat "8.3"). -Notation Zmax_case_strong := Z.max_case_strong (compat "8.3"). -Notation Zmax_right := Z.max_r (compat "8.3"). -Notation Zle_max_l := Z.le_max_l (compat "8.3"). -Notation Zle_max_r := Z.le_max_r (compat "8.3"). -Notation Zmax_lub := Z.max_lub (compat "8.3"). -Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.3"). -Notation Zle_max_compat_r := Z.max_le_compat_r (compat "8.3"). -Notation Zle_max_compat_l := Z.max_le_compat_l (compat "8.3"). -Notation Zmax_idempotent := Z.max_id (compat "8.3"). -Notation Zmax_n_n := Z.max_id (compat "8.3"). -Notation Zmax_comm := Z.max_comm (compat "8.3"). -Notation Zmax_assoc := Z.max_assoc (compat "8.3"). -Notation Zmax_irreducible_dec := Z.max_dec (compat "8.3"). -Notation Zmax_le_prime := Z.max_le (compat "8.3"). -Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.3"). -Notation Zmax_SS := Z.succ_max_distr (compat "8.3"). -Notation Zplus_max_distr_l := Z.add_max_distr_l (compat "8.3"). -Notation Zplus_max_distr_r := Z.add_max_distr_r (compat "8.3"). -Notation Zmax_plus := Z.add_max_distr_r (compat "8.3"). -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"). -Notation Zpos_max := Pos2Z.inj_max (compat "8.3"). -Notation Zpos_minus := Pos2Z.inj_sub_max (compat "8.3"). +Notation Zmax_case := Z.max_case (compat "8.6"). +Notation Zmax_case_strong := Z.max_case_strong (compat "8.6"). +Notation Zmax_right := Z.max_r (only parsing). +Notation Zle_max_l := Z.le_max_l (compat "8.6"). +Notation Zle_max_r := Z.le_max_r (compat "8.6"). +Notation Zmax_lub := Z.max_lub (compat "8.6"). +Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.6"). +Notation Zle_max_compat_r := Z.max_le_compat_r (only parsing). +Notation Zle_max_compat_l := Z.max_le_compat_l (only parsing). +Notation Zmax_idempotent := Z.max_id (only parsing). +Notation Zmax_n_n := Z.max_id (only parsing). +Notation Zmax_comm := Z.max_comm (compat "8.6"). +Notation Zmax_assoc := Z.max_assoc (compat "8.6"). +Notation Zmax_irreducible_dec := Z.max_dec (only parsing). +Notation Zmax_le_prime := Z.max_le (only parsing). +Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.6"). +Notation Zmax_SS := Z.succ_max_distr (only parsing). +Notation Zplus_max_distr_l := Z.add_max_distr_l (only parsing). +Notation Zplus_max_distr_r := Z.add_max_distr_r (only parsing). +Notation Zmax_plus := Z.add_max_distr_r (only parsing). +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 Zpos_max := Pos2Z.inj_max (only parsing). +Notation Zpos_minus := Pos2Z.inj_sub_max (only parsing). (** Slightly different lemmas *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index d9e3ab19e..dd9203f33 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -16,24 +16,24 @@ Local Open Scope Z_scope. (** Exact compatibility *) -Notation Zmin_case := Z.min_case (compat "8.3"). -Notation Zmin_case_strong := Z.min_case_strong (compat "8.3"). -Notation Zle_min_l := Z.le_min_l (compat "8.3"). -Notation Zle_min_r := Z.le_min_r (compat "8.3"). -Notation Zmin_glb := Z.min_glb (compat "8.3"). -Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.3"). -Notation Zle_min_compat_r := Z.min_le_compat_r (compat "8.3"). -Notation Zle_min_compat_l := Z.min_le_compat_l (compat "8.3"). -Notation Zmin_idempotent := Z.min_id (compat "8.3"). -Notation Zmin_n_n := Z.min_id (compat "8.3"). -Notation Zmin_comm := Z.min_comm (compat "8.3"). -Notation Zmin_assoc := Z.min_assoc (compat "8.3"). -Notation Zmin_irreducible_inf := Z.min_dec (compat "8.3"). -Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.3"). -Notation Zmin_SS := Z.succ_min_distr (compat "8.3"). -Notation Zplus_min_distr_r := Z.add_min_distr_r (compat "8.3"). -Notation Zmin_plus := Z.add_min_distr_r (compat "8.3"). -Notation Zpos_min := Pos2Z.inj_min (compat "8.3"). +Notation Zmin_case := Z.min_case (compat "8.6"). +Notation Zmin_case_strong := Z.min_case_strong (compat "8.6"). +Notation Zle_min_l := Z.le_min_l (compat "8.6"). +Notation Zle_min_r := Z.le_min_r (compat "8.6"). +Notation Zmin_glb := Z.min_glb (compat "8.6"). +Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.6"). +Notation Zle_min_compat_r := Z.min_le_compat_r (only parsing). +Notation Zle_min_compat_l := Z.min_le_compat_l (only parsing). +Notation Zmin_idempotent := Z.min_id (only parsing). +Notation Zmin_n_n := Z.min_id (only parsing). +Notation Zmin_comm := Z.min_comm (compat "8.6"). +Notation Zmin_assoc := Z.min_assoc (compat "8.6"). +Notation Zmin_irreducible_inf := Z.min_dec (only parsing). +Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.6"). +Notation Zmin_SS := Z.succ_min_distr (only parsing). +Notation Zplus_min_distr_r := Z.add_min_distr_r (only parsing). +Notation Zmin_plus := Z.add_min_distr_r (only parsing). +Notation Zpos_min := Pos2Z.inj_min (only parsing). (** Slightly different lemmas *) @@ -46,7 +46,7 @@ Qed. Lemma Zmin_irreducible n m : Z.min n m = n \/ Z.min n m = m. Proof. destruct (Z.min_dec n m); auto. Qed. -Notation Zmin_or := Zmin_irreducible (compat "8.3"). +Notation Zmin_or := Zmin_irreducible (only parsing). Lemma Zmin_le_prime_inf n m p : Z.min n m <= p -> {n <= p} + {m <= p}. Proof. apply Z.min_case; auto. Qed. diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index 7e62d6689..4a149f2f2 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 (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"). +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). (*end hide*) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index a6f29936b..651cda00b 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -18,7 +18,7 @@ Local Open Scope Z_scope. (** [n]th iteration of the function [f] *) -Notation iter := @Z.iter (compat "8.3"). +Notation iter := @Z.iter (only parsing). Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> Z.iter n f x = iter_nat (Z.abs_nat n) A f x. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index be712db6b..402dfe33a 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -951,65 +951,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 (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 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 Zpos_eq_Z_of_nat_o_nat_of_P := - (fun p => eq_sym (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"). + (fun p => eq_sym (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). 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 5dfc37095..521d6789e 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 (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"). +Notation Zgcd := Z.gcd (compat "8.6"). +Notation Zggcd := Z.ggcd (compat "8.6"). +Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.6"). +Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.6"). +Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.6"). +Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.6"). +Notation Zgcd_greatest := Z.gcd_greatest (compat "8.6"). +Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.6"). +Notation Zggcd_opp := Z.ggcd_opp (compat "8.6"). (** The former specialized inductive predicate [Z.divide] is now a generic existential predicate. *) -Notation Zdivide := Z.divide (compat "8.3"). +Notation Zdivide := Z.divide (compat "8.6"). (** 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 (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"). +Notation Zdivide_refl := Z.divide_refl (compat "8.6"). +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). 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 (compat "8.3"). +Notation Zdivide_1 := Z.divide_1_r (only parsing). (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) -Notation Zdivide_antisym := Z.divide_antisym (compat "8.3"). -Notation Zdivide_trans := Z.divide_trans (compat "8.3"). +Notation Zdivide_antisym := Z.divide_antisym (compat "8.6"). +Notation Zdivide_trans := Z.divide_trans (compat "8.6"). (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) @@ -734,7 +734,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 (compat "8.3"). +Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing). Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b). Proof. @@ -767,8 +767,8 @@ Proof. - subst. now case (Z.gcd a b). Qed. -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"). +Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing). +Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing). Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Z.gcd a b -> @@ -798,16 +798,16 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Notation Zgcd_comm := Z.gcd_comm (compat "8.3"). +Notation Zgcd_comm := Z.gcd_comm (compat "8.6"). Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c). Proof. symmetry. apply Z.gcd_assoc. Qed. -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"). +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). Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index ff8e22029..d188681fe 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 (compat "8.3"). -Notation dec_Zle := Z.le_decidable (compat "8.3"). -Notation dec_Zlt := Z.lt_decidable (compat "8.3"). +Notation dec_eq := Z.eq_decidable (only parsing). +Notation dec_Zle := Z.le_decidable (only parsing). +Notation dec_Zlt := Z.lt_decidable (only parsing). 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 (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"). +Notation Zgt_lt := Z.gt_lt (compat "8.6"). +Notation Zlt_gt := Z.lt_gt (compat "8.6"). +Notation Zge_le := Z.ge_le (compat "8.6"). +Notation Zle_ge := Z.le_ge (compat "8.6"). +Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). +Notation Zge_iff_le := Z.ge_le_iff (only parsing). Lemma Zle_not_lt n m : n <= m -> ~ m < n. Proof. @@ -121,18 +121,18 @@ Qed. (** Reflexivity *) -Notation Zle_refl := Z.le_refl (compat "8.3"). -Notation Zeq_le := Z.eq_le_incl (compat "8.3"). +Notation Zle_refl := Z.le_refl (compat "8.6"). +Notation Zeq_le := Z.eq_le_incl (only parsing). Hint Resolve Z.le_refl: zarith. (** Antisymmetry *) -Notation Zle_antisym := Z.le_antisymm (compat "8.3"). +Notation Zle_antisym := Z.le_antisymm (only parsing). (** Asymmetry *) -Notation Zlt_asym := Z.lt_asymm (compat "8.3"). +Notation Zlt_asym := Z.lt_asymm (only parsing). Lemma Zgt_asym n m : n > m -> ~ m > n. Proof. @@ -141,8 +141,8 @@ Qed. (** Irreflexivity *) -Notation Zlt_irrefl := Z.lt_irrefl (compat "8.3"). -Notation Zlt_not_eq := Z.lt_neq (compat "8.3"). +Notation Zlt_irrefl := Z.lt_irrefl (compat "8.6"). +Notation Zlt_not_eq := Z.lt_neq (only parsing). Lemma Zgt_irrefl n : ~ n > n. Proof. @@ -151,8 +151,8 @@ Qed. (** Large = strict or equal *) -Notation Zlt_le_weak := Z.lt_le_incl (compat "8.3"). -Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (compat "8.3"). +Notation Zlt_le_weak := Z.lt_le_incl (only parsing). +Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing). Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m. Proof. @@ -161,11 +161,11 @@ Qed. (** Dichotomy *) -Notation Zle_or_lt := Z.le_gt_cases (compat "8.3"). +Notation Zle_or_lt := Z.le_gt_cases (only parsing). (** Transitivity of strict orders *) -Notation Zlt_trans := Z.lt_trans (compat "8.3"). +Notation Zlt_trans := Z.lt_trans (compat "8.6"). Lemma Zgt_trans n m p : n > m -> m > p -> n > p. Proof. @@ -174,8 +174,8 @@ Qed. (** Mixed transitivity *) -Notation Zlt_le_trans := Z.lt_le_trans (compat "8.3"). -Notation Zle_lt_trans := Z.le_lt_trans (compat "8.3"). +Notation Zlt_le_trans := Z.lt_le_trans (compat "8.6"). +Notation Zle_lt_trans := Z.le_lt_trans (compat "8.6"). Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p. Proof. @@ -189,7 +189,7 @@ Qed. (** Transitivity of large orders *) -Notation Zle_trans := Z.le_trans (compat "8.3"). +Notation Zle_trans := Z.le_trans (compat "8.6"). Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p. Proof. @@ -240,8 +240,8 @@ Qed. (** Special base instances of order *) -Notation Zlt_succ := Z.lt_succ_diag_r (compat "8.3"). -Notation Zlt_pred := Z.lt_pred_l (compat "8.3"). +Notation Zlt_succ := Z.lt_succ_diag_r (only parsing). +Notation Zlt_pred := Z.lt_pred_l (only parsing). Lemma Zgt_succ n : Z.succ n > n. Proof. @@ -255,8 +255,8 @@ Qed. (** Relating strict and large order using successor or predecessor *) -Notation Zlt_succ_r := Z.lt_succ_r (compat "8.3"). -Notation Zle_succ_l := Z.le_succ_l (compat "8.3"). +Notation Zlt_succ_r := Z.lt_succ_r (compat "8.6"). +Notation Zle_succ_l := Z.le_succ_l (compat "8.6"). Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m. Proof. @@ -295,10 +295,10 @@ Qed. (** Weakening order *) -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"). +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). Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m. Proof. @@ -334,8 +334,8 @@ Qed. (** Special cases of ordered integers *) -Notation Zlt_0_1 := Z.lt_0_1 (compat "8.3"). -Notation Zle_0_1 := Z.le_0_1 (compat "8.3"). +Notation Zlt_0_1 := Z.lt_0_1 (compat "8.6"). +Notation Zle_0_1 := Z.le_0_1 (compat "8.6"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. @@ -375,10 +375,10 @@ Qed. (** ** Addition *) (** Compatibility of addition wrt to order *) -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"). +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). Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m. Proof. @@ -412,7 +412,7 @@ Qed. (** Compatibility of addition wrt to being positive *) -Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (compat "8.3"). +Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing). (** Simplification of addition wrt to order *) @@ -570,9 +570,9 @@ Qed. (** Compatibility of multiplication by a positive wrt to being positive *) -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"). +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). Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0. Proof. @@ -624,9 +624,9 @@ Qed. (** * Equivalence between inequalities *) -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"). +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). 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 a768868bd..a3a3b9727 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 (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 := Pos2Z.inj_pow (compat "8.3"). +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 := Pos2Z.inj_pow (only parsing). 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 3ea3ae4ab..e0d62b99c 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 (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"). +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). Theorem Zpower_le_monotone a b c : 0 < a -> 0 <= b <= c -> a^b <= a^c. @@ -231,7 +231,7 @@ Qed. (** * Z.square: a direct definition of [z^2] *) -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"). +Notation Psquare := Pos.square (compat "8.6"). +Notation Zsquare := Z.square (compat "8.6"). +Notation Psquare_correct := Pos.square_spec (only parsing). +Notation Zsquare_correct := Z.square_spec (only parsing). diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index efb56c469..808a32ea2 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -31,21 +31,21 @@ Local Open Scope Z_scope. exploiting the arbitrary value of division by 0). *) -Notation Ndiv_Zquot := N2Z.inj_quot (compat "8.3"). -Notation Nmod_Zrem := N2Z.inj_rem (compat "8.3"). -Notation Z_quot_rem_eq := Z.quot_rem' (compat "8.3"). -Notation Zrem_lt := Z.rem_bound_abs (compat "8.3"). -Notation Zquot_unique := Z.quot_unique (compat "8.3"). -Notation Zrem_unique := Z.rem_unique (compat "8.3"). -Notation Zrem_1_r := Z.rem_1_r (compat "8.3"). -Notation Zquot_1_r := Z.quot_1_r (compat "8.3"). -Notation Zrem_1_l := Z.rem_1_l (compat "8.3"). -Notation Zquot_1_l := Z.quot_1_l (compat "8.3"). -Notation Z_quot_same := Z.quot_same (compat "8.3"). -Notation Z_quot_mult := Z.quot_mul (compat "8.3"). -Notation Zquot_small := Z.quot_small (compat "8.3"). -Notation Zrem_small := Z.rem_small (compat "8.3"). -Notation Zquot2_quot := Zquot2_quot (compat "8.3"). +Notation Ndiv_Zquot := N2Z.inj_quot (only parsing). +Notation Nmod_Zrem := N2Z.inj_rem (only parsing). +Notation Z_quot_rem_eq := Z.quot_rem' (only parsing). +Notation Zrem_lt := Z.rem_bound_abs (only parsing). +Notation Zquot_unique := Z.quot_unique (compat "8.6"). +Notation Zrem_unique := Z.rem_unique (compat "8.6"). +Notation Zrem_1_r := Z.rem_1_r (compat "8.6"). +Notation Zquot_1_r := Z.quot_1_r (compat "8.6"). +Notation Zrem_1_l := Z.rem_1_l (compat "8.6"). +Notation Zquot_1_l := Z.quot_1_l (compat "8.6"). +Notation Z_quot_same := Z.quot_same (compat "8.6"). +Notation Z_quot_mult := Z.quot_mul (only parsing). +Notation Zquot_small := Z.quot_small (compat "8.6"). +Notation Zrem_small := Z.rem_small (compat "8.6"). +Notation Zquot2_quot := Zquot2_quot (compat "8.6"). (** Particular values taken for [a÷0] and [(Z.rem a 0)]. We avise to not rely on these arbitrary values. *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index a7065c031..673cfdb99 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -146,10 +146,9 @@ let add_vo_require opts d p export = let add_compat_require opts v = match v with - | Flags.V8_5 -> add_vo_require opts "Coq.Compat.Coq85" None (Some false) | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false) | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false) - | Flags.VOld | Flags.Current -> opts + | Flags.Current -> opts let set_batch_mode opts = Flags.quiet := true; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index d8aaf3db8..6f461fd53 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -26,7 +26,7 @@ let load_rcfile ~rcfile ~time ~state = match rcfile with | Some rcfile -> if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile + Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) | None -> try @@ -37,7 +37,7 @@ let load_rcfile ~rcfile ~time ~state = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc + Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc with Not_found -> state (* Flags.if_verbose diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index deb2c2038..5afc4e182 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -90,10 +90,10 @@ let outputstate opts = (******************************************************************************) let load_vernacular opts ~state = List.fold_left - (fun state (f_in, verbosely) -> + (fun state (f_in, echo) -> let s = Loadpath.locate_file f_in in (* Should make the beautify logic clearer *) - let load_vernac f = Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true ~state f in + let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in if !Flags.beautify then Flags.with_option Flags.beautify_file load_vernac f_in else load_vernac s @@ -192,7 +192,7 @@ let ensure_exists f = fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile opts ~verbosely ~f_in ~f_out = +let compile opts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in @@ -230,7 +230,7 @@ let compile opts ~verbosely ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -271,7 +271,7 @@ let compile opts ~verbosely ~f_in ~f_out = let state = { doc; sid; proof = None } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in - let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~time:opts.time ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in @@ -286,17 +286,17 @@ let compile opts ~verbosely ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile opts ~verbosely ~f_in ~f_out = +let compile opts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts ~verbosely ~f_in ~f_out; + compile opts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts (f_in, verbosely) = +let compile_file opts (f_in, echo) = if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts ~verbosely ~f_in ~f_out:None) f_in + (fun f_in -> compile opts ~echo ~f_in ~f_out:None) f_in else - compile opts ~verbosely ~f_in ~f_out:None + compile opts ~echo ~f_in ~f_out:None let compile_files opts = let compile_list = List.rev opts.compile_list in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a84990f91..5d3addfec 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -40,37 +40,6 @@ let vernac_echo ?loc in_chan = let open Loc in Feedback.msg_notice @@ str @@ really_input_string in_chan len ) loc -(* vernac parses the given stream, executes interpfun on the syntax tree it - * parses, and is verbose on "primitives" commands if verbosely is true *) - -let beautify_suffix = ".beautified" - -let set_formatter_translator ch = - let out s b e = output_substring ch s b e in - let ft = Format.make_formatter out (fun () -> flush ch) in - Format.pp_set_max_boxes ft max_int; - ft - -let pr_new_syntax_in_context ?loc ft_beautify ocom = - let loc = Option.cata Loc.unloc (0,0) loc in - let fs = States.freeze ~marshallable:`No in - (* Side-effect: order matters *) - let before = comment (CLexer.extract_comments (fst loc)) in - let com = match ocom with - | Some com -> Ppvernac.pr_vernac com - | None -> mt() in - let after = comment (CLexer.extract_comments (snd loc)) in - if !Flags.beautify_file then - (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after)); - Format.pp_print_flush ft_beautify ()) - else - Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); - States.unfreeze fs - -let pr_new_syntax ?loc po ft_beautify ocom = - (* Reinstall the context of parsing which includes the bindings of comments to locations *) - Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc ft_beautify) ocom - (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) @@ -174,18 +143,16 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -let load_vernac ~time ~verbosely ~check ~interactive ~state file = - let ft_beautify, close_beautify = - if !Flags.beautify_file then - let chan_beautify = open_out (file^beautify_suffix) in - set_formatter_translator chan_beautify, fun () -> close_out chan_beautify; - else - !Topfmt.std_ft, fun () -> () - in +let load_vernac_core ~time ~echo ~check ~interactive ~state file = + (* Keep in sync *) let in_chan = open_utf8_file_in file in - let in_echo = if verbosely then Some (open_utf8_file_in file) else None in + let in_echo = if echo then Some (open_utf8_file_in file) else None in + let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in + let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let rstate = ref state in + (* For beautify, list of parsed sids *) + let rids = ref [] in let open State in try (* we go out of the following infinite loop when a End_of_input is @@ -212,36 +179,78 @@ let load_vernac ~time ~verbosely ~check ~interactive ~state file = *) in (* Printing of vernacs *) - if !Flags.beautify then pr_new_syntax ?loc in_pa ft_beautify (Some ast); Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in + rids := state.sid :: !rids; rstate := state; done; - !rstate + input_cleanup (); + !rstate, !rids, Pcoq.Gram.comment_state in_pa with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - close_in in_chan; - Option.iter close_in in_echo; + input_cleanup (); match e with - | Stm.End_of_input -> - (* Is this called so comments at EOF are printed? *) - if !Flags.beautify then - pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None; - if !Flags.beautify_file then close_beautify (); - !rstate - | reraise -> - if !Flags.beautify_file then close_beautify (); - iraise (disable_drop e, info) - -(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] - It executes one vernacular command. By default the command is - considered as non-state-preserving, in which case we add it to the - Backtrack stack (triggering a save of a frozen state and the generation - of a new state label). An example of state-preserving command is one coming - from the query panel of Coqide. *) + | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa + | reraise -> iraise (disable_drop e, info) let process_expr ~time ~state loc_ast = checknav_deep loc_ast; interp_vernac ~time ~interactive:true ~check:true ~state loc_ast + +(******************************************************************************) +(* Beautify-specific code *) +(******************************************************************************) + +(* vernac parses the given stream, executes interpfun on the syntax tree it + * parses, and is verbose on "primitives" commands if verbosely is true *) +let beautify_suffix = ".beautified" + +let set_formatter_translator ch = + let out s b e = output_substring ch s b e in + let ft = Format.make_formatter out (fun () -> flush ch) in + Format.pp_set_max_boxes ft max_int; + ft + +let pr_new_syntax ?loc ft_beautify ocom = + let loc = Option.cata Loc.unloc (0,0) loc in + let before = comment (Pputils.extract_comments (fst loc)) in + let com = Option.cata Ppvernac.pr_vernac (mt ()) ocom in + let after = comment (Pputils.extract_comments (snd loc)) in + if !Flags.beautify_file then + (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after)); + Format.pp_print_flush ft_beautify ()) + else + Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))) + +(* load_vernac with beautify *) +let beautify_pass ~doc ~comments ~ids ~filename = + let ft_beautify, close_beautify = + if !Flags.beautify_file then + let chan_beautify = open_out (filename^beautify_suffix) in + set_formatter_translator chan_beautify, fun () -> close_out chan_beautify; + else + !Topfmt.std_ft, fun () -> () + in + (* The interface to the comment printer is imperative, so we first + set the comments, then we call print. This has to be done for + each file. *) + Pputils.beautify_comments := comments; + List.iter (fun id -> + Option.iter (fun (loc,ast) -> + pr_new_syntax ?loc ft_beautify (Some ast)) + (Stm.get_ast ~doc id)) ids; + + (* Is this called so comments at EOF are printed? *) + pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) ft_beautify None; + close_beautify () + +(* Main driver for file loading. For now, we only do one beautify + pass. *) +let load_vernac ~time ~echo ~check ~interactive ~state filename = + let ostate, ids, comments = load_vernac_core ~time ~echo ~check ~interactive ~state filename in + (* Pass for beautify *) + if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename; + (* End pass *) + ostate diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index e909ada1e..ca825197b 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -26,5 +26,5 @@ val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.l (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> +val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool -> state:State.t -> string -> State.t |