3 files changed, 6 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index f55093ed48..c2316689fc 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) :=
 
 Hint Unfold compose.
 
+Declare Scope program_scope.
+
 Notation " g ∘ f " := (compose g f)
   (at level 40, left associativity) : program_scope.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index bc83881849..edbae6534a 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -326,7 +326,7 @@ Ltac program_solve_wf :=
 
 Create HintDb program discriminated.
 
-Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf.
+Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf.
 
 Obligation Tactic := program_simpl.
 
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 78c36dc7d1..c51cacac68 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -20,12 +20,13 @@ Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident, at level 10) : type_scope.
 
+Declare Scope program_scope.
+Delimit Scope program_scope with prg.
+
 (** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _) : program_scope.
 
-Delimit Scope program_scope with prg.
-
 (** Abbreviation for first projection and hiding of proofs of subset objects. *)
 
 Notation " `  t " := (proj1_sig t) (at level 10, t at next level) : program_scope.