From be56f39ecfc0726772cc6930dbc7657348f008e1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 May 2020 14:19:04 +0200 Subject: Move the static check of evaluability in unfold tactic to runtime. See #11840 for a motivation. I had to fix Floats.FloatLemmas because it uses the same name for a notation and a term, and the fact this unfold was working on this was clearly a bug. I hope nobody relies on this kind of stuff in the wild. Fixes #5764: "Cannot coerce ..." should be a runtime error. Fixes #5159: "Cannot coerce ..." should not be an error. Fixes #4925: unfold gives error on Admitted. --- plugins/ltac/tacintern.ml | 59 ++++++++++++++++---------------------- test-suite/bugs/closed/bug_4925.v | 6 ++++ test-suite/bugs/closed/bug_5159.v | 12 ++++++++ test-suite/bugs/closed/bug_5764.v | 7 +++++ test-suite/success/with_strategy.v | 8 +++--- theories/Floats/FloatLemmas.v | 28 +++++++++--------- 6 files changed, 68 insertions(+), 52 deletions(-) create mode 100644 test-suite/bugs/closed/bug_4925.v create mode 100644 test-suite/bugs/closed/bug_5159.v create mode 100644 test-suite/bugs/closed/bug_5764.v diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 1aa3af0087..ff1e8b92d1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -14,7 +14,6 @@ open CAst open Pattern open Genredexpr open Glob_term -open Tacred open Util open Names open Libnames @@ -294,23 +293,30 @@ let intern_destruction_arg ist = function else clear,ElimOnIdent (make ?loc id) -let short_name = function - | {v=AN qid} when qualid_is_ident qid && not !strict_check -> +let short_name qid = + if qualid_is_ident qid && not !strict_check then Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) - | _ -> None - -let intern_evaluable_global_reference ist qid = - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) - with Not_found -> - if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else Nametab.error_global_not_found qid - -let intern_evaluable_reference_or_by_notation ist = function - | {v=AN r} -> intern_evaluable_global_reference ist r + else None + +let evalref_of_globref ?loc ?short = function + | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) + | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) + | r -> + user_err ?loc (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ + spc () ++ str "to an evaluable reference.") + +let intern_evaluable ist = function + | {v=AN qid} -> + begin match intern_global_reference ist qid with + | ArgVar _ as v -> v + | ArgArg (loc, r) -> + let short = short_name qid in + evalref_of_globref ?loc ?short r + end | {v=ByNotation (ntn,sc);loc} -> - evaluable_of_global_reference ist.genv - (Notation.interp_notation_as_global_reference ?loc - GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) + let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in + let r = Notation.interp_notation_as_global_reference ?loc check ntn sc in + evalref_of_globref ?loc r let intern_smart_global ist = function | {v=AN r} -> intern_global_reference ist r @@ -318,21 +324,6 @@ let intern_smart_global ist = function ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) -(* Globalize a reduction expression *) -let intern_evaluable ist r = - let f ist r = - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) - in - match r with - | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> - ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) - | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> - let id = qualid_basename qid in - ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) - | _ -> f ist r - let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) let intern_flag ist red = @@ -393,10 +384,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let c = Constrintern.interp_reference sign r in match DAst.get c with | GRef (r,None) -> - Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) + Inl (evalref_of_globref r) | GVar id -> - let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in - Inl (ArgArg (r,None)) + let r = evalref_of_globref (GlobRef.VarRef id) in + Inl r | _ -> let bound_names = Glob_ops.bound_glob_vars c in Inr (bound_names,(c,None),dummy_pat) in diff --git a/test-suite/bugs/closed/bug_4925.v b/test-suite/bugs/closed/bug_4925.v new file mode 100644 index 0000000000..d4e4b35351 --- /dev/null +++ b/test-suite/bugs/closed/bug_4925.v @@ -0,0 +1,6 @@ +Axiom a: bool. + +Goal a = true. +Proof. +try unfold a. +Abort. diff --git a/test-suite/bugs/closed/bug_5159.v b/test-suite/bugs/closed/bug_5159.v new file mode 100644 index 0000000000..cbc924c2d3 --- /dev/null +++ b/test-suite/bugs/closed/bug_5159.v @@ -0,0 +1,12 @@ +Axiom foo : Type. +Definition bar := 1. +Definition bar' := Eval cbv -[bar] in bar. +Declare Reduction red' := cbv -[bar]. +Opaque bar. +Definition bar'' := Eval red' in bar. +Declare Reduction red'' := cbv -[bar]. (* Error: Cannot coerce bar to an +evaluable reference. *) +Definition bar''' := Eval cbv -[bar] in bar. (* Error: Cannot coerce bar to an +evaluable reference. *) +Definition foo' := Eval cbv -[foo] in foo. (* Error: Cannot coerce foo to an +evaluable reference. *) diff --git a/test-suite/bugs/closed/bug_5764.v b/test-suite/bugs/closed/bug_5764.v new file mode 100644 index 0000000000..0b015d9c7e --- /dev/null +++ b/test-suite/bugs/closed/bug_5764.v @@ -0,0 +1,7 @@ +Module Type A. +Parameter a : nat. +End A. + +Module B (mA : A). +Ltac cbv_a := cbv [mA.a]. +End B. diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v index 077b57c87f..6f0833211e 100644 --- a/test-suite/success/with_strategy.v +++ b/test-suite/success/with_strategy.v @@ -195,8 +195,8 @@ Opaque F.id. Goal F.id 0 = F.id 0. Fail unfold F.id. - (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *) - Fail F.with_transparent_id ltac:(progress unfold F.id). + F.with_transparent_id ltac:(progress unfold F.id). + Undo. F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x). Abort. @@ -212,8 +212,8 @@ Opaque F2.id. Goal F2.id 0 = F2.id 0. Fail unfold F2.id. - (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *) - Fail F2.with_transparent_id ltac:(progress unfold F2.id). + F2.with_transparent_id ltac:(progress unfold F2.id). + Undo. F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x). Abort. diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v index 29b1451822..1be6d2502a 100644 --- a/theories/Floats/FloatLemmas.v +++ b/theories/Floats/FloatLemmas.v @@ -49,7 +49,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S rewrite Hmod_elim. clear Hmod_elim. revert Hv. - unfold valid_binary, bounded, canonical_mantissa. + unfold SpecFloat.valid_binary, bounded, canonical_mantissa. unfold fexp. rewrite Bool.andb_true_iff. intro H'. @@ -62,7 +62,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S destruct (Z.max_spec (Z.pos (digits2_pos m) + e0 - prec) emin) as [ (H, Hm) | (H, Hm) ]. + rewrite Hm in H1. rewrite <- H1. - rewrite !Z.max_l by (revert He; unfold emax, emin, prec; lia). + rewrite !Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (emin + _)%Z with emax by ring. unfold shl_align. rewrite <- H1 in H. @@ -74,7 +74,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold fexp. unfold Zdigits2. unfold shr_record_of_loc, shr. - rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). + rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z by ring. assert (Hs : (Z.pos (digits2_pos (shift_pos p m)) <= prec)%Z). { @@ -103,26 +103,26 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold round_nearest_even. remember (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z as ds. destruct ds. - * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). - rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with Z0 by lia. - rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). reflexivity. * exfalso; lia. - * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with (Zneg p0) by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). - rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with (Zneg p0) by lia. - rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). replace (_ - _)%Z with (Zneg p0) by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). reflexivity. - + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). + + rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). rewrite Hm in H1. clear Hm. replace (Zpos _ + _ - _)%Z with (e0 + (emax - emin))%Z by (rewrite <- H1 at 1; ring). @@ -134,7 +134,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold shr_fexp. unfold fexp. unfold Zdigits2. - rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). + rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). unfold shr_record_of_loc. unfold shr. unfold Zdigits2. @@ -142,17 +142,17 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold shr_m. unfold loc_of_shr_record. unfold round_nearest_even. - rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia). + rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. - rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia). + rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). reflexivity. - rewrite Z.min_le_iff. intro H. - destruct H as [ He | Habs ]; [ | revert Habs; now unfold emin, emax ]. + destruct H as [ He | Habs ]; [ | revert Habs; now unfold SpecFloat.emin, emax ]. unfold shl_align. assert (Hprec : (Z.pos (digits2_pos m) <= prec)%Z). { -- cgit v1.2.3 From 3af3409a8ec23deb3e0d32f00a31363a36f6209b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 May 2020 16:29:30 +0200 Subject: Generalize the interpretation of syntactic notation as reference to their head. This seems to be a pattern used quite a bit in the wild, it does not hurt to be a bit more lenient to tolerate this kind of use. Interestingly the API was already offering a similar generalization in some unrelated places. We also backtrack on the change in Floats.FloatLemmas since it is an instance of this phenomenon. --- interp/notation.ml | 8 ++++---- interp/notation.mli | 3 ++- interp/smartlocate.ml | 8 ++++---- plugins/ltac/tacintern.ml | 6 +++--- theories/Floats/FloatLemmas.v | 28 ++++++++++++++-------------- vernac/prettyp.ml | 4 ++-- vernac/vernacentries.ml | 2 +- 7 files changed, 30 insertions(+), 29 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 7761606f11..47cf4ec6ef 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1807,10 +1807,10 @@ let browse_notation strict ntn map = map [] in List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l -let global_reference_of_notation test (ntn,(sc,c,_)) = +let global_reference_of_notation ~head test (ntn,(sc,c,_)) = match c with | NRef ref when test ref -> Some (ntn,sc,ref) - | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref -> + | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref -> Some (ntn,sc,ref) | _ -> None @@ -1822,14 +1822,14 @@ let error_notation_not_reference ?loc ntn = (str "Unable to interpret " ++ quote (str ntn) ++ str " as a reference.") -let interp_notation_as_global_reference ?loc test ntn sc = +let interp_notation_as_global_reference ?loc ~head test ntn sc = let scopes = match sc with | Some sc -> let scope = find_scope (find_delimiters_scope sc) in String.Map.add sc scope String.Map.empty | None -> !scope_map in let ntns = browse_notation true ntn scopes in - let refs = List.map (global_reference_of_notation test) ntns in + let refs = List.map (global_reference_of_notation ~head test) ntns in match Option.List.flatten refs with | [_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn diff --git a/interp/notation.mli b/interp/notation.mli index 842f2b1458..cfe3ea12d0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes -> (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> +(** If head is true, also allows applied global references. *) +val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t (** Checks for already existing notations *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 98fa71e15d..03977fcb4e 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -62,15 +62,15 @@ let global_with_alias ?head qid = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid -let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function +let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> - global_with_alias ?head r + global_with_alias ~head r | ByNotation (ntn,sc) -> - Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc) + Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc) let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_inductive_with_alias r | ByNotation (ntn,sc) -> destIndRef - (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc)) + (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc)) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ff1e8b92d1..fcedbe8e2e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -97,7 +97,7 @@ let intern_global_reference ist qid = else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then let id = qualid_basename qid in ArgArg (qid.CAst.loc, GlobRef.VarRef id) - else match locate_global_with_alias qid with + else match locate_global_with_alias ~head:true qid with | r -> ArgArg (qid.CAst.loc, r) | exception Not_found -> if not !strict_check && qualid_is_ident qid then @@ -315,13 +315,13 @@ let intern_evaluable ist = function end | {v=ByNotation (ntn,sc);loc} -> let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in - let r = Notation.interp_notation_as_global_reference ?loc check ntn sc in + let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in evalref_of_globref ?loc r let intern_smart_global ist = function | {v=AN r} -> intern_global_reference ist r | {v=ByNotation (ntn,sc);loc} -> - ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v index 1be6d2502a..29b1451822 100644 --- a/theories/Floats/FloatLemmas.v +++ b/theories/Floats/FloatLemmas.v @@ -49,7 +49,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S rewrite Hmod_elim. clear Hmod_elim. revert Hv. - unfold SpecFloat.valid_binary, bounded, canonical_mantissa. + unfold valid_binary, bounded, canonical_mantissa. unfold fexp. rewrite Bool.andb_true_iff. intro H'. @@ -62,7 +62,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S destruct (Z.max_spec (Z.pos (digits2_pos m) + e0 - prec) emin) as [ (H, Hm) | (H, Hm) ]. + rewrite Hm in H1. rewrite <- H1. - rewrite !Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + rewrite !Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (emin + _)%Z with emax by ring. unfold shl_align. rewrite <- H1 in H. @@ -74,7 +74,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold fexp. unfold Zdigits2. unfold shr_record_of_loc, shr. - rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). replace (_ - _)%Z with (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z by ring. assert (Hs : (Z.pos (digits2_pos (shift_pos p m)) <= prec)%Z). { @@ -103,26 +103,26 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold round_nearest_even. remember (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z as ds. destruct ds. - * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (_ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). - rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (_ - _)%Z with Z0 by lia. - rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (_ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). reflexivity. * exfalso; lia. - * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (_ - _)%Z with (Zneg p0) by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). - rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (_ - _)%Z with (Zneg p0) by lia. - rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia). + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). replace (_ - _)%Z with (Zneg p0) by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). reflexivity. - + rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). + + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). rewrite Hm in H1. clear Hm. replace (Zpos _ + _ - _)%Z with (e0 + (emax - emin))%Z by (rewrite <- H1 at 1; ring). @@ -134,7 +134,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold shr_fexp. unfold fexp. unfold Zdigits2. - rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). unfold shr_record_of_loc. unfold shr. unfold Zdigits2. @@ -142,17 +142,17 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S unfold shr_m. unfold loc_of_shr_record. unfold round_nearest_even. - rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). + rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia). replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. - rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia). + rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia). replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). reflexivity. - rewrite Z.min_le_iff. intro H. - destruct H as [ He | Habs ]; [ | revert Habs; now unfold SpecFloat.emin, emax ]. + destruct H as [ He | Habs ]; [ | revert Habs; now unfold emin, emax ]. unfold shl_align. assert (Hprec : (Z.pos (digits2_pos m) <= prec)%Z). { diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index a7170c8e18..faf53d3fad 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -906,7 +906,7 @@ let print_name env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> print_any_name env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> @@ -960,7 +960,7 @@ let print_about env sigma na udecl = match na with | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> print_about_any ?loc env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true) ntn sc)) udecl | {loc;v=Constrexpr.AN ref} -> print_about_any ?loc env sigma (locate_any_name ref) udecl diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index aac0b54ed4..b8dce9ed44 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1779,7 +1779,7 @@ let interp_search_about_item env sigma = try let ref = Notation.interp_notation_as_global_reference - (fun _ -> true) s sc in + ~head:false (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> user_err ~hdr:"interp_search_about_item" -- cgit v1.2.3 From 2e53445be16ef28058599fed3f06424db17f6943 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 9 May 2020 15:52:47 +0200 Subject: Add test for #11727, which was indirectly fixed by this PR. --- test-suite/bugs/closed/bug_11727.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 test-suite/bugs/closed/bug_11727.v diff --git a/test-suite/bugs/closed/bug_11727.v b/test-suite/bugs/closed/bug_11727.v new file mode 100644 index 0000000000..d346f05c10 --- /dev/null +++ b/test-suite/bugs/closed/bug_11727.v @@ -0,0 +1,8 @@ +Tactic Notation "myunfold" reference(x) := unfold x. +Notation idnat := (@id nat). +Goal let n := 0 in idnat n = 0. +Proof. + intro n. + myunfold idnat. + myunfold n. +Abort. -- cgit v1.2.3 From 5e1da5b05860750606f32063a221d6023cabf5dc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 9 May 2020 15:56:55 +0200 Subject: Tweak the error message of reference internalization. --- plugins/ltac/tacintern.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index fcedbe8e2e..53dc518bd3 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -302,8 +302,14 @@ let evalref_of_globref ?loc ?short = function | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) | r -> - user_err ?loc (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ - spc () ++ str "to an evaluable reference.") + let tpe = match r with + | GlobRef.IndRef _ -> "inductive" + | GlobRef.ConstructRef _ -> "constructor" + | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false + in + user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++ + Nametab.pr_global_env Id.Set.empty r ++ spc () ++ + str "into an evaluable reference.") let intern_evaluable ist = function | {v=AN qid} -> -- cgit v1.2.3 From ec14db89d7fd580904cfa14665c16e877924b8cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2020 10:17:27 +0200 Subject: Remove an outdated piece of documentation about limitations of unfold. --- doc/sphinx/proof-engine/tactics.rst | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 127e4c6dbe..ad799fbbcd 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3393,17 +3393,6 @@ the conversion in hypotheses :n:`{+ @ident}`. never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to ensure that unfolding does not fail. - .. note:: - - This tactic unfortunately does not yet play well with tactic - internalization, resulting in interpretation-time errors when - you try to use it directly with opaque identifiers, as seen in - the first (failing) use of :tacn:`with_strategy` in the - following example. This can be worked around by binding the - identifier to an |Ltac| variable, and this issue should - disappear in a future version of |Coq|; see `#12179 - `_. - .. example:: .. coqtop:: all reset abort @@ -3411,8 +3400,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Opaque id. Goal id 10 = 10. Fail unfold id. - Fail with_strategy transparent [id] unfold id. - let id' := id in with_strategy transparent [id] unfold id'. + with_strategy transparent [id] unfold id. .. warning:: -- cgit v1.2.3 From b5ecd2e46202f47cfccf305e449bcdd8a6a14a0f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 May 2020 12:37:12 +0200 Subject: Adding changelog. --- doc/changelog/04-tactics/12256-unfold-dyn-check.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/04-tactics/12256-unfold-dyn-check.rst diff --git a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst new file mode 100644 index 0000000000..c2f7065f4c --- /dev/null +++ b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst @@ -0,0 +1,4 @@ +- **Changed:** + The check that unfold arguments were indeed unfoldable has been moved to runtime + (`#12256 `_, + by Pierre-Marie Pédrot). -- cgit v1.2.3