diff options
63 files changed, 450 insertions, 284 deletions
diff --git a/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh new file mode 100644 index 0000000000..4c8cdbbb45 --- /dev/null +++ b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then + + overlay perennial https://github.com/herbelin/perennial master+adapt13512-fresness-names-apply-in-introduction-pattern + +fi diff --git a/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh new file mode 100644 index 0000000000..69bd038b78 --- /dev/null +++ b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh @@ -0,0 +1 @@ +overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725 diff --git a/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst new file mode 100644 index 0000000000..aaacb2aadf --- /dev/null +++ b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Possible collision between a user-level name and an internal name when + using the :n:`%` introduction pattern + (`#13512 <https://github.com/coq/coq/pull/13512>`_, + fixes `#13413 <https://github.com/coq/coq/issues/13413>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13699-fix13579.rst b/doc/changelog/04-tactics/13699-fix13579.rst new file mode 100644 index 0000000000..9cf62fb595 --- /dev/null +++ b/doc/changelog/04-tactics/13699-fix13579.rst @@ -0,0 +1,6 @@ +- **Fixed:** + :tacn:`simpl` and :tacn:`hnf` now reduce primitive functions + on primitive integers, floats and arrays + (`#13699 <https://github.com/coq/coq/pull/13699>`_, + fixes `#13579 <https://github.com/coq/coq/issues/13579>`_, + by Pierre Roux). diff --git a/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst new file mode 100644 index 0000000000..653e9cd0cd --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst @@ -0,0 +1,5 @@ +- **Changed:** + :cmd:`Hint Rewrite` now supports locality attributes (including :attr:`export`) like other :ref:`Hint <creating_hints>` commands + (`#13725 <https://github.com/coq/coq/pull/13725>`_, + fixes `#13724 <https://github.com/coq/coq/issues/13724>`_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b63ae32311..2046788ef3 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -339,7 +339,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite Ack0 Ack1 Ack2 : base0. + Global Hint Rewrite Ack0 Ack1 Ack2 : base0. .. coqtop:: all @@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite g0 g1 g2 using lia : base1. + Global Hint Rewrite g0 g1 g2 using lia : base1. .. coqtop:: in diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index d7228a3907..d2e88261ae 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -273,12 +273,15 @@ Creating Hints :cmd:`Import` or :cmd:`Require` the current module. + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current - module, but not when they only :cmd:`Require` it. This attribute is supported by - all `Hint` commands except for :cmd:`Hint Rewrite`. + module, but not when they only :cmd:`Require` it. + :attr:`global` hints are visible from other modules when they :cmd:`Import` or :cmd:`Require` the current module. + .. versionadded:: 8.14 + + The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands. + .. deprecated:: 8.13 The default value for hint locality will change in a future diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f3ba884856..8138b4c6d9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1463,23 +1463,33 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PIf (c,b1,b2) -> GIf (glob_of_pat avoid env sigma c, (Anonymous,None), glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2) - | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> - let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in + | PCase ({cip_style=Constr.LetStyle},None,tm,[(0,n,b)]) -> + let n, b = glob_of_pat_under_context avoid env sigma (n, b) in + let nal = Array.to_list n in GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b) | PCase (info,p,tm,bl) -> let mat = match bl, info.cip_ind with | [], _ -> [] | _, Some ind -> - let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in - simple_cases_matrix_of_branches ind bl' + let map (i, n, c) = + let n, c = glob_of_pat_under_context avoid env sigma (n, c) in + let nal = Array.to_list n in + let mkPatVar na = DAst.make @@ PatVar na in + let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in + let ids = List.map_filter Nameops.Name.to_option nal in + CAst.make @@ (ids,[p],c) + in + List.map map bl | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in let mat = if info.cip_extensible then mat @ [any_any_branch] else mat in - let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with - | PMeta None, _, _ -> (Anonymous,None),None - | _, Some ind, Some nargs -> - return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p) + let indnames,rtn = match p, info.cip_ind with + | None, _ -> (Anonymous,None),None + | Some p, Some ind -> + let nas, p = glob_of_pat_under_context avoid env sigma p in + let nas = Array.rev_to_list nas in + ((List.hd nas, Some (CAst.make (ind, List.tl nas))), Some p) | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) @@ -1523,6 +1533,18 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with let glob_of = glob_of_pat avoid env sigma in GArray (None, Array.map glob_of t, glob_of def, glob_of ty) +and glob_of_pat_under_context avoid env sigma (nas, pat) = + let fold (avoid, env, nas, epat) na = + let na, avoid = compute_displayed_name_in_pattern sigma avoid na epat in + let env = Termops.add_name na env in + let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in + (avoid, env, na :: nas, epat) + in + let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in + let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in + let pat = glob_of_pat avoid' env' sigma pat in + (Array.rev_of_list nas, pat) + let extern_constr_pattern env sigma pat = extern true (InConstrEntrySomeLevel,(None,[])) (* XXX no vars? *) diff --git a/interp/notation.ml b/interp/notation.ml index 33d96f0439..d6002d71b5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1357,6 +1357,7 @@ let find_with_delimiters = function match (String.Map.find scope !scope_map).delimiters with | Some key -> Some (Some scope, Some key) | None -> None + | exception Not_found -> None let rec find_without_delimiters find (ntn_scope,ntn) = function | OpenScopeItem scope :: scopes -> diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index a32c8f1cd1..8edf916a7a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1171,16 +1171,6 @@ module FNativeEntries = fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) }; fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) }; | None -> defined_f_class := false - let defined_refl = ref false - - let frefl = ref dummy - - let init_refl retro = - match retro.Retroknowledge.retro_refl with - | Some crefl -> - defined_refl := true; - frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) } - | None -> defined_refl := false let defined_array = ref false @@ -1197,7 +1187,6 @@ module FNativeEntries = init_cmp !current_retro; init_f_cmp !current_retro; init_f_class !current_retro; - init_refl !current_retro; init_array !current_retro let check_env env = diff --git a/kernel/environ.ml b/kernel/environ.ml index 6f2aeab203..63fbaa6a3b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -571,6 +571,12 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let get_primitive env c = + let cb = lookup_constant c env in + match cb.Declarations.const_body with + | Declarations.Primitive p -> Some p + | _ -> None + let is_int63_type env c = match env.retroknowledge.Retroknowledge.retro_int63 with | None -> false diff --git a/kernel/environ.mli b/kernel/environ.mli index dfd9173d10..414ef2b4d7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -248,6 +248,7 @@ val constant_type_in : env -> Constant.t puniverses -> types val constant_opt_value_in : env -> Constant.t puniverses -> constr option val is_primitive : env -> Constant.t -> bool +val get_primitive : env -> Constant.t -> CPrimitives.t option val is_array_type : env -> Constant.t -> bool val is_int63_type : env -> Constant.t -> bool diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index f7c4b62d1f..505f6c648d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -35,7 +35,6 @@ type retroknowledge = { (* PNormal, NNormal, PSubn, NSubn, PZero, NZero, PInf, NInf, NaN *) - retro_refl : constructor option } let empty = { @@ -48,7 +47,6 @@ let empty = { retro_cmp = None; retro_f_cmp = None; retro_f_class = None; - retro_refl = None; } type action = diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index fd412cdd0a..80c0baaf95 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -29,7 +29,6 @@ type retroknowledge = { (* PNormal, NNormal, PSubn, NSubn, PZero, NZero, PInf, NInf, NaN *) - retro_refl : constructor option } val empty : retroknowledge diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 90c366ed63..d9da47134d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -299,7 +299,7 @@ TACTIC EXTEND rewrite_star { -let add_rewrite_hint ~poly bases ort t lcsr = +let add_rewrite_hint ~locality ~poly bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in let f ce = @@ -315,7 +315,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = in CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in let eqs = List.map f lcsr in - let add_hints base = add_rew_rules base eqs in + let add_hints base = add_rew_rules ~locality base eqs in List.iter add_hints bases let classify_hint _ = VtSideff ([], VtLater) @@ -323,15 +323,15 @@ let classify_hint _ = VtSideff ([], VtLater) } VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:polymorphic bl o None l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic bl o None l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:polymorphic bl o (Some t) l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - { add_rewrite_hint ~poly:polymorphic ["core"] o None l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l } + { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l } END (**********************************************************************) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index c77feeafbb..15d1ddb4ec 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -352,10 +352,9 @@ let matches_core env sigma allow_bound_rels (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) -> - let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in - let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in - let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in - let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in + let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in + let ctx_b2,b2 = br2.(0) in + let ctx_b2',b2' = br2.(1) in let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then @@ -370,7 +369,7 @@ let matches_core env sigma allow_bound_rels raise PatternMatchingFailure | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) -> - let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in + let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in let n2 = Array.length br2 in let () = match ci1.cip_ind with | None -> () @@ -383,14 +382,37 @@ let matches_core env sigma allow_bound_rels if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) then raise PatternMatchingFailure in + let sorec_under_ctx subst (n, c1) (decls, c2) = + let env = push_rel_context decls env in + let rec fold (ctx, subst) nas decls = match nas, decls with + | [], _ -> + (* Historical corner case: less bound variables are allowed in + destructuring let-bindings. See #13735. *) + (ctx, subst) + | na1 :: nas, d :: decls -> + let na2 = Context.Rel.Declaration.get_annot d in + let t = Context.Rel.Declaration.get_type d in + let ctx = push_binder na1 na2 t ctx in + let subst = add_binders na1 na2 binding_vars subst in + fold (ctx, subst) nas decls + | _, [] -> + assert false + in + let ctx, subst = fold (ctx, subst) (Array.to_list n) (List.rev decls) in + sorec ctx env subst c1 c2 + in let chk_branch subst (j,n,c) = (* (ind,j+1) is normally known to be a correct constructor and br2 a correct match over the same inductive *) assert (j < n2); - sorec ctx env subst c br2.(j) + sorec_under_ctx subst (n, c) br2.(j) + in + let subst = sorec ctx env subst a1 a2 in + let subst = match p1 with + | None -> subst + | Some p1 -> sorec_under_ctx subst p1 p2 in - let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in - List.fold_left chk_branch chk_head br1 + List.fold_left chk_branch subst br1 | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2)) when Array.equal Int.equal ln1 ln2 && i1 = i2 -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb5125f5ed..722a0a2048 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1160,18 +1160,3 @@ let rec subst_glob_constr env subst = DAst.map (function GArray(u,t',def',ty') ) - -(* Utilities to transform kernel cases to simple pattern-matching problem *) - -let simple_cases_matrix_of_branches ind brs = - List.map (fun (i,n,b) -> - let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = DAst.make @@ PatVar na in - let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let ids = List.map_filter Nameops.Name.to_option nal in - CAst.make @@ (ids,[p],c)) - brs - -let return_type_of_predicate ind nrealargs_tags pred = - let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in - (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 254f772ff8..6d6f7fa97b 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -72,14 +72,6 @@ val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option val force_wildcard : unit -> bool val synthetize_type : unit -> bool -(** Utilities to transform kernel cases to simple pattern-matching problem *) - -val it_destRLambda_or_LetIn_names : bool list -> glob_constr -> Name.t list * glob_constr -val simple_cases_matrix_of_branches : - inductive -> (int * bool list * glob_constr) list -> cases_clauses -val return_type_of_predicate : - inductive -> bool list -> glob_constr -> predicate_pattern * glob_constr option - val subst_genarg_hook : (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index f6d61f4892..553511f1bf 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -18,7 +18,6 @@ type patvar = Id.t type case_info_pattern = { cip_style : Constr.case_style; cip_ind : inductive option; - cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = @@ -35,8 +34,8 @@ type constr_pattern = | PSort of Sorts.family | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * bool list * constr_pattern) list (** index of constructor, nb of args *) + | PCase of case_info_pattern * (Name.t array * constr_pattern) option * constr_pattern * + (int * Name.t array * constr_pattern) list (** index of constructor, nb of args *) | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) | PInt of Uint63.t diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 47097a0e32..0c4bbf71e2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -24,7 +24,6 @@ open Environ let case_info_pattern_eq i1 i2 = i1.cip_style == i2.cip_style && Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind && - Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags && i1.cip_extensible == i2.cip_extensible let rec constr_pattern_eq p1 p2 = match p1, p2 with @@ -51,7 +50,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) -> case_info_pattern_eq info1 info2 && - constr_pattern_eq p1 p2 && + Option.equal (fun (nas1, p1) (nas2, p2) -> Array.equal Name.equal nas1 nas2 && constr_pattern_eq p1 p2) p1 p2 && constr_pattern_eq r1 r2 && List.equal pattern_eq l1 l2 | PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) -> @@ -74,7 +73,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = - Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2 + Int.equal i1 i2 && Array.equal Name.equal j1 j2 && constr_pattern_eq p1 p2 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && @@ -92,8 +91,8 @@ let rec occur_meta_pattern = function | PIf (c,c1,c2) -> (occur_meta_pattern c) || (occur_meta_pattern c1) || (occur_meta_pattern c2) - | PCase(_,p,c,br) -> - (occur_meta_pattern p) || + | PCase(_, p,c,br) -> + Option.cata (fun (_, p) -> occur_meta_pattern p) false p || (occur_meta_pattern c) || (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) | PArray (t,def,ty) -> @@ -115,10 +114,10 @@ let rec occurn_pattern n = function | PIf (c,c1,c2) -> (occurn_pattern n c) || (occurn_pattern n c1) || (occurn_pattern n c2) - | PCase(_,p,c,br) -> - (occurn_pattern n p) || + | PCase(_, p, c, br) -> + Option.cata (fun (nas, p) -> occurn_pattern (Array.length nas + n) p) false p || (occurn_pattern n c) || - (List.exists (fun (_,_,p) -> occurn_pattern n p) br) + (List.exists (fun (_, nas, p) -> occurn_pattern (Array.length nas + n) p) br) | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> List.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false @@ -202,18 +201,25 @@ let pattern_of_constr env sigma t = | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) - | Case (ci, u, pms, p, iv, a, br) -> - let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in + | Case (ci, u, pms, p0, iv, a, br0) -> + let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in + let pattern_of_ctx c (nas, c0) = + let ctx, c = Term.decompose_lam_n_decls (Array.length nas) c in + let env = push_rel_context ctx env in + let c = pattern_of_constr env c in + (Array.map Context.binder_name nas, c) + in + let p = pattern_of_ctx p p0 in let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; - cip_ind_tags = Some ci.ci_pp_info.ind_tags; cip_extensible = false } in let branch_of_constr i c = - (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c) + let nas, c = pattern_of_ctx c br0.(i) in + (i, nas, c) in - PCase (cip, pattern_of_constr env p, pattern_of_constr env a, + PCase (cip, Some p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) | Fix (lni,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in @@ -242,7 +248,10 @@ let map_pattern_with_binders g f l = function | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b) | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) | PCase (ci,po,p,pl) -> - PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) + let fold nas l = Array.fold_left (fun l na -> g na l) l nas in + let map_branch (i, n, c) = (i, n, f (fold n l) c) in + let po = Option.map (fun (nas, po) -> nas, (f (fold nas l) po)) po in + PCase (ci,po,f l p, List.map map_branch pl) | PProj (p,pc) -> PProj (p, f l pc) | PFix (lni,(lna,tl,bl)) -> let l' = Array.fold_left (fun l na -> g na l) l lna in @@ -352,7 +361,11 @@ let rec subst_pattern env sigma subst pat = let ind = cip.cip_ind in let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in - let typ' = subst_pattern env sigma subst typ in + let map ((nas, typ) as t) = + let typ' = subst_pattern env sigma subst typ in + if typ' == typ then t else (nas, typ') + in + let typ' = Option.Smart.map map typ in let c' = subst_pattern env sigma subst c in let subst_branch ((i,n,c) as br) = let c' = subst_pattern env sigma subst c in @@ -382,8 +395,6 @@ let rec subst_pattern env sigma subst pat = let mkPLetIn na b t c = PLetIn(na,b,t,c) let mkPProd na t u = PProd(na,t,u) let mkPLambda na t b = PLambda(na,t,b) -let mkPLambdaUntyped na b = PLambda(na,PMeta None,b) -let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped let mkPProd_or_LetIn (na,_,bo,t) c = match bo with @@ -446,18 +457,14 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda na c = DAst.make ?loc @@ - GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in - let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; - cip_ind_tags = None; cip_extensible = false } in - let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in - PCase (cip, PMeta None, pat_of_raw metas vars b, - [0,tags,pat_of_raw metas vars c]) + let tags = Array.of_list nal (* Approximation which can be without let-ins... *) in + PCase (cip, None, pat_of_raw metas vars b, + [0,tags,pat_of_raw metas (List.rev_append (Array.to_list tags) vars) c]) | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind p = match DAst.get p with | PatCstr((ind,_),_,_) -> Some ind @@ -476,18 +483,17 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function let pred = match p,indnames with | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in - rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p)) - | None, _ -> PMeta None + Some (Array.rev_of_list (na :: List.rev nal), pat_of_raw metas nvars p) + | None, _ -> None | Some p, None -> match DAst.get p with - | GHole _ -> PMeta None + | GHole _ -> None | _ -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; cip_ind = ind; - cip_ind_tags = None; cip_extensible = ext } in (* Nota : when we have a non-trivial predicate, @@ -556,10 +562,10 @@ and pats_of_glob_branches loc metas vars ind brs = err ?loc (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in - let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in + let vars' = List.rev_append lna vars in + let tags = Array.of_list lna in + let pat = pat_of_raw metas vars' br in let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in - let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) | _ -> err ?loc:loc' (Pp.str "Non supported pattern.") diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d4866541b0..54a47a252d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -961,6 +961,9 @@ let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) +let whd_const_state c e = raw_whd_state_gen CClosure.RedFlags.(mkflags [fCONST c]) e +let whd_const c = red_of_state_red (whd_const_state c) + let whd_delta_state e = raw_whd_state_gen CClosure.delta e let whd_delta_stack = stack_red_of_state_red whd_delta_state let whd_delta = red_of_state_red whd_delta_state diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 140ebdc87d..41d16f1c3c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -178,6 +178,7 @@ val whd_betalet_stack : stack_reduction_function (** {6 Head normal forms } *) +val whd_const : Constant.t -> reduction_function val whd_delta_stack : stack_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index bd21ecef93..a103699716 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -68,8 +68,7 @@ let error_not_evaluable r = spc () ++ str "to an evaluable reference.") let is_evaluable_const env cst = - is_transparent env (ConstKey cst) && - (evaluable_constant cst env || is_primitive env cst) + is_transparent env (ConstKey cst) && evaluable_constant cst env let is_evaluable_var env id = is_transparent env (VarKey id) && evaluable_named id env @@ -163,6 +162,10 @@ let reference_value env sigma c u = | None -> raise NotEvaluable | Some d -> d +let is_primitive_val sigma c = match EConstr.kind sigma c with + | Int _ | Float _ | Array _ -> true + | _ -> false + (************************************************************************) (* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic). *) (* One reuses the name of the function after reduction of the fixpoint *) @@ -714,7 +717,8 @@ and reduce_params env sigma stack l = let arg = List.nth stack i in let rarg = whd_construct_stack env sigma arg in match EConstr.kind sigma (fst rarg) with - | Construct _ -> List.assign stack i (applist rarg) + | Construct _ | Int _ | Float _ | Array _ -> + List.assign stack i (applist rarg) | _ -> raise Redelimination) stack l @@ -770,6 +774,16 @@ and whd_simpl_stack env sigma = else s' with Redelimination -> s') + | Const (cst, _) when is_primitive env cst -> + (try + let args = + List.map_filter_i (fun i a -> + match a with CPrimitives.Kwhnf -> Some i | _ -> None) + (CPrimitives.kind (Option.get (get_primitive env cst))) in + let stack = reduce_params env sigma stack args in + whd_const cst env sigma (applist (x, stack)), [] + with Redelimination -> s') + | _ -> match match_eval_ref env sigma x stack with | Some (ref, u) -> @@ -880,11 +894,11 @@ and special_red_case env sigma (ci, u, pms, p, iv, c, lf) = in redrec (push_app sigma (c, [])) -(* reduce until finding an applied constructor or fail *) +(* reduce until finding an applied constructor (or primitive value) or fail *) and whd_construct_stack env sigma s = let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in - if reducible_mind_case sigma constr then s' + if reducible_mind_case sigma constr || is_primitive_val sigma constr then s' else match match_eval_ref env sigma constr cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index cc56de066d..1d876537ef 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -206,9 +206,15 @@ let subst_hintrewrite (subst,(rbase,list as node)) = (rbase,list') (* Declaration of the Hint Rewrite library object *) -let inHintRewrite : string * HintDN.t -> Libobject.obj = +let inGlobalHintRewrite : string * HintDN.t -> Libobject.obj = let open Libobject in - declare_object @@ superglobal_object_nodischarge "HINT_REWRITE" + declare_object @@ superglobal_object_nodischarge "HINT_REWRITE_GLOBAL" + ~cache:cache_hintrewrite + ~subst:(Some subst_hintrewrite) + +let inExportHintRewrite : string * HintDN.t -> Libobject.obj = + let open Libobject in + declare_object @@ global_object_nodischarge "HINT_REWRITE_EXPORT" ~cache:cache_hintrewrite ~subst:(Some subst_hintrewrite) @@ -250,7 +256,8 @@ let find_applied_relation ?loc env sigma c left2right = spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) -let add_rew_rules base lrul = +let add_rew_rules ~locality base lrul = + let () = Hints.check_hint_locality locality in let counter = ref 0 in let env = Global.env () in let sigma = Evd.from_env env in @@ -267,5 +274,9 @@ let add_rew_rules base lrul = rew_tac = Option.map intern t} in incr counter; HintDN.add pat (!counter, rul) dn) HintDN.empty lrul - in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) - + in + let open Goptions in + match locality with + | OptLocal -> cache_hintrewrite ((),(base,lrul)) + | OptDefault | OptGlobal -> Lib.add_anonymous_leaf (inGlobalHintRewrite (base,lrul)) + | OptExport -> Lib.add_anonymous_leaf (inExportHintRewrite (base,lrul)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 974aef8e8f..dec6cc5ef4 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -17,7 +17,7 @@ open Equality type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t (** To add rewriting rules to a base *) -val add_rew_rules : string -> raw_rew_rule list -> unit +val add_rew_rules : locality:Goptions.option_locality -> string -> raw_rew_rule list -> unit (** The AutoRewrite tactic. The optional conditions tell rewrite how to handle matching and side-condition solving. diff --git a/tactics/hints.ml b/tactics/hints.ml index 0cc8becd8f..058602acfd 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1187,6 +1187,28 @@ let create_hint_db l n st b = let hint = make_hint ~local:l n (CreateDB (b, st)) in Lib.add_anonymous_leaf (inAutoHint hint) +let warn_deprecated_hint_without_locality = + CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated" + (fun () -> strbrk "The default value for hint locality is currently \ + \"local\" in a section and \"global\" otherwise, but is scheduled to change \ + in a future release. For the time being, adding hints outside of sections \ + without specifying an explicit locality is therefore deprecated. It is \ + recommended to use \"export\" whenever possible.") + +let check_hint_locality = let open Goptions in function +| OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); +| OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); +| OptDefault -> + if not @@ Global.sections_are_opened () then + warn_deprecated_hint_without_locality () +| OptLocal -> () + let interp_locality = function | Goptions.OptDefault | Goptions.OptGlobal -> false, true | Goptions.OptExport -> false, false diff --git a/tactics/hints.mli b/tactics/hints.mli index f5947bb946..381c7a1951 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -182,6 +182,8 @@ val searchtable_map : hint_db_name -> hint_db val searchtable_add : (hint_db_name * hint_db) -> unit +val check_hint_locality : Goptions.option_locality -> unit + (** [create_hint_db local name st use_dn]. [st] is a transparency state for unification using this db [use_dn] switches the use of the discrimination net for all hints diff --git a/tactics/tactics.ml b/tactics/tactics.ml index aef6596e8f..c64f583428 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1295,7 +1295,7 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = +let clenv_refine_in ?err with_evars targetid replace sigma0 clenv tac = let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in let clenv = Clenv.update_clenv_evd clenv evd in @@ -1306,11 +1306,10 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = let new_hyp_prf = clenv_value clenv in let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in - let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas evd)) (Tacticals.New.tclTHENLAST - (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac) + (assert_after_then_gen ?err replace naming new_hyp_typ tac) exact_tac) (********************************************) (* Elimination tactics *) @@ -1361,7 +1360,7 @@ let elimination_in_clause_scheme env sigma with_evars ~flags if EConstr.eq_constr sigma hyp_typ new_hyp_typ then user_err ~hdr:"general_rewrite_in" (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' + clenv_refine_in with_evars id true sigma elimclause'' (fun id -> Proofview.tclUNIT ()) (* @@ -1810,6 +1809,7 @@ let apply_in_once ?(respect_opaque = false) with_delta let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in + let replace = Id.equal id targetid in let rec aux ?err idstoclear with_destruct c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1822,7 +1822,7 @@ let apply_in_once ?(respect_opaque = false) with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ?err with_evars targetid id sigma clause + clenv_refine_in ?err with_evars targetid replace sigma clause (fun id -> replace_error_option err ( apply_clear_request clear_flag false c <*> @@ -2320,26 +2320,31 @@ let rewrite_hyp_then with_evars thin l2r id tac = tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end -let prepare_naming ?loc = function - | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) - | IntroAnonymous -> NamingAvoid Id.Set.empty - | IntroFresh id -> NamingBasedOn (id, Id.Set.empty) - -let rec explicit_intro_names = let open CAst in function -| {v=IntroForthcoming _} :: l -> explicit_intro_names l -| {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l) +let rec collect_intro_names = let open CAst in function +| {v=IntroForthcoming _} :: l -> collect_intro_names l +| {v=IntroNaming (IntroIdentifier id)} :: l -> + let ids1, ids2 = collect_intro_names l in Id.Set.add id ids1, ids2 | {v=IntroAction (IntroOrAndPattern l)} :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in - let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in - List.fold_left fold Id.Set.empty ll + let fold (ids1',ids2') l = + let ids1, ids2 = collect_intro_names (l@l') in + Id.Set.union ids1 ids1', Id.Set.union ids2 ids2' in + List.fold_left fold (Id.Set.empty,Id.Set.empty) ll | {v=IntroAction (IntroInjection l)} :: l' -> - explicit_intro_names (l@l') + collect_intro_names (l@l') | {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> - explicit_intro_names (pat::l') -| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + collect_intro_names (pat::l') +| {v=IntroNaming (IntroFresh id)} :: l -> + let ids1, ids2 = collect_intro_names l in ids1, Id.Set.add id ids2 +| {v=(IntroNaming IntroAnonymous | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> - explicit_intro_names l -| [] -> Id.Set.empty + collect_intro_names l +| [] -> Id.Set.empty, Id.Set.empty + +let explicit_intro_names l = fst (collect_intro_names l) + +let explicit_all_intro_names l = + let ids1,ids2 = collect_intro_names l in Id.Set.union ids1 ids2 let rec check_name_unicity env ok seen = let open CAst in function | {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l @@ -2364,30 +2369,33 @@ let rec check_name_unicity env ok seen = let open CAst in function check_name_unicity env ok seen l | [] -> () -let wild_id = Id.of_string "_tmp" +let fresh_wild ids = + let rec aux s = + if Id.Set.exists (fun id -> String.is_prefix s (Id.to_string id)) ids + then aux (s ^ "'") + else Id.of_string s in + aux "_H" -let rec list_mem_assoc_right id = function - | [] -> false - | {CAst.v=id'}::l -> Id.equal id id' || list_mem_assoc_right id l - -let check_thin_clash_then id thin avoid tac = - if list_mem_assoc_right id thin then - let newid = next_ident_away (add_suffix id "'") avoid in - let thin = - List.map CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in - Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin) - else - tac thin +let make_naming ?loc avoid l = function + | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) + | IntroAnonymous -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) + | IntroFresh id -> NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)) -let make_tmp_naming avoid l = function +let rec make_naming_action avoid l = function (* In theory, we could use a tmp id like "wild_id" for all actions but we prefer to avoid it to avoid this kind of "ugly" names *) - (* Alternatively, we could have called check_thin_clash_then on - IntroAnonymous, but at the cost of a "renaming"; Note that in the - case of IntroFresh, we should use check_thin_clash_then anyway to - prevent the case of an IntroFresh precisely using the wild_id *) - | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) - | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) + | IntroWildcard -> + NamingBasedOn (fresh_wild (Id.Set.union avoid (explicit_all_intro_names l)), Id.Set.empty) + | IntroApplyOn (_,{CAst.v=pat;loc}) -> make_naming_pattern avoid ?loc l pat + | (IntroOrAndPattern _ | IntroInjection _ | IntroRewrite _) as pat -> + NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) + +and make_naming_pattern ?loc avoid l = function + | IntroNaming pat -> make_naming ?loc avoid l pat + | IntroAction pat -> make_naming_action avoid l pat + | IntroForthcoming _ -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) + +let prepare_naming ?loc pat = make_naming ?loc Id.Set.empty [] pat let fit_bound n = function | None -> true @@ -2426,38 +2434,21 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac = [CAst.make @@ IntroNaming IntroAnonymous] | {CAst.loc;v=pat} :: l -> if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else + let naming = make_naming_pattern avoid l pat in match pat with | IntroForthcoming onlydeps -> - intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt onlydeps bound n + intro_forthcoming_then_gen naming destopt onlydeps bound n (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound (n+List.length ids) tac l) | IntroAction pat -> - intro_then_gen (make_tmp_naming avoid l pat) - destopt true false + intro_then_gen naming destopt true false (intro_pattern_action ?loc with_evars pat thin destopt (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0 (fun ids thin -> intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l))) | IntroNaming pat -> - intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l - - (* Pi-introduction rule, used backwards *) -and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l = - match pat with - | IntroIdentifier id -> - check_thin_clash_then id thin avoid (fun thin -> - intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)) - | IntroAnonymous -> - intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) - | IntroFresh id -> - (* todo: avoid thinned names to interfere with generation of fresh name *) - intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) + intro_then_gen naming destopt true false + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound (n+1) tac l) and intro_pattern_action ?loc with_evars pat thin destopt tac id = match pat with @@ -2470,24 +2461,16 @@ and intro_pattern_action ?loc with_evars pat thin destopt tac id = | IntroRewrite l2r -> rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None []) | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> - let naming,tac_ipat = - prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in - let doclear = - if naming = NamingMustBe (CAst.make ?loc id) then - Proofview.tclUNIT () (* apply_in_once do a replacement *) - else - clear [id] in - let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) - in + let naming = NamingMustBe (CAst.make ?loc id) in + let tac_ipat = prepare_action ?loc with_evars destopt pat in + let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f) - (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) + (fun id -> Tacticals.New.tclTHENLIST [tac_ipat id; tac thin None []]) -and prepare_intros ?loc with_evars dft destopt = function +and prepare_action ?loc with_evars destopt = function | IntroNaming ipat -> - prepare_naming ?loc ipat, - (fun id -> move_hyp id destopt) + (fun _ -> Proofview.tclUNIT ()) | IntroAction ipat -> - prepare_naming ?loc dft, (let tac thin bound = intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in @@ -2524,9 +2507,19 @@ let intros_patterns with_evars = function (* Forward reasoning *) (**************************) -let prepare_intros_opt with_evars dft destopt = function - | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) - | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat +let prepare_intros_opt with_evars dft destopt ipat = + let naming, loc, ipat = match ipat with + | None -> + let pat = IntroNaming dft in make_naming_pattern Id.Set.empty [] pat, None, pat + | Some {CAst.loc;v=(IntroNaming pat as ipat)} -> + (* "apply ... in H as id" needs to use id and H is kept iff id<>H *) + prepare_naming ?loc pat, loc, ipat + | Some {CAst.loc;v=(IntroAction pat as ipat)} -> + (* "apply ... in H as pat" reuses H so that old H is always cleared *) + (match dft with IntroIdentifier _ -> prepare_naming ?loc dft | _ -> make_naming_action Id.Set.empty [] pat), + loc, ipat + | Some {CAst.loc;v=(IntroForthcoming _)} -> assert false in + naming, prepare_action ?loc with_evars destopt ipat let ipat_of_name = function | Anonymous -> None @@ -3041,8 +3034,7 @@ let specialize (c,lbind) ipat = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> (* Like assert (id:=id args) but with the concept of specialization *) - let naming,tac = - prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in + let naming,tac = prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in let repl = do_replace (Some id) naming in Tacticals.New.tclTHENFIRST (assert_before_then_gen repl naming typ tac) @@ -3055,10 +3047,10 @@ let specialize (c,lbind) ipat = (* TODO: add intro to be more homogeneous. It will break scripts but will be easy to fix *) (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) - | Some {CAst.loc;v=ipat} -> + | Some _ as ipat -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in + let naming, tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) (exact_no_check term) diff --git a/test-suite/bugs/closed/bug_13413.v b/test-suite/bugs/closed/bug_13413.v new file mode 100644 index 0000000000..b4414a6a1d --- /dev/null +++ b/test-suite/bugs/closed/bug_13413.v @@ -0,0 +1,20 @@ +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?H%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H J%H H0. +exact J. +Qed. + +Set Mangle Names. +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H _0. +assumption. +Qed. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e46774f68a..9fd846ac16 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {B}%type_scope {y}, [_] _ @@ -22,7 +22,7 @@ eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [_] _ (where some original arguments have been renamed) Expands to: Constructor Coq.Init.Logic.eq_refl -Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x. Arguments myEq _%type_scope _ _ Arguments myrefl {C}%type_scope x _ @@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq A B x x + myrefl : B -> myEq A B x x. Arguments myEq (_ _)%type_scope _ _ Arguments myrefl A%type_scope {C}%type_scope x _ diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8e10107673..fc3b6fbd99 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,7 +5,7 @@ A : Set a : A l : list' A Unable to unify "list' (A * A)%type" with "list' A". -Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x. Arguments foo _%type_scope _ Arguments Foo _%type_scope _ diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 02e58775b5..fdd609f5b2 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}. Arguments sig2 [A]%type_scope (_ _)%type_scope Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index ca8e1b58a8..7ca4de1e46 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -56,3 +56,21 @@ t = 2%i63 : int = 37151199385380486 : int + = 4 + : int + = 4 + : int + = 4 + : int + = add + : int -> int -> int + = 12 + : int + = 12 + : int + = 12 + : int + = 3 + x + : int + = 1 + 2 + x + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 6f1046f7a5..50910264f2 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -40,3 +40,18 @@ Open Scope int63_scope. Check (2+2). Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. + +Eval simpl in 2+2. +Eval hnf in 2+2. +Eval cbn in 2+2. +Eval hnf in PrimInt63.add. + +Eval simpl in (2 * 3) + (2 * 3). +Eval hnf in (2 * 3) + (2 * 3). +Eval cbn in (2 * 3) + (2 * 3). + +Section TestNoSimpl. +Variable x : int. +Eval simpl in 1 + 2 + x. +Eval hnf in 1 + 2 + x. +End TestNoSimpl. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index fe16dba496..03b9e3b527 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%type_scope _%function_scope _ _ Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := - existT : forall x : A, P x -> {x : A & P x} + existT : forall x : A, P x -> {x : A & P x}. Arguments sigT [A]%type_scope _%type_scope Arguments existT [A]%type_scope _%function_scope _ _ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, [_] _ @@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := - le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope @@ -60,7 +60,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := - Eq : comparison | Lt : comparison | Gt : comparison + Eq : comparison | Lt : comparison | Gt : comparison. bar : foo bar is not universe polymorphic @@ -78,7 +78,7 @@ Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, {_} _ diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out index 1a9bc068c5..7c7600b786 100644 --- a/test-suite/output/PrintModule.out +++ b/test-suite/output/PrintModule.out @@ -7,3 +7,11 @@ Module N : S with Module T := K := M Module N : S with Module T := M Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End +Module +A +:= Struct + Variant I : Set := C : nat -> I. + Record R : Set := Build_R { n : nat }. + Definition n : R -> nat. + End + diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v index 54ef305be4..b4de03b556 100644 --- a/test-suite/output/PrintModule.v +++ b/test-suite/output/PrintModule.v @@ -60,3 +60,10 @@ Print Func. End Shortest_path. End QUX. + +Module A. +Variant I := C : nat -> I. +Record R := { n : nat }. +End A. + +Print Module A. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 95b6c6ee95..4993b747fa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,6 +1,7 @@ -Inductive Empty@{uu} : Type@{uu} := +Inductive Empty@{uu} : Type@{uu} := . (* uu |= *) -Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap + { punwrap : A }. (* uu |= *) PWrap has primitive projections with eta conversion. @@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p (* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap + { runwrap : A }. (* uu |= *) Arguments RWrap _%type_scope @@ -80,9 +82,9 @@ foo@{uu u v} = Type@{u} -> Type@{v} -> Type@{uu} : Type@{max(uu+1,u+1,v+1)} (* uu u v |= *) -Inductive Empty@{E} : Type@{E} := +Inductive Empty@{E} : Type@{E} := . (* E |= *) -Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }. (* E |= *) PWrap has primitive projections with eta conversion. @@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} + inseccstr : Type@{k} -> insecind@{k}. (* k |= *) Arguments inseccstr _%type_scope @@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* uu v |= *) Inductive insecind@{uu k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{uu k} + inseccstr : Type@{k} -> insecind@{uu k}. (* uu k |= *) Arguments inseccstr _%type_scope diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v index 71d333d439..0ac62fcdc9 100644 --- a/test-suite/success/autorewrite.v +++ b/test-suite/success/autorewrite.v @@ -4,25 +4,35 @@ Axiom Ack0 : forall m : nat, Ack 0 m = S m. Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). -Hint Rewrite Ack0 Ack1 Ack2 : base0. +Module M. + #[export] Hint Rewrite Ack0 Ack1 Ack2 : base0. -Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. + Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. + Proof. + intros. + autorewrite with base0 in H using try (apply H; reflexivity). + Qed. +End M. + +Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. Proof. intros. - autorewrite with base0 in H using try (apply H; reflexivity). -Qed. + Fail autorewrite with base0 in *. +Abort. + +Import M. Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. Proof. intros. autorewrite with base0 in *. - apply H;reflexivity. + apply H;reflexivity. Qed. (* Check autorewrite does not solve existing evars *) (* See discussion started by A. Chargueraud in Oct 2010 on coqdev *) -Hint Rewrite <- plus_n_O : base1. +Global Hint Rewrite <- plus_n_O : base1. Goal forall y, exists x, y+x = y. eexists. autorewrite with base1. Fail reflexivity. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 4e36dec15b..62c788e910 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -27,3 +27,7 @@ Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) 2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) Abort. +Goal nat. +assert nat as J%S by exact 0. +exact J. +Qed. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index d37ad9f528..b8fbff05c6 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -152,3 +152,15 @@ Definition d := ltac:(intro x; exact (x*x)). Definition d' : nat -> _ := ltac:(intros;exact 0). End Evar. + +Module Wildcard. + +(* We check that the wildcard internal name does not interfere with + user fresh names (currently the prefix is "_H") *) + +Goal nat -> bool -> nat -> bool. +intros _ ?_H ?_H. +exact _H. +Qed. + +End Wildcard. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index d597c0404a..5fe2cade3b 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of FSet Propositions *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 115c7cb365..d6277b3bb5 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -3327,7 +3327,7 @@ Ltac invlist f := (** * Exporting hints and tactics *) -Hint Rewrite +Global Hint Rewrite rev_involutive (* rev (rev l) = l *) rev_unit (* rev (l ++ a :: nil) = a :: rev l *) map_nth (* nth n (map f l) (f d) = f (nth n l d) *) diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index aa0c419f0e..579e5e9630 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of MSet Propositions *) diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f80929e320..2d210e24a6 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -651,7 +651,7 @@ Proof. destruct (rbal'_match l x r); ok. Qed. -Hint Rewrite In_node_iff In_leaf_iff +Global Hint Rewrite In_node_iff In_leaf_iff makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb. Ltac descolor := destruct_all Color.t. @@ -670,7 +670,7 @@ Proof. - descolor; autorew; rewrite IHl; intuition_in. - descolor; autorew; rewrite IHr; intuition_in. Qed. -Hint Rewrite ins_spec : rb. +Global Hint Rewrite ins_spec : rb. Instance ins_ok s x `{Ok s} : Ok (ins x s). Proof. @@ -685,7 +685,7 @@ Proof. unfold add. now autorew. Qed. -Hint Rewrite add_spec' : rb. +Global Hint Rewrite add_spec' : rb. Lemma add_spec s x y `{Ok s} : InT y (add x s) <-> X.eq y x \/ InT y s. @@ -754,7 +754,7 @@ Proof. * ok. apply lbal_ok; ok. Qed. -Hint Rewrite lbalS_spec rbalS_spec : rb. +Global Hint Rewrite lbalS_spec rbalS_spec : rb. (** ** Append for deletion *) @@ -807,7 +807,7 @@ Proof. [intros a y b | intros t Ht]; autorew; tauto. Qed. -Hint Rewrite append_spec : rb. +Global Hint Rewrite append_spec : rb. Lemma append_ok : forall x l r `{Ok l, Ok r}, lt_tree x l -> gt_tree x r -> Ok (append l r). @@ -861,7 +861,7 @@ induct s x. rewrite ?IHr by trivial; intuition_in; order. Qed. -Hint Rewrite del_spec : rb. +Global Hint Rewrite del_spec : rb. Instance del_ok s x `{Ok s} : Ok (del x s). Proof. @@ -882,7 +882,7 @@ Proof. unfold remove. now autorew. Qed. -Hint Rewrite remove_spec : rb. +Global Hint Rewrite remove_spec : rb. Instance remove_ok s x `{Ok s} : Ok (remove x s). Proof. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 48df5fe884..420c17c9a4 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -127,7 +127,7 @@ Qed. End N2Nat. -Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double +Global Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min N2Nat.id @@ -147,7 +147,7 @@ Proof. induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Hint Rewrite id : Nnat. +Global Hint Rewrite id : Nnat. Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. (** [N.of_nat] is hence injective *) @@ -206,7 +206,7 @@ Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. -Hint Rewrite Nat2N.id : Nnat. +Global Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index e3e8f532b3..374af6de63 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -348,7 +348,7 @@ Local Notation "- x" := (ZnZ.opp x). Local Infix "*" := ZnZ.mul. Local Notation wB := (base ZnZ.digits). -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_opp ZnZ.spec_sub : cyclic. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7c5b43096a..f74a78e876 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -51,7 +51,7 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. Ltac zify := unfold eq, zero, one, two, succ, pred, add, sub, mul in *; diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index f324bbf52b..7bb725538b 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -954,6 +954,7 @@ Proof. intros _ HH; generalize (HH H1); discriminate. clear H. generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl. + change 62%int63 with (digits - 1)%int63. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 0c097b6773..9d9244eefb 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -18,7 +18,7 @@ Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) -Hint Rewrite opp_0 : nz. +Global Hint Rewrite opp_0 : nz. Theorem add_pred_l n m : P n + m == P (n + m). Proof. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 4d2361689d..832931e5ef 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -26,7 +26,7 @@ Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. Ltac order_pos' := try apply abs_nonneg; order_pos. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -566,7 +566,7 @@ Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm) Ltac bitwise := bitwise as ?m ?Hm. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. (** The streams of bits that correspond to a numbers are exactly the ones which are stationary after some point. *) diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 66cbba9e08..2ad8dfcedb 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -14,9 +14,9 @@ Require Import NZAxioms NZBase. Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). -Hint Rewrite +Global Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. -Hint Rewrite one_succ two_succ : nz'. +Global Hint Rewrite one_succ two_succ : nz'. Ltac nzsimpl := autorewrite with nz. Ltac nzsimpl' := autorewrite with nz nz'. @@ -39,7 +39,7 @@ Proof. intros n m. now rewrite add_succ_r, add_succ_l. Qed. -Hint Rewrite add_0_r add_succ_r : nz. +Global Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. Proof. @@ -58,7 +58,7 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite add_1_l add_1_r : nz. +Global Hint Rewrite add_1_l add_1_r : nz. Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. @@ -104,6 +104,6 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite sub_1_r : nz. +Global Hint Rewrite sub_1_r : nz. End NZAddProp. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 3d6465191d..14728eaf40 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -28,7 +28,7 @@ Proof. now rewrite add_cancel_r. Qed. -Hint Rewrite mul_0_r mul_succ_r : nz. +Global Hint Rewrite mul_0_r mul_succ_r : nz. Theorem mul_comm : forall n m, n * m == m * n. Proof. @@ -69,7 +69,7 @@ Proof. intro n. now nzsimpl'. Qed. -Hint Rewrite mul_1_l mul_1_r : nz. +Global Hint Rewrite mul_1_l mul_1_r : nz. Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. Proof. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 3b2a496229..00edcd641f 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -45,7 +45,7 @@ Module Type NZPowProp (Import B : NZPow' A) (Import C : NZMulOrderProp A). -Hint Rewrite pow_0_r pow_succ_r : nz. +Global Hint Rewrite pow_0_r pow_succ_r : nz. (** Power and basic constants *) @@ -76,14 +76,14 @@ Proof. - now nzsimpl. Qed. -Hint Rewrite pow_1_r pow_1_l : nz. +Global Hint Rewrite pow_1_r pow_1_l : nz. Lemma pow_2_r : forall a, a^2 == a*a. Proof. intros. rewrite two_succ. nzsimpl; order'. Qed. -Hint Rewrite pow_2_r : nz. +Global Hint Rewrite pow_2_r : nz. (** Power and nullity *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 313b9adfd1..427a18d4ae 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -23,7 +23,7 @@ Module Type NBitsProp Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -368,7 +368,7 @@ Proof. split. apply bits_inj. intros EQ; now rewrite EQ. Qed. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. Tactic Notation "bitwise" "as" simple_intropattern(m) := apply bits_inj; intros m; autorewrite with bitwise. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index e97f2dc748..7d50bdacad 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -876,7 +876,7 @@ Lemma compare_xO_xI p q : (p~0 ?= q~1) = switch_Eq Lt (p ?= q). Proof. exact (compare_cont_spec p q Lt). Qed. -Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. +Global Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. Ltac simpl_compare := autorewrite with compare. Ltac simpl_compare_in H := autorewrite with compare in H. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 8813131d7b..18e55aefc6 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -40,8 +40,8 @@ Proof. reflexivity. Qed. -Hint Rewrite @compose_id_left @compose_id_right : core. -Hint Rewrite <- @compose_assoc : core. +Global Hint Rewrite @compose_id_left @compose_id_right : core. +Global Hint Rewrite <- @compose_assoc : core. (** [flip] is involutive. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 25af2d5ffb..090322054e 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -162,7 +162,7 @@ Ltac pi_eq_proofs := repeat pi_eq_proof. Ltac clear_eq_proofs := abstract_eq_proofs ; pi_eq_proofs. -Hint Rewrite <- eq_rect_eq : refl_id. +Global Hint Rewrite <- eq_rect_eq : refl_id. (** The [refl_id] database should be populated with lemmas of the form [coerce_* t eq_refl = t]. *) @@ -178,7 +178,7 @@ Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) : Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. Proof. apply UIP_refl. Qed. -Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. +Global Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. Ltac rewrite_refl_id := autorewrite with refl_id. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5a23a20811..620ed6b5b7 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -180,4 +180,4 @@ intros; rewrite Q2R_mult. rewrite Q2R_inv; auto. Qed. -Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. +Global Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 4ac54d280a..c3e67b9d5a 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -53,7 +53,7 @@ Module Type CompareFacts (Import O:DecStrOrder'). rewrite compare_gt_iff; intuition. Qed. - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. Proof. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index abf7f681b0..c709149109 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -146,7 +146,7 @@ Module MoreInt (Import I:Int). (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) - Hint Rewrite -> + Global Hint Rewrite -> i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max i2z_eqb i2z_ltb i2z_leb : i2z. diff --git a/vernac/printmod.ml b/vernac/printmod.ml index fdf7f6c74a..ba4a7857e7 100644 --- a/vernac/printmod.ml +++ b/vernac/printmod.ml @@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib udecl = let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ + (print_one_inductive env sigma mib) inds ++ str "." ++ Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) let get_fields = @@ -173,7 +173,7 @@ let print_record env mind mib udecl = prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> Id.print id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }." ++ Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f3fc46c12..1c774a35bf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1401,31 +1401,9 @@ let warn_implicit_core_hint_db = (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " ++ strbrk"Please specify a hint database.") -let warn_deprecated_hint_without_locality = - CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated" - (fun () -> strbrk "The default value for hint locality is currently \ - \"local\" in a section and \"global\" otherwise, but is scheduled to change \ - in a future release. For the time being, adding hints outside of sections \ - without specifying an explicit locality is therefore deprecated. It is \ - recommended to use \"export\" whenever possible.") - -let check_hint_locality = function -| OptGlobal -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the global attribute in sections."); -| OptExport -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the export attribute in sections."); -| OptDefault -> - if not @@ Global.sections_are_opened () then - warn_deprecated_hint_without_locality () -| OptLocal -> () - let vernac_remove_hints ~atts dbnames ids = let locality = Attributes.(parse option_locality atts) in - let () = check_hint_locality locality in + let () = Hints.check_hint_locality locality in let dbnames = if List.is_empty dbnames then (warn_implicit_core_hint_db (); ["core"]) @@ -1440,7 +1418,7 @@ let vernac_hints ~atts dbnames h = else dbnames in let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in - let () = check_hint_locality locality in + let () = Hints.check_hint_locality locality in Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = |