Commit a47f27d4 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compilation against Coq master.

parent 03de4677
Pipeline #16787 failed with stage
in 17 minutes and 46 seconds
-Q theories iron -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/algebra/ufrac_auth.v
theories/bi/fracpred.v theories/bi/fracpred.v
theories/proofmode/fracpred.v theories/proofmode/fracpred.v
......
...@@ -35,7 +35,7 @@ Section ofe. ...@@ -35,7 +35,7 @@ Section ofe.
Lemma fracPred_ofe_mixin : OfeMixin (fracPred PROP). Lemma fracPred_ofe_mixin : OfeMixin (fracPred PROP).
Proof. Proof.
refine (iso_ofe_mixin (λ P : fracPred _, P : _ -c> _) _ _); refine (iso_ofe_mixin (λ P : fracPred PROP, P : _ -c> _) _ _);
(split; [by destruct 1|by constructor]). (split; [by destruct 1|by constructor]).
Qed. Qed.
Canonical Structure fracPredC : ofeT := OfeT (fracPred PROP) fracPred_ofe_mixin. Canonical Structure fracPredC : ofeT := OfeT (fracPred PROP) fracPred_ofe_mixin.
......
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