(* *)
(**************************************************************************)
-include "ordered_set.ma".
+include "dama/ordered_set.ma".
(* Definition 2.2, setoid *)
record bishop_set: Type ≝ {
notation > "s 'squareB'" non associative with precedence 90
for @{ 'squareB $s }.
interpretation "bishop set square" 'squareB x = (square_bishop_set x).
-interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).