fix: minor

Event-Structures · Jun 13, 2021 · 157666e · 157666e
1 parent e0c0e92
commit 157666e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/concur/porf_eventstruct.v b/theories/concur/porf_eventstruct.v
@@ -1128,7 +1128,7 @@ Lemma prime_inj : injective (porf_eventstruct_of).
 Proof. exact: val_inj. Qed.
 
 Lemma rf_ncf_dom_es (es : prime_porf_eventstruct) : rf_ncf_dom es.
-Proof. by case: es. Qed.
+Proof. by case: es=> /= ? /andP[]. Qed.
 
 Variable (es : prime_porf_eventstruct).