diff --git a/_CoqProject b/_CoqProject index e2d75403e6d9b1f7354f311cd4931cc912cc4122..b4f5b22a8deb3058cc40a9aebb00518c6b07f78f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,5 @@ -Q theories iron --arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files +-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-undeclared-scope,-convert_concl_no_check theories/algebra/ufrac_auth.v theories/bi/fracpred.v theories/proofmode/fracpred.v diff --git a/theories/bi/fracpred.v b/theories/bi/fracpred.v index 5cff46f7a3e1d75ca36d2e32f364fa17c5bfead8..e19b99d3cb8631dd99b05205dbe5af6ac02ec4b0 100644 --- a/theories/bi/fracpred.v +++ b/theories/bi/fracpred.v @@ -35,7 +35,7 @@ Section ofe. Lemma fracPred_ofe_mixin : OfeMixin (fracPred PROP). Proof. - refine (iso_ofe_mixin (λ P : fracPred _, P : _ -c> _) _ _); + refine (iso_ofe_mixin (λ P : fracPred PROP, P : _ -c> _) _ _); (split; [by destruct 1|by constructor]). Qed. Canonical Structure fracPredC : ofeT := OfeT (fracPred PROP) fracPred_ofe_mixin.