From 140b6f096d8fa528ab252f0189880f44099e2521 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 14 Apr 2026 16:50:40 +0200 Subject: [PATCH 1/3] Have implicit arguments with "Asymmetric Patterns" Add a flag "Asymmetric Patterns No Implicits" (false by default) that can be set to true to retrieve the previous behavior of "Asymmetric Patterns" (needed for backward compat). --- ...ymmetric-patterns-no-implicits-Changed.rst | 8 +++++++ doc/sphinx/language/extensions/match.rst | 9 ++++++++ interp/constrintern.ml | 9 +++++++- interp/constrintern.mli | 2 ++ test-suite/bugs/bug_11576.v | 7 +++--- test-suite/bugs/bug_3045.v | 4 ++-- test-suite/bugs/bug_3262.v | 4 ++-- test-suite/bugs/bug_3732.v | 4 ++-- test-suite/bugs/bug_4001.v | 2 +- test-suite/bugs/bug_7916.v | 2 +- test-suite/output/Cases.out | 17 ++++++++------ test-suite/output/Cases.v | 6 ++--- test-suite/prerequisite/ssr_mini_mathcomp.v | 22 +++++++++---------- test-suite/success/Case22.v | 2 +- theories/Corelib/Compat/Rocq92.v | 2 ++ 15 files changed, 65 insertions(+), 35 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst diff --git a/doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst b/doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst new file mode 100644 index 000000000000..8b145881bd07 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst @@ -0,0 +1,8 @@ +- **Changed:** + the bahavior of the :flag:`Asymmetric Patterns` flag, which no + longer disactivates implicit arguments in patterns. Set the + compatibility flag :flag:`Asymmetric Patterns No Implicits` to + retrieve the previous behavior + (`#21947 `_, + fixes `#21769 `_, + by Pierre Roux). diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index fb44d8cfa6c9..8269a5b1d6b6 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -664,6 +664,15 @@ When we use parameters in patterns there is an error message: end). Unset Asymmetric Patterns. +.. flag:: Asymmetric Patterns No Implicits + + This compatibility :term:`flag` (off by default) disactivates + implicit arguments in patterns when :flag:`Asymmetric Patterns` is + on, thus recovering the behavior of :flag:`Asymmetric Patterns` + before Rocq 9.3. + + .. deprecated:: 9.3 + Implicit arguments in patterns ------------------------------ diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 35ff54ca4669..e1c324f62ee1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1776,6 +1776,13 @@ let { Goptions.get = get_asymmetric_patterns } = ~value:false () +let { Goptions.get = get_asymmetric_patterns_no_implicits } = + Goptions.declare_bool_option_and_ref + ~depr:(Deprecation.make ~since:"9.3" ()) + ~key:["Asymmetric";"Patterns";"No";"Implicits"] + ~value:false + () + type global_reference_test = { for_ind : bool; test_kind : ?loc:Loc.t -> GlobRef.t -> unit @@ -1853,7 +1860,7 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = let loc = pt.loc in (* The two policies implied by asymmetric pattern mode *) let add_par_if_no_ntn_with_par = get_asymmetric_patterns () && not for_ind in - let no_impl = get_asymmetric_patterns () && not for_ind in + let no_impl = get_asymmetric_patterns_no_implicits () && get_asymmetric_patterns () && not for_ind in match pt.v with | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id) | CPatRecord l -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index c53597e3a9f7..3cbf381ca920 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -251,6 +251,8 @@ val parsing_explicit : bool ref (** Placeholder for global option, should be moved to a parameter *) val get_asymmetric_patterns : unit -> bool +val get_asymmetric_patterns_no_implicits : unit -> bool + val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit (** Check that a list of record field definitions doesn't contain duplicates. *) diff --git a/test-suite/bugs/bug_11576.v b/test-suite/bugs/bug_11576.v index b534bfda679f..5fcba06f0414 100644 --- a/test-suite/bugs/bug_11576.v +++ b/test-suite/bugs/bug_11576.v @@ -25,12 +25,11 @@ Existing Class rep. Fixpoint translate_func' (pv:=_) {t} (e : @expr ltype t) : for_each_lhs_of_arrow ltype t -> @cmd pv := match e with - | Abs base d f => - fun (args : _ * for_each_lhs_of_arrow _ d) => + | Abs f => + fun (args : _ * for_each_lhs_of_arrow _ _) => translate_func' (f (fst args)) (snd args) - | Var base v => + | Var v => fun _ => translate_cmd (Var v) - | _ => fun _ => admit end. (* Used to be: File "./bug_01.v", line 30, characters 30-31: Error: Cannot infer this placeholder of type "parameters" (no type class diff --git a/test-suite/bugs/bug_3045.v b/test-suite/bugs/bug_3045.v index 90aa5ee9fd25..5c6f1ba55b7d 100644 --- a/test-suite/bugs/bug_3045.v +++ b/test-suite/bugs/bug_3045.v @@ -19,14 +19,14 @@ Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C - Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d := match m in @ReifiedMorphism objC C s d return Morphism C s d with - | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1) + | ReifiedComposedMorphism m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1) (@ReifiedMorphismDenote _ _ _ _ m2) end. Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d) : { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }. refine match m with - | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _ + | ReifiedComposedMorphism m1 m2 => _ end; clear m. (* This fails with an error rather than an anomaly, but morally it should work, if destruct were able to do the good generalization diff --git a/test-suite/bugs/bug_3262.v b/test-suite/bugs/bug_3262.v index 64d3388f284c..01b2d5457498 100644 --- a/test-suite/bugs/bug_3262.v +++ b/test-suite/bugs/bug_3262.v @@ -21,7 +21,7 @@ Section hlist. | l :: _ => F l end with | Hnil => tt - | Hcons _ _ x _ => x + | Hcons x _ => x end. Definition hlist_tl {a b} (hl : hlist (a :: b)) : hlist b := @@ -30,7 +30,7 @@ Section hlist. | _ :: ls => hlist ls end with | Hnil => tt - | Hcons _ _ _ x => x + | Hcons _ x => x end. Lemma hlist_eta : forall ls (h : hlist ls), diff --git a/test-suite/bugs/bug_3732.v b/test-suite/bugs/bug_3732.v index 76035606ba79..e851bd18a148 100644 --- a/test-suite/bugs/bug_3732.v +++ b/test-suite/bugs/bug_3732.v @@ -34,8 +34,8 @@ Section machine. Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) := match p with - | Inj _ P => fun _ => Inj P - | ExistsX G A p1 => fun p' => + | Inj P => fun _ => Inj P + | @ExistsX G A p1 => fun p' => match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with | nil => fun p1 _ => ExistsX p1 | cons _ _ => fun _ rc => ExistsX rc diff --git a/test-suite/bugs/bug_4001.v b/test-suite/bugs/bug_4001.v index ed05f0d41e4c..775c8c8dad5f 100644 --- a/test-suite/bugs/bug_4001.v +++ b/test-suite/bugs/bug_4001.v @@ -14,5 +14,5 @@ Inductive t : list A -> Type := Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x := match s in t l' with | snil => False - | scons _ e _ _ => e + | scons e _ => e end. diff --git a/test-suite/bugs/bug_7916.v b/test-suite/bugs/bug_7916.v index 53861dc303a4..d3bb1ed0cf9f 100644 --- a/test-suite/bugs/bug_7916.v +++ b/test-suite/bugs/bug_7916.v @@ -53,7 +53,7 @@ Module MathComp. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). - Definition class := let: Pack _ c := cT return class_of cT in c. + Definition class := let: Pack c := cT return class_of cT in c. End ClassDef. Coercion sort : type >-> Sortclass. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 226918e1e256..edeb75224723 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -231,15 +231,18 @@ File "./output/Cases.v", line 279, characters 33-39: The command has indeed failed with message: The constructor cons (in type list) is expected to be applied to 2 arguments while it is actually applied to 1 argument. -File "./output/Cases.v", line 281, characters 33-39: -The command has indeed failed with message: -The constructor D' (in type J') is expected to be applied to 3 arguments (or -4 arguments when including variables for local definitions) while it is -actually applied to 2 arguments. +fun x : J' ?T ?p => match x with + | @D' _ _ _ _ _ _ _ _ => 0 + end + : J' ?T ?p -> nat +where +?T : [x : J' ?T ?p |- Type] (x cannot be used) +?T0 : [x : J' ?T ?p |- Type] (x cannot be used) +?p : [x : J' ?T ?p |- (?T * ?T0)%type] (x cannot be used) File "./output/Cases.v", line 282, characters 33-45: The command has indeed failed with message: -The constructor D' (in type J') is expected to be applied to 3 arguments (or -4 arguments when including variables for local definitions) while it is +The constructor D' (in type J') is expected to be applied to 2 arguments (or +3 arguments when including variables for local definitions) while it is actually applied to 5 arguments. fun x : J' bool (true, true) => match x with diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 8cca5ef8909f..e59e4f23553e 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -278,10 +278,10 @@ Fail Check fun x => match x with (y,z) w => y+z+w end. Fail Check fun x => match x with cons y z w => 0 | nil => 0 end. Fail Check fun x => match x with cons y => 0 | nil => 0 end. -Fail Check fun x => match x with D' n _ => 0 end. +Check fun x => match x with D' n _ => 0 end. Fail Check fun x => match x with D' n m p e _ => 0 end. -Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end. -Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end. +Check fun x : J' bool (true,true) => match x with D' n e => existT (fun x => eq x x) _ e end. +Check fun x : J' bool (true,true) => match x with D' n p e => (n,p) end. End ConstructorArgumentsNumber. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index 78a41c2501ef..e25aa27b6745 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -35,7 +35,7 @@ Structure type := Pack {sort; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ := cT return class_of cT in c. +Definition class := let: Pack c _ := cT return class_of cT in c. Definition pack c := @Pack T c T. Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c. @@ -694,9 +694,9 @@ Local Coercion base : class_of >-> Equality.class_of. Structure type := Pack {sort; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition class := let: Pack c _ as cT' := cT return class_of cT' in c. Definition clone c & phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Let xT := let: @Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). Definition pack m := @@ -797,9 +797,9 @@ Local Coercion base : class_of >-> Choice.class_of. Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition class := let: Pack c _ as cT' := cT return class_of cT' in c. Definition clone c & phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Let xT := let: @Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). Definition pack m := @@ -881,7 +881,7 @@ Structure subCountType : Type := SubCountType {subCount_sort :> subType P; _ : mixin_of subCount_sort}. Coercion sub_countType (sT : subCountType) := - Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id. + Eval hnf in pack (let: SubCountType m := sT return mixin_of sT in m) id. Canonical sub_countType. Definition pack_subCountType U := @@ -925,7 +925,7 @@ Section Mixins. Variable T : countType. Definition EnumMixin := - let: Countable.Pack _ (Countable.Class _ m) _ as cT := T + let: Countable.Pack (Countable.Class _ m) _ as cT := T return forall e : seq cT, axiom e -> mixin_of cT in @Mixin (EqType _ _) m. @@ -947,9 +947,9 @@ Local Coercion base : class_of >-> Choice.class_of. Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition class := let: Pack c _ as cT' := cT return class_of cT' in c. Definition clone c & phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Let xT := let: @Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (EqType T b0)) := @@ -1016,7 +1016,7 @@ Definition pack_subFinType U := Implicit Type sT : subFinType. Definition subFin_mixin sT := - let: SubFinType _ m := sT return mixin_of (sub_eqType sT) in m. + let: SubFinType m := sT return mixin_of (sub_eqType sT) in m. Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT). Canonical subFinType_subCountType. @@ -1047,7 +1047,7 @@ Variable n : nat. Inductive ordinal : predArgType := Ordinal m of m < n. -Coercion nat_of_ord i := let: Ordinal m _ := i in m. +Coercion nat_of_ord i := let: @Ordinal m _ := i in m. Canonical ordinal_subType := [subType for nat_of_ord]. Definition ordinal_eqMixin := Eval hnf in [eqMixin of ordinal by <:]. diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index 90c1b308f2b6..5ccd46f6507f 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -100,5 +100,5 @@ Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end. Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a. Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end. Set Asymmetric Patterns. -Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end. +Check fun (x:expr true) => match x in expr n return n=n with intro a _ => eq_refl a end. Unset Asymmetric Patterns. diff --git a/theories/Corelib/Compat/Rocq92.v b/theories/Corelib/Compat/Rocq92.v index 377a995a6e0b..bf6541048caf 100644 --- a/theories/Corelib/Compat/Rocq92.v +++ b/theories/Corelib/Compat/Rocq92.v @@ -16,3 +16,5 @@ #[export] Set Warnings "-deprecated-since-9.3". #[export] Set Inline Abstract Subproof. + +#[export] Set Asymmetric Patterns No Implicits. From 91955da8ea1b9b42be06333ee3accf045632b3a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 14 Apr 2026 16:54:52 +0200 Subject: [PATCH 2/3] Improve pattern externalization with Asymettric Patterns --- interp/constrextern.ml | 21 +++++++++++++-------- test-suite/output/Cases.out | 4 ++-- test-suite/output/PrintMatch.out | 2 +- 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9668ef64bb96..397eb9bbe440 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -307,18 +307,23 @@ let rec extern_cases_pattern_in_scope ~flags ((custom,(lev_after:int option)),sc | Some l -> CPatRecord l | None -> let c = extern_reference vars (GlobRef.ConstructRef cstrsp) in - if Constrintern.get_asymmetric_patterns () then - if pattern_printable_in_both_syntax ~flags cstrsp - then CPatCstr (c, None, args) - else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) - else - let full_args = add_patt_for_params (fst cstrsp) args in + let full_args = add_patt_for_params (fst cstrsp) args in + let drop n = let tags = try Inductiveops.constructor_alltags (Global.env()) cstrsp with _ when !Flags.in_debugger -> [] in - match drop_implicits_in_patt ~flags (GlobRef.ConstructRef cstrsp) 0 ~tags full_args with + let tags = List.skipn_at_best n tags in + let args = List.skipn_at_best n full_args in + match drop_implicits_in_patt ~flags (GlobRef.ConstructRef cstrsp) n ~tags args with | Some true_args -> CPatCstr (c, None, true_args) - | None -> CPatCstr (c, Some full_args, []) + | None -> CPatCstr (c, Some full_args, []) in + if Constrintern.get_asymmetric_patterns () then + if pattern_printable_in_both_syntax ~flags cstrsp + then CPatCstr (c, None, args) + else if Constrintern.get_asymmetric_patterns_no_implicits () + then CPatCstr (c, Some full_args, []) + else drop (Inductiveops.inductive_nparamdecls (Global.env()) (fst cstrsp)) + else drop 0 in insert_pat_alias ?loc (CAst.make ?loc p) na in diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index edeb75224723..583f8f8546ba 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -232,7 +232,7 @@ The command has indeed failed with message: The constructor cons (in type list) is expected to be applied to 2 arguments while it is actually applied to 1 argument. fun x : J' ?T ?p => match x with - | @D' _ _ _ _ _ _ _ _ => 0 + | D' _ _ _ => 0 end : J' ?T ?p -> nat where @@ -246,7 +246,7 @@ The constructor D' (in type J') is expected to be applied to 2 arguments (or actually applied to 5 arguments. fun x : J' bool (true, true) => match x with -| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e +| D' m _ e => existT (fun x0 : nat => x0 = x0) m e end : J' bool (true, true) -> {x : nat & x = x} fun x : J' bool (true, true) => diff --git a/test-suite/output/PrintMatch.out b/test-suite/output/PrintMatch.out index 84400087400e..21edf10e2e76 100644 --- a/test-suite/output/PrintMatch.out +++ b/test-suite/output/PrintMatch.out @@ -41,7 +41,7 @@ Arguments eq_sym [A]%_type_scope [x y] H eq_sym = fun (A : Type) (x y : A) (H : x = y) => match H in _ = y0 return y0 = x with -| @eq_refl _ _ => @eq_refl A x +| eq_refl => @eq_refl A x end : forall [A : Type] [x y : A], x = y -> y = x From fd3b165818f026fd5847e9403940cae9acb56234 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Apr 2026 12:50:40 +0200 Subject: [PATCH 3/3] Add overlays --- ...47-proux01-asymmetric-patterns-no-implicits.sh | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 dev/ci/user-overlays/21947-proux01-asymmetric-patterns-no-implicits.sh diff --git a/dev/ci/user-overlays/21947-proux01-asymmetric-patterns-no-implicits.sh b/dev/ci/user-overlays/21947-proux01-asymmetric-patterns-no-implicits.sh new file mode 100644 index 000000000000..247a03d3a511 --- /dev/null +++ b/dev/ci/user-overlays/21947-proux01-asymmetric-patterns-no-implicits.sh @@ -0,0 +1,15 @@ +overlay aac_tactics https://github.com/rocq-community/aac-tactics rocq21947 21947 +overlay atbr https://github.com/rocq-community/atbr rocq21947 21947 +overlay ext_lib https://github.com/coq-community/coq-ext-lib rocq21947 21947 +overlay equations https://github.com/proux01/Coq-Equations rocq21947 21947 +overlay fiat_crypto https://github.com/proux01/fiat-crypto rocq21947 21947 +overlay fiat_crypto_legacy https://github.com/proux01/fiat-crypto rocq21947-legacy 21947 +overlay fiat_parsers https://github.com/proux01/fiat rocq21947 21947 +overlay hott https://github.com/proux01/HoTT rocq21947 21947 +overlay kami https://github.com/proux01/kami rocq21947 21947 +overlay mathcomp https://github.com/proux01/math-comp rocq21947 21947 +overlay metarocq https://github.com/proux01/metarocq rocq21947 21947 +overlay relation_algebra https://github.com/proux01/relation-algebra rocq21947 21947 +overlay rewriter https://github.com/proux01/rewriter rocq21947 21947 +overlay stdlib https://github.com/proux01/stdlib rocq21947 21947 +overlay vst https://github.com/proux01/vst rocq21947 21947