Commit 102189ac authored by Ralf Jung's avatar Ralf Jung

restore compatibility with Coq 8.10

parent ef305cd2
Pipeline #33428 passed with stage
in 14 minutes and 41 seconds
-Q theories orc11
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
# Non-canonical projections require Coq 8.11.
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
theories/base.v
theories/value.v
......
......@@ -393,36 +393,21 @@ Structure latticeT : Type := Make_Lat {
lat_ty :> Type;
lat_equiv : Equiv lat_ty;
lat_sqsubseteq : SqSubsetEq lat_ty;
#[canonical(false)]
lat_join : Join lat_ty;
#[canonical(false)]
lat_meet : Meet lat_ty;
#[canonical(false)]
lat_inhabited : Inhabited lat_ty;
#[canonical(false)]
lat_sqsubseteq_proper : Proper (() ==> () ==> iff) ();
#[canonical(false)]
lat_join_proper : Proper (() ==> () ==> ()) ();
#[canonical(false)]
lat_meet_proper : Proper (() ==> () ==> ()) ();
#[canonical(false)]
lat_equiv_equivalence : Equivalence ();
#[canonical(false)]
lat_pre_order : PreOrder (@{lat_ty});
#[canonical(false)]
lat_sqsubseteq_antisym : AntiSymm () ();
#[canonical(false)]
lat_join_sqsubseteq_l (X Y : lat_ty) : X X Y;
#[canonical(false)]
lat_join_sqsubseteq_r (X Y : lat_ty) : Y X Y;
#[canonical(false)]
lat_join_lub (X Y Z : lat_ty) : X Z Y Z X Y Z;
#[canonical(false)]
lat_meet_sqsubseteq_l (X Y : lat_ty) : X Y X;
#[canonical(false)]
lat_meet_sqsubseteq_r (X Y : lat_ty) : X Y Y;
#[canonical(false)]
lat_meet_glb (X Y Z : lat_ty) : X Y X Z X Y Z
}.
Arguments lat_equiv : simpl never.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment