Library Coq.Compat.Coq817


Compatibility file for making Coq act similar to Coq v8.17


Require Export Coq.Compat.Coq818.

Require Coq.Lists.ListSet.

Module Export Coq.
  Module Export Lists.
    Module Export ListSet.
      Import List ListSet.
      Local Lemma Private_set_diff_nodup :
        forall (A:Type) (Aeq_dec : forall x y:A, {x = y} + {x <> y}) l l',
         NoDup l -> NoDup l' -> NoDup (set_diff Aeq_dec l l').
      #[deprecated(since="8.18", note="The NoDup assumption for the second list has been dropped, please adjust uses of the lemma")]
      Notation set_diff_nodup := Private_set_diff_nodup.
    End ListSet.
  End Lists.
End Coq.