diff options
| -rw-r--r-- | dev/ci/user-overlays/11368-trailing-implicit-error.sh | 33 | ||||
| -rw-r--r-- | doc/changelog/02-specification-language/11368-trailing_implicit_error.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 4 | ||||
| -rw-r--r-- | interp/impargs.ml | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_2729.v | 2 | ||||
| -rw-r--r-- | test-suite/complexity/injection.v | 2 | ||||
| -rw-r--r-- | test-suite/prerequisite/ssr_mini_mathcomp.v | 6 | ||||
| -rw-r--r-- | test-suite/success/Inductive.v | 2 | ||||
| -rw-r--r-- | test-suite/success/Inversion.v | 2 | ||||
| -rw-r--r-- | test-suite/success/RecTutorial.v | 4 |
10 files changed, 53 insertions, 16 deletions
diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh new file mode 100644 index 0000000000..a125337dd9 --- /dev/null +++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh @@ -0,0 +1,33 @@ +if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then + + mathcomp_CI_REF=non_maximal_implicit + mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp + + oddorder_CI_REF=non_maximal_implicit + oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order + + stdlib2_CI_REF=non_maximal_implicit + stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2 + + coq_dpdgraph_CI_REF=non_maximal_implicit + coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph + + vst_CI_REF=non_maximal_implicit + vst_CI_GITURL=https://github.com/SimonBoulier/VST + + equations_CI_REF=non_maximal_implicit + equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations + + mtac2_CI_REF=non_maximal_implicit + mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2 + + relation_algebra_CI_REF=non_maximal_implicit + relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra + + fiat_parsers_CI_REF=non_maximal_implicit + fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat + + Corn_CI_REF=non_maximal_implicit + Corn_CI_GITURL=https://github.com/SimonBoulier/corn + +fi diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst new file mode 100644 index 0000000000..a7ffde31fc --- /dev/null +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -0,0 +1,6 @@ +- **Changed:** + The warning raised when a trailing implicit is declared to be non maximally + inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error. + This was deprecated since Coq 8.10. + (`#11368 <https://github.com/coq/coq/pull/11368>`_, + by SimonBoulier). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index bdfdffeaad..510e271951 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1728,11 +1728,11 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. warn:: Argument number @num is a trailing implicit so must be maximal. +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance in - .. coqtop:: all warn + .. coqtop:: all fail Arguments prod _ [_]. diff --git a/interp/impargs.ml b/interp/impargs.ml index df28b32f81..e2c732809a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -646,11 +646,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l -(* TODO: either turn these warnings on and document them, or handle these cases sensibly *) -let warn_set_maximal_deprecated = - CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated" - (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal")) +let msg_trailing_implicit id = + user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].")) type implicit_kind = Implicit | MaximallyImplicit | NotImplicit @@ -662,7 +660,7 @@ let compute_implicit_statuses autoimps l = | Name id :: autoimps, Implicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality imps' false in - if max then warn_set_maximal_deprecated i; + if max then msg_trailing_implicit id; Some (ExplByName id, Manual, (max, true)) :: imps' | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> user_err ~hdr:"set_implicits" diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v index ff08bdc6bb..52cc34beb3 100644 --- a/test-suite/bugs/closed/bug_2729.v +++ b/test-suite/bugs/closed/bug_2729.v @@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Arguments Nil [pu cxt]. +Arguments Nil {pu cxt}. Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 298a07c1c4..7022987096 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Arguments ADMIT [p]. +Arguments ADMIT {p}. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index d293dc0533..048fb3b027 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -65,7 +65,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Arguments eqP [T x y]. +Arguments eqP {T x y}. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -345,7 +345,7 @@ Proof. by []. Qed. End SubEqType. -Arguments val_eqP [T P sT x y]. +Arguments val_eqP {T P sT x y}. Prenex Implicits val_eqP. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) @@ -386,7 +386,7 @@ Qed. Canonical nat_eqMixin := EqMixin eqnP. Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. -Arguments eqnP [x y]. +Arguments eqnP {x y}. Prenex Implicits eqnP. Coercion nat_of_bool (b : bool) := if b then 1 else 0. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index d17b266690..4b2d4457bf 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Arguments LNil [A]. +Arguments LNil {A}. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 1dbeaf3e1f..8297f54641 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Arguments NL [I]. +Arguments NL {I}. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 4fac798f76..15672eab7c 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -994,7 +994,7 @@ Qed. Arguments Vector.cons [A] _ [n]. -Arguments Vector.nil [A]. +Arguments Vector.nil {A}. Arguments Vector.hd [A n]. Arguments Vector.tl [A n]. @@ -1161,7 +1161,7 @@ infiniteproof map_iterate'. Qed. -Arguments LNil [A]. +Arguments LNil {A}. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). |