diff --git a/theories/algebra/base.v b/theories/algebra/base.v deleted file mode 100644 index 603e9c20cebe850070a8c639514fcc2949b87a97..0000000000000000000000000000000000000000 --- a/theories/algebra/base.v +++ /dev/null @@ -1,6 +0,0 @@ -From Coq.ssr Require Export ssreflect. -From stdpp Require Export prelude. -Set Default Proof Using "Type". -Global Open Scope general_if_scope. -Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *) -Ltac done := stdpp.tactics.done.