diff --git a/_CoqProject b/_CoqProject
index 2dfd79d44a04174b594ee6101522116ab8b626a3..567c5dd8bec1847aea1e4a04652f730442352b1c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,6 +53,7 @@ stdpp/nat_cancel.v
 stdpp/namespaces.v
 stdpp/telescopes.v
 stdpp/binders.v
+stdpp/ssreflect.v
 
 stdpp_unstable/bitblast.v
 stdpp_unstable/bitvector.v
diff --git a/stdpp/ssreflect.v b/stdpp/ssreflect.v
new file mode 100644
index 0000000000000000000000000000000000000000..0361cc017bf36e36f96943778a407bb3be2efc05
--- /dev/null
+++ b/stdpp/ssreflect.v
@@ -0,0 +1,14 @@
+(** This file provides support for using std++ in combination with the ssreflect
+tactics. It patches up some global options of ssreflect. *)
+From Coq.ssr Require Export ssreflect.
+From stdpp Require Export prelude.
+From stdpp Require Import options.
+
+(** Restore Coq's normal "if" scope, ssr redefines it. *)
+Global Open Scope general_if_scope.
+
+(** See Coq issue #5706 *)
+Global Set SsrOldRewriteGoalsOrder.
+
+(** Overwrite ssr's [done] tactic with ours *)
+Ltac done := stdpp.tactics.done.