adapt for Coq 8.9.0

thtuerk · Sep 19, 2019 · 437aff0 · 437aff0
1 parent ca02fad
commit 437aff0
Show file tree

Hide file tree

Showing 8 changed files with 7,570 additions and 1,773 deletions.
diff --git a/MSetIntervals.v b/MSetIntervals.v
@@ -4536,7 +4536,6 @@ Lemma elementsZ_insert_intervalZ_guarded : forall x c s,
   Proof.
     intros s.
     case s => //=.
-    split => //.
   Qed.
 
   Lemma compare_eq_Lt_nil_r : forall s,