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.
      #[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.