base.v 237 Bytes
Newer Older
1
From Coq.ssr Require Export ssreflect.
Ralf Jung's avatar
Ralf Jung committed
2
From stdpp Require Export prelude.
3
Set Default Proof Using "Type".
4
Global Open Scope general_if_scope.
5
Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ralf Jung's avatar
Ralf Jung committed
6
Ltac done := stdpp.tactics.done.