4 files changed, 16 insertions, 5 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index f55093ed48..d86112abc0 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,7 +26,9 @@ Arguments id {A} x.
 Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
-Hint Unfold compose.
+Hint Unfold compose : core.
+
+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..001e1cfb01 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -237,6 +237,8 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i
 
 Definition fix_proto {A : Type} (a : A) := a.
 
+Register fix_proto as program.tactic.fix_proto.
+
 Ltac destruct_rec_calls :=
   match goal with
     | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H
@@ -326,8 +328,10 @@ 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.
 
 Definition obligation (A : Type) {a : A} := a.
+
+Register obligation as program.tactics.obligation.
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.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 6278798543..f9d23e3cf6 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -32,6 +32,8 @@ Section Well_founded.
 
   Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
 
+  Register Fix_sub as program.wf.fix_sub.
+
   (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
   (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)
 
@@ -89,6 +91,8 @@ Section Measure_well_founded.
 
   Definition MR (x y: T): Prop := R (m x) (m y).
 
+  Register MR as program.wf.mr.
+
   Lemma measure_wf: well_founded MR.
   Proof with auto.
     unfold well_founded.
@@ -106,7 +110,7 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
-Hint Resolve measure_wf.
+Hint Resolve measure_wf : core.
 
 Section Fix_rects.