diff options
44 files changed, 69 insertions, 130 deletions
@@ -6,6 +6,11 @@ Tools - Coq_makefile lets one override or extend the following variables from the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS. +Vernacular Commands + +- Removed deprecated commands Arguments Scope and Implicit Arguments + (not the option). Use the Arguments command instead. + Changes from 8.7.2 to 8.8+beta1 =============================== diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index dc1110ad8..96b4a0e26 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -409,8 +409,6 @@ type nonrec vernac_expr = | VernacHints of string list * hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacDeclareImplicits of reference or_by_notation * - (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * @@ -418,8 +416,6 @@ type nonrec vernac_expr = [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list - | VernacArgumentsScope of reference or_by_notation * - scope_name option list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8543d2b84..7114e6c58 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -601,14 +601,6 @@ GEXTEND Gram ; END -let warn_deprecated_arguments_scope = - CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" - (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") - -let warn_deprecated_implicit_arguments = - CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" - (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") - (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name hint_info; @@ -691,20 +683,6 @@ GEXTEND Gram let more_implicits = Option.default [] more_implicits in VernacArguments (qid, args, more_implicits, !slash_position, mods) - - (* moved there so that camlp5 factors it with the previous rule *) - | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - warn_deprecated_arguments_scope ~loc:!@loc (); - VernacArgumentsScope (qid,scl) - - (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> - List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - warn_deprecated_implicit_arguments ~loc:!@loc (); - VernacDeclareImplicits (qid,pos) - | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl @@ -734,12 +712,6 @@ GEXTEND Gram [`ClearImplicits; `ClearScopes] ] ] ; - implicit_name: - [ [ "!"; id = ident -> (id, false, true) - | id = ident -> (id,false,false) - | "["; "!"; id = ident; "]" -> (id,true,true) - | "["; id = ident; "]" -> (id,true, false) ] ] - ; scope: [ [ "%"; key = IDENT -> key ] ] ; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7df0a0c94..2706893ac 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -155,13 +155,6 @@ open Decl_kinds let pr_locality local = if local then keyword "Local" else keyword "Global" - let pr_explanation (e,b,f) = - let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") - | ExplByName id -> pr_id id in - let a = if f then str"!" ++ a else a in - if b then str "[" ++ a ++ str "]" else a - let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s @@ -653,16 +646,6 @@ open Decl_kinds keyword "Bind Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll ) - | VernacArgumentsScope (q,scl) -> - let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc - in - return ( - keyword "Arguments Scope" - ++ spc() ++ pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - ) | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " @@ -1016,18 +999,6 @@ open Decl_kinds | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacDeclareImplicits (q,[]) -> - return ( - hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) - ) - | VernacDeclareImplicits (q,impls) -> - return ( - hov 1 (keyword "Implicit Arguments" ++ spc () ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - ) | VernacArguments (q, args, more_implicits, nargs, mods) -> return ( hov 2 ( diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 9a8af3a58..4efe1f7ba 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -145,7 +145,7 @@ let classify_vernac e = | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacArguments _ | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v index 8c5a38859..79a0a14d7 100644 --- a/test-suite/bugs/closed/1341.v +++ b/test-suite/bugs/closed/1341.v @@ -8,7 +8,7 @@ Hypothesis Xst : forall A, Equivalence (Xeq A). Variable map : forall A B, (A -> B) -> X A -> X B. -Implicit Arguments map [A B]. +Arguments map [A B]. Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c). intros A B a b c f Hab Hbc. diff --git a/test-suite/bugs/closed/1844.v b/test-suite/bugs/closed/1844.v index 17eeb3529..c41e45900 100644 --- a/test-suite/bugs/closed/1844.v +++ b/test-suite/bugs/closed/1844.v @@ -5,7 +5,7 @@ Definition zeq := Z.eq_dec. Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := fun y => if zeq x y then v else s y. -Implicit Arguments update [A]. +Arguments update [A]. Definition ident := Z. Parameter operator: Set. diff --git a/test-suite/bugs/closed/1891.v b/test-suite/bugs/closed/1891.v index 685811176..5024a5bc9 100644 --- a/test-suite/bugs/closed/1891.v +++ b/test-suite/bugs/closed/1891.v @@ -3,7 +3,7 @@ Definition f (A: Set) (l: T A): unit := tt. - Implicit Arguments f [A]. + Arguments f [A]. Lemma L (x: T unit): (unit -> T unit) -> unit. Proof. diff --git a/test-suite/bugs/closed/1951.v b/test-suite/bugs/closed/1951.v index 7558b0b86..e950554c4 100644 --- a/test-suite/bugs/closed/1951.v +++ b/test-suite/bugs/closed/1951.v @@ -42,7 +42,7 @@ match s as a return (S a) with pair (ind2 a0) IHl) l) end. (* some induction principle *) -Implicit Arguments ind [S]. +Arguments ind [S]. Lemma k : a -> Type. (* some ininteresting lemma *) intro;pattern H;apply ind;intros. diff --git a/test-suite/bugs/closed/1981.v b/test-suite/bugs/closed/1981.v index 99952682d..a3d942930 100644 --- a/test-suite/bugs/closed/1981.v +++ b/test-suite/bugs/closed/1981.v @@ -1,4 +1,4 @@ -Implicit Arguments ex_intro [A]. +Arguments ex_intro [A]. Goal exists n : nat, True. eapply ex_intro. exact 0. exact I. diff --git a/test-suite/bugs/closed/2362.v b/test-suite/bugs/closed/2362.v index febb9c7bb..10e86cd12 100644 --- a/test-suite/bugs/closed/2362.v +++ b/test-suite/bugs/closed/2362.v @@ -8,7 +8,7 @@ Class Pointed (M:Type -> Type) := Unset Implicit Arguments. Inductive FPair (A B:Type) (neutral: B) : Type:= fpair : forall (a:A) (b:B), FPair A B neutral. -Implicit Arguments fpair [[A] [B] [neutral]]. +Arguments fpair {A B neutral}. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 23a58501f..6d73d58d4 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -63,7 +63,7 @@ Fixpoint lpSat st f: Prop := end. End PropLogic. -Implicit Arguments lpSat. +Arguments lpSat : default implicits. Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := match f with @@ -71,7 +71,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) end. -Implicit Arguments LPTransfo. +Arguments LPTransfo : default implicits. Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f. @@ -139,7 +139,7 @@ Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) := fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)). -Implicit Arguments trProd. +Arguments trProd : default implicits. Require Import Setoid. Theorem satTrProd: diff --git a/test-suite/bugs/closed/2404.v b/test-suite/bugs/closed/2404.v index 8ac696e91..f6ec67601 100644 --- a/test-suite/bugs/closed/2404.v +++ b/test-suite/bugs/closed/2404.v @@ -22,13 +22,13 @@ Section Derived. Definition bexportw := exportw base. Definition bwweak := wweak base. - Implicit Arguments bexportw [a b]. + Arguments bexportw [a b]. Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type := starReflS : forall a, RstarSetProof T a a | starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k. -Implicit Arguments starTransS [I T i j k]. +Arguments starTransS [I T i j k]. Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))). diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v index ef2e4e355..b5a723b47 100644 --- a/test-suite/bugs/closed/2584.v +++ b/test-suite/bugs/closed/2584.v @@ -8,7 +8,7 @@ Inductive res (A: Type) : Type := | OK: A -> res A | Error: err -> res A. -Implicit Arguments Error [A]. +Arguments Error [A]. Set Printing Universes. diff --git a/test-suite/bugs/closed/2667.v b/test-suite/bugs/closed/2667.v index 0631e5358..0e6d0108c 100644 --- a/test-suite/bugs/closed/2667.v +++ b/test-suite/bugs/closed/2667.v @@ -1,11 +1,11 @@ -(* Check that extra arguments to Arguments Scope do not disturb use of *) +(* Check that extra arguments to Arguments do not disturb use of *) (* scopes in constructors *) Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt. Bind Scope Cminor with stmt. (* extra argument is ok because of possible coercion to funclass *) -Arguments Scope Scall [_ Cminor ]. +Arguments Scall _ _%Cminor : extra scopes. (* extra argument is ok because of possible coercion to funclass *) Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end. diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v index 7929b8810..c9d65c12c 100644 --- a/test-suite/bugs/closed/2729.v +++ b/test-suite/bugs/closed/2729.v @@ -82,8 +82,8 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Implicit Arguments Nil [pu cxt]. -Implicit Arguments Cons [pu from mid to]. +Arguments Nil [pu cxt]. +Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} {from mid to : NameSet} diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index bb607b785..07a5cf91a 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -49,9 +49,9 @@ Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) := ; af_level2 : forall x y, age1 x = Some y -> level x = S (level y) }. -Implicit Arguments af_unage [[A] [level] [age1]]. -Implicit Arguments af_level1 [[A] [level] [age1]]. -Implicit Arguments af_level2 [[A] [level] [age1]]. +Arguments af_unage {A level age1}. +Arguments af_level1 {A level age1}. +Arguments af_level2 {A level age1}. Class ageable (A:Type) := mkAgeable { level : A -> nat @@ -77,7 +77,7 @@ Coercion app_pred : pred >-> Funclass. Global Opaque pred. Definition derives {A} `{ageable A} (P Q:pred A) := forall a:A, P a -> Q a. -Implicit Arguments derives. +Arguments derives : default implicits. Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A := fun a:A => P a /\ Q a. @@ -170,7 +170,7 @@ Class Functor `(C:Category) `(D:Category) (im : C -> D) := { fmap g ∘ fmap f ≈ fmap (g ∘ f) }. Coercion functor_im : Functor >-> Funclass. -Implicit Arguments fmap [Object Hom C Object0 Hom0 D im a b]. +Arguments fmap [Object Hom C Object0 Hom0 D im] _ [a b]. Add Parametric Morphism `(C:Category) `(D:Category) (Im:C->D) (F:Functor C D Im) (a b:C) : (@fmap _ _ C _ _ D Im F a b) diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index 79671ce93..9811733dc 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -33,7 +33,7 @@ Section Counted_list. End Counted_list. -Implicit Arguments counted_def_nth [A n]. +Arguments counted_def_nth [A n]. Section Finite_nat_set. diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 1f0f3b0da..a1d0b9107 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -21,7 +21,7 @@ Section ILogic_Fun. Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. +Arguments ILFunFrm _ {e} _ {ILOps}. Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; ltrue := True; land P Q := P /\ Q; diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v index f5a22bd50..e91c004c7 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -26,7 +26,7 @@ Record morphism T T' `{e : type T} `{e' : type T'} := mkMorph { morph :> T -> T'; morph_resp : setoid_resp morph}. -Implicit Arguments mkMorph [T T' e e0 e' e1]. +Arguments mkMorph [T T' e0 e e1 e']. Infix "-s>" := morphism (at level 45, right associativity). Section Morphisms. Context {S T U V} `{eS : type S} `{eT : type T} `{eU : type U} `{eV : type V}. @@ -334,8 +334,8 @@ Section ILogic_Fun. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. -Implicit Arguments mkILFunFrm [T Frm ILOps]. +Arguments ILFunFrm _ {e} _ {ILOps}. +Arguments mkILFunFrm [T] _ [Frm ILOps]. Program Definition ILFun_eq {T R} {ILOps: ILogicOps R} {ILogic: ILogic R} (P : T -> R) : @ILFunFrm T _ R ILOps := diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v index 09f1149c2..13d62b8ff 100644 --- a/test-suite/bugs/closed/3732.v +++ b/test-suite/bugs/closed/3732.v @@ -16,7 +16,7 @@ Section machine. | Inj : forall G, Prop -> propX G | ExistsX : forall G A, propX (A :: G) -> propX G. - Implicit Arguments Inj [G]. + Arguments Inj [G]. Definition PropX := propX nil. Fixpoint last (G : list Type) : Type. diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index 8d7dfbd49..bc9380f90 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -23,7 +23,7 @@ Section ILogic_Fun. Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. +Arguments ILFunFrm _ {e} _ {ILOps}. Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; ltrue := True; land P Q := P /\ Q; diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v index c5bf3289b..da4e53aab 100644 --- a/test-suite/bugs/closed/4865.v +++ b/test-suite/bugs/closed/4865.v @@ -48,5 +48,5 @@ Fail Check g 0 0 1. (* 2nd 0 in bool *) Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. Notation "0" := true. -Arguments Scope lam [nat_scope nat_scope]. +Arguments lam _%nat_scope _%nat_scope : extra scopes. Check (lam 1 0). diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v index 6cca5c9fb..5294adefd 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/opened/2456.v @@ -6,7 +6,7 @@ Parameter Patch : nat -> nat -> Set. Inductive Catch (from to : nat) : Type := MkCatch : forall (p : Patch from to), Catch from to. -Implicit Arguments MkCatch [from to]. +Arguments MkCatch [from to]. Inductive CatchCommute5 : forall {from mid1 mid2 to : nat}, diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v index 2a156e333..c09649de7 100644 --- a/test-suite/bugs/opened/3295.v +++ b/test-suite/bugs/opened/3295.v @@ -5,7 +5,7 @@ Class lops := lmk_ops { weq: relation car }. -Implicit Arguments car []. +Arguments car : clear implicits. Coercion car: lops >-> Sortclass. @@ -23,7 +23,7 @@ Class ops := mk_ops { dot: forall n m p, mor n m -> mor m p -> mor n p }. Coercion mor: ops >-> Funclass. -Implicit Arguments ob []. +Arguments ob : clear implicits. Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). Proof. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 08f489d75..a76fa19d3 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. -Implicit Arguments ADMIT [p]. +Arguments ADMIT [p]. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v index a148ebe8e..0ef4b417a 100644 --- a/test-suite/failure/check.v +++ b/test-suite/failure/check.v @@ -1,3 +1,3 @@ -Implicit Arguments eq [A]. +Arguments eq [A]. Fail Check (bool = true). diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 8ba8525c6..be3310491 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -1,8 +1,8 @@ Set Implicit Arguments. Unset Strict Implicit. -Implicit Arguments fst. -Implicit Arguments snd. +Arguments fst : default implicits. +Arguments snd : default implicits. Module Type PO. Parameter T : Set. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 7214287a6..ece1b47b4 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,7 +1,7 @@ Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) (th el : T) := if s then th else el. -Implicit Arguments ifte. +Arguments ifte : default implicits. Lemma Reflexivity_provable : forall (A : Set) (a : A) (s : {a = a} + {a <> a}), diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index 8700a6c4e..6d9117c05 100644 --- a/test-suite/prerequisite/make_local.v +++ b/test-suite/prerequisite/make_local.v @@ -2,8 +2,7 @@ Definition f (A:Type) (a:A) := a. -Local Arguments Scope f [type_scope type_scope]. -Local Implicit Arguments f [A]. +Local Arguments f [A]%type_scope _%type_scope. (* Used in ImportedCoercion.v to test the locality flag *) diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index b4efa7edc..d0aa5c857 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -28,8 +28,8 @@ Class interp_pair (abs : Type) := { repr : term; link: abs = interp repr }. -Implicit Arguments repr [[interp_pair]]. -Implicit Arguments link [[interp_pair]]. +Arguments repr _ {interp_pair}. +Arguments link _ {interp_pair}. Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)). simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index 921433cad..9a19b595e 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). -Implicit Arguments vector []. +Arguments vector A : clear implicits. Require Import Coq.Program.Program. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 5b1482fd5..f07c0191f 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -73,7 +73,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Implicit 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 45c71615f..ca8da3948 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). -Implicit 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 841940492..29350d620 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -991,10 +991,10 @@ Proof. Qed. -Implicit Arguments Vector.cons [A n]. -Implicit Arguments Vector.nil [A]. -Implicit Arguments Vector.hd [A n]. -Implicit Arguments Vector.tl [A n]. +Arguments Vector.cons [A] _ [n]. +Arguments Vector.nil [A]. +Arguments Vector.hd [A n]. +Arguments Vector.tl [A n]. Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. @@ -1064,7 +1064,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} | S n', Vector.cons _ v' => vector_nth A n' _ v' end. -Implicit Arguments vector_nth [A p]. +Arguments vector_nth [A] _ [p]. Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, @@ -1159,7 +1159,7 @@ infiniteproof map_iterate'. Qed. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 6f27c1d36..18ebcd638 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -5,7 +5,7 @@ Require Import Program. Require Import List. Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. -Implicit Arguments vector []. +Arguments vector : clear implicits. Coercion vec_list : vector >-> list. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index ca3746716..2da630633 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -11,7 +11,7 @@ Check (A.opp 3). Record B := { f :> Z -> Z }. Variable a:B. -Arguments Scope a [Z_scope]. +Arguments a _%Z_scope : extra scopes. Check a 0. (* Check that casts activate scopes if ever possible *) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index cd6eac35c..400479ae8 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Implicit Arguments unit [[m] [m0] [α]]. -Implicit Arguments Monad []. +Arguments unit {m m0 α}. +Arguments Monad : clear implicits. Notation "'return' t" := (unit t). (* Test correct handling of existentials and defined fields. *) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 02e043bc3..b287b5fac 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -39,7 +39,7 @@ Qed. (* Check apply/eapply distinction in presence of open terms *) Parameter h : forall x y z : nat, x = z -> x = y. -Implicit Arguments h [[x] [y]]. +Arguments h {x y}. Goal 1 = 0 -> True. intro H. apply h in H || exact I. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index f5bb884d2..55ae54ca0 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -42,7 +42,7 @@ Inductive ctx : Type := Bind Scope context_scope with ctx. Delimit Scope context_scope with ctx. -Arguments Scope snoc [context_scope]. +Arguments snoc _%context_scope. Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 627794832..5b13f35d5 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c }. -Implicit Arguments mkTri [R S T]. +Arguments mkTri [R S T]. Definition tri_iffT : tri iffT iffT iffT := (mkTri (fun X0 X1 X2 E01 E02 => diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index a0981311b..23853890d 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y. Definition eq2 := fun (A:Type) (x y:A) => x=y. Definition eq3 := fun (A:Type) (x y:A) => x=y. -Implicit Arguments op' []. -Global Implicit Arguments op'' []. +Arguments op' : clear implicits. +Global Arguments op'' : clear implicits. -Implicit Arguments eq2 []. -Global Implicit Arguments eq3 []. +Arguments eq2 : clear implicits. +Global Arguments eq3 : clear implicits. Check (op 0 0). Check (op' nat 0 0). @@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} := (* Check multiple implicit arguments signatures *) -Implicit Arguments eq_refl [[A] [x]] [[A]]. +Arguments eq_refl {A x}, {A}. Check eq_refl : 0 = 0. (* Check that notations preserve implicit (since 8.3) *) Parameter p : forall A, A -> forall n, n = 0 -> True. -Implicit Arguments p [A n]. +Arguments p [A] _ [n]. Notation Q := (p 0). Check Q eq_refl. diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el index 662762b08..7c59fb6ae 100644 --- a/tools/gallina-syntax.el +++ b/tools/gallina-syntax.el @@ -432,7 +432,6 @@ ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") ("Cd" nil "Cd #." nil "Cd") diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9ff4e3302..5dcc170b1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2025,7 +2025,6 @@ let interp ?proof ~atts ~st c = | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> vernac_notation ~atts c infpl sc @@ -2099,8 +2098,6 @@ let interp ?proof ~atts ~st c = vernac_hints ~atts dbnames hints | VernacSyntacticDefinition (id,c,b) -> vernac_syntactic_definition ~atts id c b - | VernacDeclareImplicits (qid,l) -> - vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> vernac_arguments ~atts qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl @@ -2168,7 +2165,7 @@ let check_vernac_supports_locality c l = | VernacDeclareMLModule _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ - | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ + | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ | VernacSetOption _ | VernacUnsetOption _ |