4 files changed, 16 insertions, 15 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index c2316689fc..d86112abc0 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,7 +26,7 @@ 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.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index cf42ed18db..5ae933d433 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -257,6 +257,7 @@ Ltac blocked t := block_goal ; t ; unblock_goal.
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
    principles for things in [Prop] which are not automatically generated. *)
 
+#[universes(template)]
 Class DependentEliminationPackage (A : Type) :=
   { elim_type : Type ; elim : elim_type }.
 
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 1c89b6c3b1..ae366204ac 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -73,10 +73,10 @@ Proof.
   simpl.
   split ; intros ; subst.
 
-  inversion H.
-  reflexivity.
+  - inversion H.
+    reflexivity.
 
-  pi.
+  - pi.
 Qed.
 
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 8479b9a2bb..092c1d6f48 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -97,20 +97,20 @@ Section Measure_well_founded.
   Proof with auto.
     unfold well_founded.
     cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
-      intros.
+    + intros.
       apply (H (m a))...
-    apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
-    intros.
-    apply Acc_intro.
-    intros.
-    unfold MR in H1.
-    rewrite H0 in H1.
-    apply (H (m y))...
+    + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
+      intros.
+      apply Acc_intro.
+      intros.
+      unfold MR in H1.
+      rewrite H0 in H1.
+      apply (H (m y))...
   Defined.
 
 End Measure_well_founded.
 
-Hint Resolve measure_wf.
+Hint Resolve measure_wf : core.
 
 Section Fix_rects.
 
@@ -245,8 +245,8 @@ Module WfExtensionality.
     intros ; apply Fix_eq ; auto.
     intros.
     assert(f = g).
-    extensionality y ; apply H.
-    rewrite H0 ; auto.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
   Qed.
 
   (** Tactic to unfold once a definition based on [Fix_sub]. *)