diff options
47 files changed, 189 insertions, 183 deletions
diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v index 0940b1352..ce6600520 100644 --- a/plugins/dp/test2.v +++ b/plugins/dp/test2.v @@ -73,7 +73,7 @@ zenon. Inductive IN (A:Set) : A -> list A -> Prop := | IN1 : forall x l, IN A x (x::l) | IN2: forall x l, IN A x l -> forall y, IN A x (y::l). -Implicit Arguments IN [A]. +Arguments IN [A] _ _. Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l). zenon. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 7b4fdb089..4af650861 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -308,7 +308,7 @@ Definition map_option (A B:Type) (f : A -> option B) (o : option A) : option B : | Some x => f x end. -Implicit Arguments map_option [A B]. +Arguments map_option [A B] f o. Definition map_option2 (A B C : Type) (f : A -> B -> option C) (o: option A) (o': option B) : option C := @@ -318,7 +318,7 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C) | Some x , Some x' => f x x' end. -Implicit Arguments map_option2 [A B C]. +Arguments map_option2 [A B C] f o o'. Definition Rops_wd := mk_reqe rplus rtimes ropp req sor.(SORplus_wd) @@ -1034,4 +1034,4 @@ End Micromega. (* Local Variables: *) (* coding: utf-8 *) -(* End: *)
\ No newline at end of file +(* End: *) diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index e499f2220..c6dff3e00 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -746,11 +746,11 @@ Qed. (* End properties. *) End semi_rings. -Implicit Arguments Cons_varlist. -Implicit Arguments Cons_monom. -Implicit Arguments SPconst. -Implicit Arguments SPplus. -Implicit Arguments SPmult. +Arguments Cons_varlist : default implicits. +Arguments Cons_monom : default implicits. +Arguments SPconst : default implicits. +Arguments SPplus : default implicits. +Arguments SPmult : default implicits. Section rings. diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index 41190e8d9..ad75a8a4d 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -1011,11 +1011,11 @@ Qed. End semi_setoid_rings. -Implicit Arguments Cons_varlist. -Implicit Arguments Cons_monom. -Implicit Arguments SetSPconst. -Implicit Arguments SetSPplus. -Implicit Arguments SetSPmult. +Arguments Cons_varlist : default implicits. +Arguments Cons_monom : default implicits. +Arguments SetSPconst : default implicits. +Arguments SetSPplus : default implicits. +Arguments SetSPmult : default implicits. diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index f311d2447..56ae921ed 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -868,11 +868,11 @@ Inductive term : Set := | Tvar : nat -> term. Delimit Scope romega_scope with term. -Arguments Scope Tint [Int_scope]. -Arguments Scope Tplus [romega_scope romega_scope]. -Arguments Scope Tmult [romega_scope romega_scope]. -Arguments Scope Tminus [romega_scope romega_scope]. -Arguments Scope Topp [romega_scope romega_scope]. +Arguments Tint _%I. +Arguments Tplus (_ _)%term. +Arguments Tmult (_ _)%term. +Arguments Tminus (_ _)%term. +Arguments Topp _%term. Infix "+" := Tplus : romega_scope. Infix "*" := Tmult : romega_scope. diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index b34cf338b..77f8f8345 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -34,7 +34,7 @@ match n with O => Some x | S m => Lget A m q end end . -Implicit Arguments Lget [A]. +Arguments Lget [A] n l. Lemma map_app : forall (A B:Set) (f:A -> B) l m, List.map f (l ++ m) = List.map f l ++ List.map f m. @@ -288,34 +288,34 @@ Qed. End Store. -Implicit Arguments PNone [A]. -Implicit Arguments PSome [A]. +Arguments PNone [A]. +Arguments PSome [A] _. -Implicit Arguments Tempty [A]. -Implicit Arguments Branch0 [A]. -Implicit Arguments Branch1 [A]. +Arguments Tempty [A]. +Arguments Branch0 [A] _ _. +Arguments Branch1 [A] _ _ _. -Implicit Arguments Tget [A]. -Implicit Arguments Tadd [A]. +Arguments Tget [A] p T. +Arguments Tadd [A] p a T. -Implicit Arguments Tget_Tempty [A]. -Implicit Arguments Tget_Tadd [A]. +Arguments Tget_Tempty [A] p. +Arguments Tget_Tadd [A] i j a T. -Implicit Arguments mkStore [A]. -Implicit Arguments index [A]. -Implicit Arguments contents [A]. +Arguments mkStore [A] index contents. +Arguments index [A] s. +Arguments contents [A] s. -Implicit Arguments empty [A]. -Implicit Arguments get [A]. -Implicit Arguments push [A]. +Arguments empty [A]. +Arguments get [A] i S. +Arguments push [A] a S. -Implicit Arguments get_empty [A]. -Implicit Arguments get_push_Full [A]. +Arguments get_empty [A] i. +Arguments get_push_Full [A] i a S _. -Implicit Arguments Full [A]. -Implicit Arguments F_empty [A]. -Implicit Arguments F_push [A]. -Implicit Arguments In [A]. +Arguments Full [A] _. +Arguments F_empty [A]. +Arguments F_push [A] a S _. +Arguments In [A] x S F. Section Map. @@ -367,8 +367,8 @@ Defined. End Map. -Implicit Arguments Tmap [A B]. -Implicit Arguments map [A B]. -Implicit Arguments Full_map [A B f]. +Arguments Tmap [A B] f T. +Arguments map [A B] f S. +Arguments Full_map [A B f] S _. Notation "hyps \ A" := (push A hyps) (at level 72,left associativity). diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 8b5e42447..9cae7a44e 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -73,7 +73,7 @@ case_eq (form_eq p1 q1);clean. intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. Qed. -Implicit Arguments form_eq_refl [p q]. +Arguments form_eq_refl [p q] _. Section with_env. @@ -161,7 +161,7 @@ intros hyps F p g e; apply project_In. apply get_In with p;assumption. Qed. -Implicit Arguments project [hyps p g]. +Arguments project [hyps] F [p g] _. Inductive proof:Set := Ax : positive -> proof diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 6643c1429..c95f89c9f 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -54,3 +54,8 @@ negb'' : bool -> bool negb'' is transparent Expands to: Constant Top.negb'' +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index f423f8513..a2e6a1cfb 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -94,3 +94,6 @@ For eq_refl, when applied to 1 argument: Argument A is implicit and maximally inserted For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] +Warning: Implicit Arguments is deprecated; use Arguments instead +Warning: Implicit Arguments is deprecated; use Arguments instead +Warning: Implicit Arguments is deprecated; use Arguments instead diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 1dd5ce16c..146546dc1 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -19,7 +19,7 @@ Fixpoint fact (n:nat) : nat := | S n => S n * fact n end. -Arguments Scope fact [nat_scope]. +Arguments fact n%nat. Lemma lt_O_fact : forall n:nat, 0 < fact n. Proof. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 73a092143..24b6a7760 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -66,4 +66,4 @@ Definition bool_of_sumbool : intros A B H. elim H; intro; [exists true | exists false]; assumption. Defined. -Implicit Arguments bool_of_sumbool. +Arguments bool_of_sumbool : default implicits. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 55199cdea..8e491b1b8 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -55,8 +55,8 @@ Definition respectful {A B : Type} Delimit Scope signature_scope with signature. -Arguments Scope Proper [type_scope signature_scope]. -Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. Module ProperNotations. @@ -121,7 +121,7 @@ Definition forall_relation {A : Type} {B : A -> Type} (sig : forall a, relation (B a)) : relation (forall x, B x) := fun f g => forall a, sig a (f a) (g a). -Arguments Scope forall_relation [type_scope type_scope signature_scope]. +Arguments forall_relation {A B}%type sig%signature _ _. (** Non-dependent pointwise lifting *) diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 3a34e3a11..cf05d9d4c 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -351,7 +351,7 @@ Definition relation_equivalence {A : Type} : relation (relation A) := Class subrelation {A:Type} (R R' : relation A) : Prop := is_subrelation : @predicate_implication (A::A::Tnil) R R'. -Implicit Arguments subrelation [[A]]. +Arguments subrelation {A} R R'. Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := @predicate_intersection (A::A::Tnil) R R'. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 0fa5bfaa6..2b010206c 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -15,27 +15,25 @@ Require Import Relations Morphisms. fix the simpl tactic, since "simpl fst" would be refused for the moment. -Implicit Arguments fst [[A] [B]]. -Implicit Arguments snd [[A] [B]]. -Implicit Arguments pair [[A] [B]]. +Arguments fst {A B}. +Arguments snd {A B}. +Arguments pair {A B}. /NB *) Local Notation Fst := (@fst _ _). Local Notation Snd := (@snd _ _). -Arguments Scope relation_conjunction - [type_scope signature_scope signature_scope]. -Arguments Scope relation_equivalence - [type_scope signature_scope signature_scope]. -Arguments Scope subrelation [type_scope signature_scope signature_scope]. -Arguments Scope Reflexive [type_scope signature_scope]. -Arguments Scope Irreflexive [type_scope signature_scope]. -Arguments Scope Symmetric [type_scope signature_scope]. -Arguments Scope Transitive [type_scope signature_scope]. -Arguments Scope PER [type_scope signature_scope]. -Arguments Scope Equivalence [type_scope signature_scope]. -Arguments Scope StrictOrder [type_scope signature_scope]. +Arguments relation_conjunction A%type (R R')%signature _ _. +Arguments relation_equivalence A%type (_ _)%signature. +Arguments subrelation A%type (R R')%signature. +Arguments Reflexive A%type R%signature. +Arguments Irreflexive A%type R%signature. +Arguments Symmetric A%type R%signature. +Arguments Transitive A%type R%signature. +Arguments PER A%type R%signature. +Arguments Equivalence A%type R%signature. +Arguments StrictOrder A%type R%signature. Generalizable Variables A B RA RB Ri Ro f. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 7665ac05b..0c1448c9b 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -652,7 +652,7 @@ Add Relation key E.eq transitivity proved by E.eq_trans as KeySetoid. -Implicit Arguments Equal [[elt]]. +Arguments Equal {elt} m m'. Add Parametric Relation (elt : Type) : (t elt) Equal reflexivity proved by (@Equal_refl elt) diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 206714949..2e2eb166d 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -84,7 +84,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section A. Variable A:Type. - Implicit Arguments Leaf [A]. + Arguments Leaf [A]. Definition empty : t A := Leaf. @@ -814,7 +814,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Variable A B C : Type. Variable f : option A -> option B -> option C. - Implicit Arguments Leaf [A]. + Arguments Leaf [A]. Fixpoint xmap2_l (m : t A) : t C := match m with diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index bab764bcb..41f6b70b2 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -137,7 +137,7 @@ Inductive nat : Set := Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. -Arguments Scope S [nat_scope]. +Arguments S _%nat. (********************************************************************) @@ -149,7 +149,7 @@ Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. -Implicit Arguments None [A]. +Arguments None [A]. Definition option_map (A B:Type) (f:A->B) o := match o with @@ -165,8 +165,8 @@ Inductive sum (A B:Type) : Type := Notation "x + y" := (sum x y) : type_scope. -Implicit Arguments inl [[A] [B]] [A]. -Implicit Arguments inr [[A] [B]] [B]. +Arguments inl {A B} _ , [A] B _. +Arguments inr {A B} _ , A [B] _. (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) @@ -179,7 +179,7 @@ Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. -Implicit Arguments pair [[A] [B]]. +Arguments pair {A B} _ _. Section projections. Variables A B : Type. @@ -221,7 +221,7 @@ Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. -Implicit Arguments nil [A]. +Arguments nil [A]. Infix "::" := cons (at level 60, right associativity) : list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. @@ -330,9 +330,9 @@ Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. Hint Resolve identity_refl: core. -Implicit Arguments identity_ind [A]. -Implicit Arguments identity_rec [A]. -Implicit Arguments identity_rect [A]. +Arguments identity_ind [A] a P f y i. +Arguments identity_rec [A] a P f y i. +Arguments identity_rect [A] a P f y i. (** Identity type *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index b9e22f15e..d1eabcabf 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -62,8 +62,8 @@ Inductive or (A B:Prop) : Prop := where "A \/ B" := (or A B) : type_scope. -Implicit Arguments or_introl [A B] [A]. -Implicit Arguments or_intror [A B] [B]. +Arguments or_introl [A B] _, [A] B _. +Arguments or_intror [A B] _, A [B] _. (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) @@ -270,12 +270,12 @@ Notation "x = y" := (x = y :>_) : type_scope. Notation "x <> y :> T" := (~ x = y :>T) : type_scope. Notation "x <> y" := (x <> y :>_) : type_scope. -Implicit Arguments eq [[A]]. -Implicit Arguments eq_refl [[A] [x]] [A]. +Arguments eq {A} x _. +Arguments eq_refl {A x} , [A] x. -Implicit Arguments eq_ind [A]. -Implicit Arguments eq_rec [A]. -Implicit Arguments eq_rect [A]. +Arguments eq_ind [A] x P _ y _. +Arguments eq_rec [A] x P _ y _. +Arguments eq_rect [A] x P _ y _. Hint Resolve I conj or_introl or_intror eq_refl: core. Hint Resolve ex_intro ex_intro2: core. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 12ac08ff0..637994b2b 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -38,10 +38,10 @@ Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := (* Notations *) -Arguments Scope sig [type_scope type_scope]. -Arguments Scope sig2 [type_scope type_scope type_scope]. -Arguments Scope sigT [type_scope type_scope]. -Arguments Scope sigT2 [type_scope type_scope type_scope]. +Arguments sig (A P)%type. +Arguments sig2 (A P Q)%type. +Arguments sigT (A P)%type. +Arguments sigT2 (A P Q)%type. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. @@ -126,8 +126,8 @@ Inductive sumbool (A B:Prop) : Set := Add Printing If sumbool. -Implicit Arguments left [[A] [B]] [A]. -Implicit Arguments right [[A] [B]] [B]. +Arguments left {A B} _, [A] B _. +Arguments right {A B} _ , A [B] _. (** [sumor] is an option type equipped with the justification of why it may not be a regular value *) @@ -139,8 +139,8 @@ Inductive sumor (A:Type) (B:Prop) : Type := Add Printing If sumor. -Implicit Arguments inleft [[A] [B]] [A]. -Implicit Arguments inright [[A] [B]] [B]. +Arguments inleft {A B} _ , [A] B _. +Arguments inright {A B} _ , A [B] _. (** Various forms of the axiom of choice for specifications *) @@ -208,11 +208,11 @@ Definition Exc := option. Definition value := Some. Definition error := @None. -Implicit Arguments error [A]. +Arguments error [A]. Definition except := False_rec. (* for compatibility with previous versions *) -Implicit Arguments except [P]. +Arguments except [P] _. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Proof. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index ef319529d..97915055d 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -748,7 +748,7 @@ rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. -Implicit Arguments eq [ [A] ]. +Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a341a7a5a..d84cd8240 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -107,8 +107,8 @@ Section Dependent_Equality. End Dependent_Equality. -Implicit Arguments eq_dep [U P]. -Implicit Arguments eq_dep1 [U P]. +Arguments eq_dep [U P] p x q _. +Arguments eq_dep1 [U P] p x q y. (** Dependent equality is equivalent to equality on dependent pairs *) @@ -412,5 +412,5 @@ Notation inj_pairT2 := inj_pair2. End EqdepTheory. -Implicit Arguments eq_dep []. -Implicit Arguments eq_dep1 []. +Arguments eq_dep U P p x q _ : clear implicits. +Arguments eq_dep1 U P p x q y : clear implicits. diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v index 421bbebcf..f5e71ef49 100644 --- a/theories/Logic/ExtensionalityFacts.v +++ b/theories/Logic/ExtensionalityFacts.v @@ -42,8 +42,8 @@ Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }. Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}. -Implicit Arguments pi1 [[A]]. -Implicit Arguments pi2 [[A]]. +Arguments pi1 {A} _. +Arguments pi2 {A} _. Lemma diagonal_projs_same_behavior : forall A (x:Delta A), pi1 x = pi2 x. Proof. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 583d348a2..753009e68 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -24,7 +24,7 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := Set Elimination Schemes. -Implicit Arguments JMeq_refl [[A] [x]] [A]. +Arguments JMeq_refl {A x} , [A] x. Hint Resolve JMeq_refl. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 1e2ddb7a6..bdada4868 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -375,7 +375,7 @@ Fixpoint fold (A : Type) (f : elt -> A -> A)(s : t) : A -> A := | Leaf => a | Node l x r _ => fold f r (f x (fold f l a)) end. -Implicit Arguments fold [A]. +Arguments fold [A] f s _. (** ** Subset *) diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 20504bcf8..f2b908af0 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -437,7 +437,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}. Definition t := t_. - Implicit Arguments Mkt [ [is_ok] ]. + Arguments Mkt this {is_ok}. Hint Resolve is_ok : typeclass_instances. Definition In (x : elt)(s : t) := M.In x s.(this). diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index 69754f144..dfb2c5025 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -27,8 +27,8 @@ Inductive positive : Set := Delimit Scope positive_scope with positive. Bind Scope positive_scope with positive. -Arguments Scope xO [positive_scope]. -Arguments Scope xI [positive_scope]. +Arguments xO _%positive. +Arguments xI _%positive. (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. @@ -41,7 +41,7 @@ Inductive N : Set := Delimit Scope N_scope with N. Bind Scope N_scope with N. -Arguments Scope Npos [positive_scope]. +Arguments Npos _%positive. (** [Z] is a datatype representing the integers in a binary way. An integer is either zero or a strictly positive number @@ -57,5 +57,5 @@ Inductive Z : Set := Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. -Arguments Scope Zpos [positive_scope]. -Arguments Scope Zneg [positive_scope]. +Arguments Zpos _%positive. +Arguments Zneg _%positive. diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 3aa075384..59656eedb 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -204,7 +204,7 @@ Module ZnZ. End Specs. - Implicit Arguments Specs [[t]]. + Arguments Specs {t} ops. (** Generic construction of double words *) diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 073afec37..a274b8395 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -53,7 +53,7 @@ Section Zn2Z. End Zn2Z. -Implicit Arguments W0 [znz]. +Arguments W0 [znz]. (** From a cyclic representation [w], we iterate the [zn2z] construct [n] times, gaining the type of binary trees of depth at most [n], diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 71d275601..443777f52 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -44,8 +44,8 @@ Local Open Scope bigZ_scope. Notation bigZ := BigZ.t. Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_. -Arguments Scope BigZ.Pos [bigN_scope]. -Arguments Scope BigZ.Neg [bigN_scope]. +Arguments BigZ.Pos _%bigN. +Arguments BigZ.Neg _%bigN. Local Notation "0" := BigZ.zero : bigZ_scope. Local Notation "1" := BigZ.one : bigZ_scope. Local Notation "2" := BigZ.two : bigZ_scope. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 8df715af9..ad7a9f3ae 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -23,7 +23,7 @@ Include NStrongRecProp N. Definition if_zero (A : Type) (a b : A) (n : N.t) : A := recursion a (fun _ _ => b) n. -Implicit Arguments if_zero [A]. +Arguments if_zero [A] a b n. Instance if_zero_wd (A : Type) : Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A). diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 039eefdf5..607746d59 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -190,7 +190,7 @@ Qed. End FixPoint. End StrongRecursion. -Implicit Arguments strong_rec [A]. +Arguments strong_rec [A] a f n. End NStrongRecProp. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index b06e42ca2..7f205b388 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -52,7 +52,7 @@ Local Open Scope bigN_scope. Notation bigN := BigN.t. Bind Scope bigN_scope with bigN BigN.t BigN.t'. -Arguments Scope BigN.N0 [int31_scope]. +Arguments BigN.N0 _%int31. Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *) diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 668a11123..3ea3d5fd5 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -705,7 +705,7 @@ pr End SameLevel. - Implicit Arguments same_level [res]. + Arguments same_level [res] f x y. Theorem spec_same_level_dep : forall res diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index aed96a831..4717d0b23 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -16,12 +16,12 @@ Require Import DoubleBase. Require Import CyclicAxioms. Require Import DoubleCyclic. -Implicit Arguments mk_zn2z_ops [t]. -Implicit Arguments mk_zn2z_ops_karatsuba [t]. -Implicit Arguments mk_zn2z_specs [t ops]. -Implicit Arguments mk_zn2z_specs_karatsuba [t ops]. -Implicit Arguments ZnZ.digits [t]. -Implicit Arguments ZnZ.zdigits [t]. +Arguments mk_zn2z_ops [t] ops. +Arguments mk_zn2z_ops_karatsuba [t] ops. +Arguments mk_zn2z_specs [t ops] specs. +Arguments mk_zn2z_specs_karatsuba [t ops] specs. +Arguments ZnZ.digits [t] Ops. +Arguments ZnZ.zdigits [t] Ops. Lemma Pshiftl_nat_Zpower : forall n p, Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n. @@ -230,8 +230,8 @@ Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) := End ExtendMax. -Implicit Arguments extend_tr[w m]. -Implicit Arguments castm[w m n]. +Arguments extend_tr [w m] v n. +Arguments castm [w m n] H x. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index a0ad7643d..2c7884ac4 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -445,7 +445,7 @@ Qed. Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) := Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n). -Implicit Arguments recursion [A]. +Arguments recursion [A] a f n. Instance recursion_wd (A : Type) (Aeq : relation A) : Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 5293a66cb..7cef5c5ad 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -17,7 +17,7 @@ (** The polymorphic identity function is defined in [Datatypes]. *) -Implicit Arguments id [[A]]. +Arguments id {A} x. (** Function composition. *) @@ -53,5 +53,5 @@ Definition apply {A B} (f : A -> B) (x : A) := f x. (** Curryfication of [prod] is defined in [Logic.Datatypes]. *) -Implicit Arguments prod_curry [[A] [B] [C]]. -Implicit Arguments prod_uncurry [[A] [B] [C]]. +Arguments prod_curry {A B C} f p. +Arguments prod_uncurry {A B C} f x y. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index a66e1284b..61d389ed5 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -18,15 +18,15 @@ Notation " () " := tt. (** Set maximally inserted implicit arguments for standard definitions. *) -Implicit Arguments Some [[A]]. -Implicit Arguments None [[A]]. +Arguments Some {A} _. +Arguments None {A}. -Implicit Arguments pair [[A] [B]]. -Implicit Arguments fst [[A] [B]]. -Implicit Arguments snd [[A] [B]]. +Arguments pair {A B} _ _. +Arguments fst {A B} _. +Arguments snd {A B} _. -Implicit Arguments nil [[A]]. -Implicit Arguments cons [[A]]. +Arguments nil {A}. +Arguments cons {A} _ _. Require List. Export List.ListNotations. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a32ccbc4b..94ea4906c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -18,7 +18,7 @@ Record Q : Set := Qmake {Qnum : Z; Qden : positive}. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. -Arguments Scope Qmake [Z_scope positive_scope]. +Arguments Qmake _%Z _%positive. Open Scope Q_scope. Ltac simpl_mult := repeat rewrite Zpos_mult_morphism. @@ -27,7 +27,7 @@ Ltac simpl_mult := repeat rewrite Zpos_mult_morphism. Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. -Arguments Scope inject_Z [Z_scope]. +Arguments inject_Z x%Z. Notation QDen p := (Zpos (Qden p)). Notation " 0 " := (0#1) : Q_scope. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 218289a4f..fea2ba398 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -18,7 +18,7 @@ Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. Delimit Scope Qc_scope with Qc. Bind Scope Qc_scope with Qc. -Arguments Scope Qcmake [Q_scope]. +Arguments Qcmake this%Q _. Open Scope Qc_scope. Lemma Qred_identity : @@ -69,7 +69,7 @@ Proof. Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). -Arguments Scope Q2Qc [Q_scope]. +Arguments Q2Qc q%Q. Notation " !! " := Q2Qc : Qc_scope. Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 18cf53e71..3075bee8f 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -28,15 +28,15 @@ Definition inv_fct f (x:R) : R := / f x. Delimit Scope Rfun_scope with F. -Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope]. -Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope]. -Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope]. -Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope]. -Arguments Scope inv_fct [Rfun_scope R_scope]. -Arguments Scope opp_fct [Rfun_scope R_scope]. -Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope]. -Arguments Scope div_real_fct [R_scope Rfun_scope R_scope]. -Arguments Scope comp [Rfun_scope Rfun_scope R_scope]. +Arguments plus_fct (f1 f2)%F x%R. +Arguments mult_fct (f1 f2)%F x%R. +Arguments minus_fct (f1 f2)%F x%R. +Arguments div_fct (f1 f2)%F x%R. +Arguments inv_fct f%F x%R. +Arguments opp_fct f%F x%R. +Arguments mult_real_fct a%R f%F x%R. +Arguments div_real_fct a%R f%F x%R. +Arguments comp (f1 f2)%F x%R. Infix "+" := plus_fct : Rfun_scope. Notation "- x" := (opp_fct x) : Rfun_scope. @@ -74,8 +74,8 @@ Definition constant_D_eq f (D:R -> Prop) (c:R) : Prop := Definition continuity_pt f (x0:R) : Prop := continue_in f no_cond x0. Definition continuity f : Prop := forall x:R, continuity_pt f x. -Arguments Scope continuity_pt [Rfun_scope R_scope]. -Arguments Scope continuity [Rfun_scope]. +Arguments continuity_pt f%F x0%R. +Arguments continuity f%F. (**********) Lemma continuity_pt_plus : @@ -274,12 +274,12 @@ Definition derivable f := forall x:R, derivable_pt f x. Definition derive_pt f (x:R) (pr:derivable_pt f x) := proj1_sig pr. Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x). -Arguments Scope derivable_pt_lim [Rfun_scope R_scope]. -Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope]. -Arguments Scope derivable_pt [Rfun_scope R_scope]. -Arguments Scope derivable [Rfun_scope]. -Arguments Scope derive_pt [Rfun_scope R_scope _]. -Arguments Scope derive [Rfun_scope _]. +Arguments derivable_pt_lim f%F x%R l. +Arguments derivable_pt_abs f%F (x l)%R. +Arguments derivable_pt f%F x%R. +Arguments derivable f%F. +Arguments derive_pt f%F x%R pr. +Arguments derive f%F pr x. Definition antiderivative f (g:R -> R) (a b:R) : Prop := (forall x:R, diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index e858d2148..8f01d7d03 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -111,7 +111,7 @@ Fixpoint INR (n:nat) : R := | S O => 1 | S n => INR n + 1 end. -Arguments Scope INR [nat_scope]. +Arguments INR n%nat. (**********************************************************) @@ -125,7 +125,7 @@ Definition IZR (z:Z) : R := | Zpos n => INR (nat_of_P n) | Zneg n => - INR (nat_of_P n) end. -Arguments Scope IZR [Z_scope]. +Arguments IZR z%Z. (**********************************************************) (** * [R] Archimedean *) diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 21beac36f..f7f5512e7 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -17,17 +17,17 @@ Require Import Relation_Operators. Section Properties. - Implicit Arguments clos_refl_trans [A]. - Implicit Arguments clos_refl_trans_1n [A]. - Implicit Arguments clos_refl_trans_n1 [A]. - Implicit Arguments clos_refl_sym_trans [A]. - Implicit Arguments clos_refl_sym_trans_1n [A]. - Implicit Arguments clos_refl_sym_trans_n1 [A]. - Implicit Arguments clos_trans [A]. - Implicit Arguments clos_trans_1n [A]. - Implicit Arguments clos_trans_n1 [A]. - Implicit Arguments inclusion [A]. - Implicit Arguments preorder [A]. + Arguments clos_refl_trans [A] R x _. + Arguments clos_refl_trans_1n [A] R x _. + Arguments clos_refl_trans_n1 [A] R x _. + Arguments clos_refl_sym_trans [A] R _ _. + Arguments clos_refl_sym_trans_1n [A] R x _. + Arguments clos_refl_sym_trans_n1 [A] R x _. + Arguments clos_trans [A] R x _. + Arguments clos_trans_1n [A] R x _. + Arguments clos_trans_n1 [A] R x _. + Arguments inclusion [A] R1 R2. + Arguments preorder [A] R. Variable A : Type. Variable R : relation A. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index cdca469ac..0e230b77b 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -25,7 +25,7 @@ Require Import List Relations Relations_1. Set Implicit Arguments. Local Notation "[ ]" := nil (at level 0). Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). -Implicit Arguments Transitive [U]. +Arguments Transitive [U] R. Section defs. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 5d8773957..f84cdf32c 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -20,9 +20,9 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := | EQ : eq x y -> Compare lt eq x y | GT : lt y x -> Compare lt eq x y. -Implicit Arguments LT [X lt eq x y]. -Implicit Arguments EQ [X lt eq x y]. -Implicit Arguments GT [X lt eq x y]. +Arguments LT [X lt eq x y] _. +Arguments EQ [X lt eq x y] _. +Arguments GT [X lt eq x y] _. Module Type MiniOrderedType. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 62cce1d26..bac50fc45 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -27,7 +27,7 @@ Module Type Int. Parameter int : Set. Parameter i2z : int -> Z. - Arguments Scope i2z [ Int_scope ]. + Arguments i2z _%I. Parameter _0 : int. Parameter _1 : int. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 86e9eb8ca..5a2c3cc32 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -111,7 +111,7 @@ Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z := end. Definition Zlength := Zlength_aux 0. -Implicit Arguments Zlength [A]. +Arguments Zlength [A] l. Section Zlength_properties. @@ -146,6 +146,6 @@ Section Zlength_properties. End Zlength_properties. -Implicit Arguments Zlength_correct [A]. -Implicit Arguments Zlength_cons [A]. -Implicit Arguments Zlength_nil_inv [A]. +Arguments Zlength_correct [A] l. +Arguments Zlength_cons [A] x l. +Arguments Zlength_nil_inv [A] l _. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index e5a92024f..314f696a2 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -124,7 +124,7 @@ Proof. exact (Z_div_mod a b Hb). Qed. -Implicit Arguments Zdiv_eucl_exist. +Arguments Zdiv_eucl_exist : default implicits. (** Uniqueness theorems *) @@ -679,7 +679,7 @@ Proof. rewrite Z.abs_neq; [ assumption | omega ]. Qed. -Implicit Arguments Zdiv_eucl_extended. +Arguments Zdiv_eucl_extended : default implicits. (** * Division and modulo in Z agree with same in nat: *) |