Commit 79a11082 authored by Ralf Jung's avatar Ralf Jung
Browse files

also add Local/Global to Arguments

parent 143d0af3
......@@ -34,8 +34,8 @@ Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
Arguments agree_car {_} _.
Arguments agree_not_nil {_} _.
Global Arguments agree_car {_} _.
Global Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Definition to_agree {A} (a : A) : agree A :=
......@@ -259,8 +259,8 @@ Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
End agree.
Global Instance: Params (@to_agree) 1 := {}.
Arguments agreeO : clear implicits.
Arguments agreeR : clear implicits.
Global Arguments agreeO : clear implicits.
Global Arguments agreeR : clear implicits.
Program Definition agree_map {A B} (f : A B) (x : agree A) : agree B :=
{| agree_car := f <$> agree_car x |}.
......
......@@ -26,7 +26,7 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Global Instance: Params (@big_opL) 4 := {}.
Arguments big_opL {M} o {_ A} _ !_ /.
Global Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
......@@ -39,7 +39,7 @@ Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Arguments big_opM {M} o {_ K _ _ A} _ _.
Global Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Global Instance: Params (@big_opM) 7 := {}.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
......@@ -53,7 +53,7 @@ Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Arguments big_opS {M} o {_ A _ _} _ _.
Global Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Global Instance: Params (@big_opS) 6 := {}.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
......@@ -64,7 +64,7 @@ Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
Arguments big_opMS {M} o {_ A _ _} _ _.
Global Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Global Instance: Params (@big_opMS) 6 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
......
......@@ -77,21 +77,21 @@ Structure cmraT := CmraT' {
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
Arguments CmraT' _ {_ _ _ _ _ _} _ _.
Global Arguments CmraT' _ {_ _ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m) (only parsing).
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_pcore : simpl never.
Arguments cmra_op : simpl never.
Arguments cmra_valid : simpl never.
Arguments cmra_validN : simpl never.
Arguments cmra_ofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Global Arguments cmra_car : simpl never.
Global Arguments cmra_equiv : simpl never.
Global Arguments cmra_dist : simpl never.
Global Arguments cmra_pcore : simpl never.
Global Arguments cmra_op : simpl never.
Global Arguments cmra_valid : simpl never.
Global Arguments cmra_validN : simpl never.
Global Arguments cmra_ofe_mixin : simpl never.
Global Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
......@@ -144,27 +144,27 @@ Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x Some x.
Arguments core_id {_} _ {_}.
Global Arguments core_id {_} _ {_}.
Global Hint Mode CoreId + ! : typeclass_instances.
Global Instance: Params (@CoreId) 1 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False.
Arguments exclusive0_l {_} _ {_} _ _.
Global Arguments exclusive0_l {_} _ {_} _ _.
Global Hint Mode Exclusive + ! : typeclass_instances.
Global Instance: Params (@Exclusive) 1 := {}.
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
cancelableN n y z : {n}(x y) x y {n} x z y {n} z.
Arguments cancelableN {_} _ {_} _ _ _ _.
Global Arguments cancelableN {_} _ {_} _ _ _ _.
Global Hint Mode Cancelable + ! : typeclass_instances.
Global Instance: Params (@Cancelable) 1 := {}.
(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
id_free0_r y : {0}x x y {0} x False.
Arguments id_free0_r {_} _ {_} _ _.
Global Arguments id_free0_r {_} _ {_} _ _.
Global Hint Mode IdFree + ! : typeclass_instances.
Global Instance: Params (@IdFree) 1 := {}.
......@@ -180,7 +180,7 @@ Global Instance: Params (@core) 2 := {}.
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
Global Arguments ε {_ _}.
Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
mixin_ucmra_unit_valid : (ε : A);
......@@ -201,19 +201,19 @@ Structure ucmraT := UcmraT' {
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
Global Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
Notation UcmraT A m :=
(UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Arguments ucmra_pcore : simpl never.
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
Arguments ucmra_ofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Global Arguments ucmra_car : simpl never.
Global Arguments ucmra_equiv : simpl never.
Global Arguments ucmra_dist : simpl never.
Global Arguments ucmra_pcore : simpl never.
Global Arguments ucmra_op : simpl never.
Global Arguments ucmra_valid : simpl never.
Global Arguments ucmra_validN : simpl never.
Global Arguments ucmra_ofe_mixin : simpl never.
Global Arguments ucmra_cmra_mixin : simpl never.
Global Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
......@@ -248,9 +248,9 @@ Class CmraMorphism {A B : cmraT} (f : A → B) := {
cmra_morphism_pcore x : f <$> pcore x pcore (f x);
cmra_morphism_op x y : f (x y) f x f y
}.
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
Global Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Global Arguments cmra_morphism_pcore {_ _} _ {_} _.
Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
(** * Properties **)
Section cmra.
......@@ -1110,7 +1110,7 @@ Section prod.
Local Instance prod_op : Op (A * B) := λ x y, (x.1 y.1, x.2 y.2).
Local Instance prod_pcore : PCore (A * B) := λ x,
c1 pcore (x.1); c2 pcore (x.2); Some (c1, c2).
Arguments prod_pcore !_ /.
Local Arguments prod_pcore !_ /.
Local Instance prod_valid : Valid (A * B) := λ x, x.1 x.2.
Local Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1 {n} x.2.
......@@ -1225,7 +1225,7 @@ End prod.
Global Hint Extern 4 (CoreId _) =>
notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
Arguments prodR : clear implicits.
Global Arguments prodR : clear implicits.
Section prod_unit.
Context {A B : ucmraT}.
......@@ -1262,7 +1262,7 @@ Section prod_unit.
Proof. unfold_leibniz. apply pair_op_2. Qed.
End prod_unit.
Arguments prodUR : clear implicits.
Global Arguments prodUR : clear implicits.
Global Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A A') (g : B B') :
CmraMorphism f CmraMorphism g CmraMorphism (prod_map f g).
......@@ -1338,7 +1338,7 @@ Section option.
Local Instance option_validN : ValidN (option A) := λ n ma,
match ma with Some a => {n} a | None => True end.
Local Instance option_pcore : PCore (option A) := λ ma, Some (ma = pcore).
Arguments option_pcore !_ /.
Local Arguments option_pcore !_ /.
Local Instance option_op : Op (option A) := union_with (λ a b, Some (a b)).
Definition Some_valid a : Some a a := reflexivity _.
......@@ -1514,8 +1514,8 @@ Section option.
Proof. destruct ma; apply _. Qed.
End option.
Arguments optionR : clear implicits.
Arguments optionUR : clear implicits.
Global Arguments optionR : clear implicits.
Global Arguments optionUR : clear implicits.
Section option_prod.
Context {A B : cmraT}.
......@@ -1659,8 +1659,8 @@ Section discrete_fun_cmra.
Proof. intros ? f Hf x. by apply: discrete. Qed.
End discrete_fun_cmra.
Arguments discrete_funR {_} _.
Arguments discrete_funUR {_} _.
Global Arguments discrete_funR {_} _.
Global Arguments discrete_funUR {_} _.
Global Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A ucmraT} (f : x, B1 x B2 x) :
( x, CmraMorphism (f x)) CmraMorphism (discrete_fun_map f).
......
......@@ -66,7 +66,7 @@ Inductive coPset_disj :=
| CoPsetBot : coPset_disj.
Section coPset_disj.
Arguments op _ _ !_ !_ /.
Local Arguments op _ _ !_ !_ /.
Canonical Structure coPset_disjO := leibnizO coPset_disj.
Local Instance coPset_disj_valid : Valid coPset_disj := λ X,
......
......@@ -28,8 +28,8 @@ with g (k : nat) : A (S k) -n> A k :=
match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
Arguments f : simpl never.
Arguments g : simpl never.
Global Arguments f : simpl never.
Global Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) x.
Proof using Fcontr.
......
......@@ -13,9 +13,9 @@ Inductive csum (A B : Type) :=
| Cinl : A csum A B
| Cinr : B csum A B
| CsumBot : csum A B.
Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}.
Global Arguments Cinl {_ _} _.
Global Arguments Cinr {_ _} _.
Global Arguments CsumBot {_ _}.
Global Instance: Params (@Cinl) 2 := {}.
Global Instance: Params (@Cinr) 2 := {}.
......@@ -110,7 +110,7 @@ Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
End ofe.
Arguments csumO : clear implicits.
Global Arguments csumO : clear implicits.
(* Functor on COFEs *)
Definition csum_map {A A' B B'} (fA : A A') (fB : B B')
......@@ -361,7 +361,7 @@ Proof.
Qed.
End cmra.
Arguments csumR : clear implicits.
Global Arguments csumR : clear implicits.
(* Functor *)
Global Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A A') (g : B B') :
......
......@@ -35,14 +35,14 @@ Structure draT := DraT {
dra_valid : Valid dra_car;
dra_mixin : DraMixin dra_car
}.
Arguments DraT _ {_ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_pcore : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_mixin : simpl never.
Global Arguments DraT _ {_ _ _ _ _} _.
Global Arguments dra_car : simpl never.
Global Arguments dra_equiv : simpl never.
Global Arguments dra_pcore : simpl never.
Global Arguments dra_disjoint : simpl never.
Global Arguments dra_op : simpl never.
Global Arguments dra_valid : simpl never.
Global Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
......@@ -93,9 +93,9 @@ Record validity (A : draT) := Validity {
validity_prf : validity_is_valid valid validity_car
}.
Add Printing Constructor validity.
Arguments Validity {_} _ _ _.
Arguments validity_car {_} _.
Arguments validity_is_valid {_} _.
Global Arguments Validity {_} _ _ _.
Global Arguments validity_car {_} _.
Global Arguments validity_is_valid {_} _.
Definition to_validity {A : draT} (x : A) : validity A :=
Validity x (valid x) id.
......@@ -105,7 +105,7 @@ Section dra.
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Arguments valid _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Instance validity_valid : Valid (validity A) := validity_is_valid.
Local Instance validity_equiv : Equiv (validity A) := λ x y,
......
......@@ -7,8 +7,8 @@ Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) :=
| Excl : A excl A
| ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclBot {_}.
Global Arguments Excl {_} _.
Global Arguments ExclBot {_}.
Global Instance: Params (@Excl) 1 := {}.
Global Instance: Params (@ExclBot) 1 := {}.
......@@ -114,8 +114,8 @@ Proof.
Qed.
End excl.
Arguments exclO : clear implicits.
Arguments exclR : clear implicits.
Global Arguments exclO : clear implicits.
Global Arguments exclR : clear implicits.
(* Functor *)
Definition excl_map {A B} (f : A B) (x : excl A) : excl B :=
......
......@@ -97,7 +97,7 @@ Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(** Internalized properties *)
End ofe.
Arguments gmapO _ {_ _} _.
Global Arguments gmapO _ {_ _} _.
(** Non-expansiveness of higher-order map functions and big-ops *)
Lemma merge_ne `{Countable K} {A B C : ofeT} (f g : option A option B option C)
......@@ -232,8 +232,8 @@ Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
End cmra.
Arguments gmapR _ {_ _} _.
Arguments gmapUR _ {_ _} _.
Global Arguments gmapR _ {_ _} _.
Global Arguments gmapUR _ {_ _} _.
Section properties.
Context `{Countable K} {A : cmraT}.
......
......@@ -95,6 +95,6 @@ Section gmultiset.
End gmultiset.
Arguments gmultisetO _ {_ _}.
Arguments gmultisetR _ {_ _}.
Arguments gmultisetUR _ {_ _}.
Global Arguments gmultisetO _ {_ _}.
Global Arguments gmultisetR _ {_ _}.
Global Arguments gmultisetUR _ {_ _}.
......@@ -66,22 +66,22 @@ Section gset.
End gset.
Arguments gsetO _ {_ _}.
Arguments gsetR _ {_ _}.
Arguments gsetUR _ {_ _}.
Global Arguments gsetO _ {_ _}.
Global Arguments gsetR _ {_ _}.
Global Arguments gsetUR _ {_ _}.
(* The disjoint union CMRA *)
Inductive gset_disj K `{Countable K} :=
| GSet : gset K gset_disj K
| GSetBot : gset_disj K.
Arguments GSet {_ _ _} _.
Arguments GSetBot {_ _ _}.
Global Arguments GSet {_ _ _} _.
Global Arguments GSetBot {_ _ _}.
Section gset_disj.
Context `{Countable K}.
Arguments op _ _ !_ !_ /.
Arguments cmra_op _ !_ !_ /.
Arguments ucmra_op _ !_ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments cmra_op _ !_ !_ /.
Local Arguments ucmra_op _ !_ !_ /.
Canonical Structure gset_disjO := leibnizO (gset_disj K).
......@@ -134,7 +134,7 @@ Section gset_disj.
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
Canonical Structure gset_disjUR := UcmraT (gset_disj K) gset_disj_ucmra_mixin.
Arguments op _ _ _ _ : simpl never.
Local Arguments op _ _ _ _ : simpl never.
Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K Prop) X :
( Y, X Y j, j Y P j)
......@@ -231,6 +231,6 @@ Section gset_disj.
Qed.
End gset_disj.
Arguments gset_disjO _ {_ _}.
Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.
Global Arguments gset_disjO _ {_ _}.
Global Arguments gset_disjR _ {_ _}.
Global Arguments gset_disjUR _ {_ _}.
......@@ -95,7 +95,7 @@ Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
End ofe.
Arguments listO : clear implicits.
Global Arguments listO : clear implicits.
(** Non-expansiveness of higher-order list functions and big-ops *)
Global Instance list_fmap_ne {A B : ofeT} (f : A B) n :
......@@ -296,8 +296,8 @@ Section cmra.
End cmra.
Arguments listR : clear implicits.
Arguments listUR : clear implicits.
Global Arguments listR : clear implicits.
Global Arguments listUR : clear implicits.
Global Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
replicate n ε ++ [x].
......
......@@ -20,9 +20,9 @@ Record namespace_map (A : Type) := NamespaceMap {
namespace_map_token_proj : coPset_disj
}.
Add Printing Constructor namespace_map.
Arguments NamespaceMap {_} _ _.
Arguments namespace_map_data_proj {_} _.
Arguments namespace_map_token_proj {_} _.
Global Arguments NamespaceMap {_} _ _.
Global Arguments namespace_map_data_proj {_} _.
Global Arguments namespace_map_token_proj {_} _.
Global Instance: Params (@NamespaceMap) 1 := {}.
Global Instance: Params (@namespace_map_data_proj) 1 := {}.
Global Instance: Params (@namespace_map_token_proj) 1 := {}.
......@@ -72,7 +72,7 @@ Global Instance namespace_map_ofe_discrete :
Proof. intros ? [??]; apply _. Qed.
End ofe.
Arguments namespace_mapO : clear implicits.
Global Arguments namespace_mapO : clear implicits.
(* Camera *)
Section cmra.
......@@ -296,5 +296,5 @@ Proof.
Qed.
End cmra.
Arguments namespace_mapR : clear implicits.
Arguments namespace_mapUR : clear implicits.
Global Arguments namespace_mapR : clear implicits.
Global Arguments namespace_mapUR : clear implicits.
......@@ -50,14 +50,14 @@ Structure ofeT := OfeT {
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car
}.
Arguments OfeT _ {_ _} _.
Global Arguments OfeT _ {_ _} _.
Add Printing Constructor ofeT.
Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
Arguments ofe_car : simpl never.
Arguments ofe_equiv : simpl never.
Arguments ofe_dist : simpl never.
Arguments ofe_mixin : simpl never.
Global Arguments ofe_car : simpl never.
Global Arguments ofe_equiv : simpl never.
Global Arguments ofe_dist : simpl never.
Global Arguments ofe_mixin : simpl never.
(** When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
we need Coq to *infer* the canonical OFE instance of a given type and take the
......@@ -100,7 +100,7 @@ Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
(** Discrete OFEs and discrete OFE elements *)
Class Discrete {A : ofeT} (x : A) := discrete y : x {0} y x y.
Arguments discrete {_} _ {_} _ _.
Global Arguments discrete {_} _ {_} _ _.
Global Hint Mode Discrete + ! : typeclass_instances.
Global Instance: Params (@Discrete) 1 := {}.
......@@ -111,8 +111,8 @@ Record chain (A : ofeT) := {
chain_car :> nat A;
chain_cauchy n i : n i chain_car i {n} chain_car n
}.
Arguments chain_car {_} _ _.
Arguments chain_cauchy {_} _ _ _ _.
Global Arguments chain_car {_} _ _.
Global Arguments chain_cauchy {_} _ _ _ _.
Program Definition chain_map {A B : ofeT} (f : A B)
`{!NonExpansive f} (c : chain A) : chain B :=
......@@ -124,7 +124,7 @@ Class Cofe (A : ofeT) := {
compl : Compl A;
conv_compl n c : compl c {n} c n;
}.
Arguments compl : simpl never.
Global Arguments compl : simpl never.
Global Hint Mode Cofe ! : typeclass_instances.
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A B) c `(NonExpansive f) :
......@@ -200,7 +200,7 @@ End ofe.
(** Contractive functions *)
Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x {n} y end.
Arguments dist_later _ _ !_ _ _ /.
Global Arguments dist_later _ _ !_ _ _ /.
Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
......@@ -321,7 +321,7 @@ Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Definition fixpoint := fixpoint_aux.(unseal).
Arguments fixpoint {A _ _} f {_}.
Global Arguments fixpoint {A _ _} f {_}.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Section fixpoint.
......@@ -529,7 +529,7 @@ Record ofe_mor (A B : ofeT) : Type := OfeMor {
ofe_mor_car :> A B;
ofe_mor_ne : NonExpansive ofe_mor_car
}.
Arguments OfeMor {_ _} _ {_}.
Global Arguments OfeMor {_ _} _ {_}.
Add Printing Constructor ofe_mor.
Existing Instance ofe_mor_ne.
......@@ -581,7 +581,7 @@ Section ofe_mor.
Proof. done. Qed.