diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index 39e0452049fe..2f9cae304083 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -31,17 +31,16 @@ Set Inline Level 50.
 (** All operations are well-defined (trivial here since eq is Leibniz) *)
 
 Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
-Local Obligation Tactic := simpl_relation.
-#[global] Program Instance succ_wd : Proper (eq==>eq) S.
-#[global] Program Instance pred_wd : Proper (eq==>eq) pred.
-#[global] Program Instance add_wd : Proper (eq==>eq==>eq) plus.
-#[global] Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
-#[global] Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
-#[global] Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
-#[global] Program Instance div_wd : Proper (eq==>eq==>eq) div.
-#[global] Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
-#[global] Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
-#[global] Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit.
+#[global] Instance succ_wd : Proper (eq==>eq) S := _.
+#[global] Instance pred_wd : Proper (eq==>eq) pred := _.
+#[global] Instance add_wd : Proper (eq==>eq==>eq) plus := _.
+#[global] Instance sub_wd : Proper (eq==>eq==>eq) minus := _.
+#[global] Instance mul_wd : Proper (eq==>eq==>eq) mult := _.
+#[global] Instance pow_wd : Proper (eq==>eq==>eq) pow := _.
+#[global] Instance div_wd : Proper (eq==>eq==>eq) div := _.
+#[global] Instance mod_wd : Proper (eq==>eq==>eq) modulo := _.
+#[global] Instance lt_wd : Proper (eq==>eq==>iff) lt := _.
+#[global] Instance testbit_wd : Proper (eq==>eq==>eq) testbit := _.
 
 (** Bi-directional induction. *)
 
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index 8e5662b053fa..6a2b0b5db496 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.v
@@ -26,7 +26,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Generalizable Variables A R eqA B S eqB.
-Local Obligation Tactic := try solve [simpl_crelation].
 
 Local Open Scope signatureT_scope.
 
@@ -54,18 +53,13 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 (** Shortcuts to make proof search easier. *)
 
 #[global]
-Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
+Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv := _.
 
 #[global]
-Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
+Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv := _.
 
 #[global]
-Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
-
-  Next Obligation.
-  Proof. intros A R sa x y z Hxy Hyz.
-         now transitivity y.
-  Qed.
+Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv := _.
 
 Arguments equiv_symmetric {A R} sa x y : rename.
 Arguments equiv_transitive {A R} sa x y z : rename.
@@ -119,14 +113,13 @@ Section Respecting.
                           eqb : Equivalence B (R' : crelation B)) : Type :=
     { morph : A -> B & respectful R R' morph morph }.
 
-  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
+  Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => 
                    forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)).
-
-  Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl.
-
-  Next Obligation.
   Proof. 
+    split.
+    { unfold respecting in * ; simpl_crelation ; program_simpl. }
+    { unfold respecting in * ; simpl_crelation ; program_simpl. }
     intros. intros f g h H H' x y Rxy.
     unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
   Qed.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index bedd66bd5401..453e0b0e059a 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -19,7 +19,6 @@ Require Import Stdlib.Program.Tactics.
 Require Export Stdlib.Classes.CRelationClasses.
 
 Generalizable Variables A eqA B C D R RA RB RC m f x y.
-Local Obligation Tactic := try solve [ simpl_crelation ].
 
 Local Arguments transitivity {A R Transitive x} y {z}.
 
@@ -277,11 +276,10 @@ Section GenericInstances.
   (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
   
-  Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
-
-  Next Obligation.
+  Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
   Proof with auto.
-    intros A R H B R' H0 x y z X X0 x0 y0 X1.
+    split. { simpl_crelation. }
+    intros x y z X X0 x0 y0 X1.
     assert(R x0 x0).
     - eapply transitivity with y0... now apply symmetry.
     - eapply transitivity with (y x0)...
@@ -292,13 +290,11 @@ Section GenericInstances.
   (** The complement of a crelation conserves its proper elements. *)
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
-  Program Definition flip_proper
+  Definition flip_proper
           `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
-    Proper (RB ==> RA ==> RC) (flip f) := _.
-  
-  Next Obligation.
+    Proper (RB ==> RA ==> RC) (flip f).
   Proof.
-    intros A B C RA RB RC f mor x y X x0 y0 X0.
+    intros x y X x0 y0 X0.
     apply mor ; auto.
   Qed.
 
@@ -306,64 +302,52 @@ Section GenericInstances.
   (** Every Transitive crelation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)
   
-  Global Program 
+  Global
   Instance trans_contra_co_type_morphism
     `(Transitive A R) : Proper (R --> R ++> arrow) R.
-  
-  Next Obligation.
   Proof with auto.
-    intros A R H x y X x0 y0 X0 X1.
+    intros x y X x0 y0 X0 X1.
     apply transitivity with x...
     apply transitivity with x0...
   Qed.
 
   (** Proper declarations for partial applications. *)
 
-  Global Program 
+  Global
   Instance trans_contra_inv_impl_type_morphism
   `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x x0 y X X0.
+    intros x0 y X X0.
     apply transitivity with y...
   Qed.
 
-  Global Program 
+  Global
   Instance trans_co_impl_type_morphism
     `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x x0 y X X0.
+    intros x0 y X X0.
     apply transitivity with x0...
   Qed.
 
-  Global Program 
+  Global
   Instance trans_sym_co_inv_impl_type_morphism
     `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x x0 y X X0.
+    intros x0 y X X0.
     apply transitivity with y... apply symmetry...
   Qed.
 
-  Global Program Instance trans_sym_contra_arrow_morphism
+  Global Instance trans_sym_contra_arrow_morphism
     `(PER A R) {x} : Proper (R --> arrow) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x x0 y X X0.
+    intros x0 y X X0.
     apply transitivity with x0... apply symmetry...
   Qed.
 
-  Global Program Instance per_partial_app_type_morphism
+  Global Instance per_partial_app_type_morphism
   `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x x0 y X.
+    intros x0 y X.
     split.
     - intros ; apply transitivity with x0...
     - intros.
@@ -373,24 +357,20 @@ Section GenericInstances.
 
   (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
 
-  Global Program 
+  Global
   Instance trans_co_eq_inv_arrow_morphism
   `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x y X y0 y1 e X0; destruct e.
+    intros x y X y0 y1 e X0; destruct e.
     apply transitivity with y...
   Qed.
 
   (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
 
-  Global Program 
+  Global
   Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1.
-
-  Next Obligation.
   Proof with auto.
-    intros A R H x y X x0 y0 X0.
+    intros x y X x0 y0 X0.
     split ; intros.
     - apply transitivity with x0...
       apply transitivity with x... apply symmetry...
@@ -402,10 +382,8 @@ Section GenericInstances.
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
   Proof. firstorder. Qed.
 
-  Global Program Instance compose_proper A B C RA RB RC :
+  Global Instance compose_proper A B C RA RB RC :
     Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).
-
-  Next Obligation.
   Proof.
     simpl_crelation.
     unfold compose. firstorder. 
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index b5c927dd310b..c69fb769ebee 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -19,7 +19,6 @@
 
 Require Export Stdlib.Classes.Init.
 Require Import Stdlib.Program.Basics.
-Require Import Stdlib.Program.Tactics.
 
 Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
@@ -122,19 +121,19 @@ Section Defs.
     Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
     Proof. tauto. Qed.
     
-    Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
+    Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
       irreflexivity (R:=R).
     
-    Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
+    Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
       fun x y H => symmetry (R:=R) H.
     
-    Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
+    Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
       fun x y H H' => asymmetry (R:=R) H H'.
     
-    Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
+    Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
       fun x y z H H' => transitivity (R:=R) H' H.
 
-    Program Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
+    Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
       Antisymmetric eqA (flip R).
     Proof. firstorder. Qed.
 
@@ -191,7 +190,8 @@ Section Defs.
         The instance has low priority as it is always applicable
         if only the type is constrained. *)
     
-    Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+    Global Instance eq_equivalence : Equivalence (@eq A) | 10.
+    Proof. split; exact _. Qed.
   End Leibniz.
   
 End Defs.
@@ -273,18 +273,18 @@ Tactic Notation "apply" "*" constr(t) :=
   first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
     refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
 
+Require Import Stdlib.Program.Tactics.
+
 Ltac simpl_crelation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ dintuition auto with crelations ]).
 
-Local Obligation Tactic := simpl_crelation.
-
 (** Logical implication. *)
 
 #[global]
-Program Instance impl_Reflexive : Reflexive impl.
+Instance impl_Reflexive : Reflexive impl. Proof. simpl_crelation. Qed.
 #[global]
-Program Instance impl_Transitive : Transitive impl.
+Instance impl_Transitive : Transitive impl. Proof. simpl_crelation. Qed.
 
 (** Logical equivalence. *)
 
@@ -298,11 +298,11 @@ Instance iff_Transitive : Transitive iff := iff_trans.
 (** Logical equivalence [iff] is an equivalence crelation. *)
 
 #[global]
-Program Instance iff_equivalence : Equivalence iff. 
+Instance iff_equivalence : Equivalence iff. Proof. split; simpl_crelation. Qed.
 #[global]
-Program Instance arrow_Reflexive : Reflexive arrow.
+Instance arrow_Reflexive : Reflexive arrow. Proof. simpl_crelation. Qed.
 #[global]
-Program Instance arrow_Transitive : Transitive arrow.
+Instance arrow_Transitive : Transitive arrow. Proof. simpl_crelation. Qed.
 
 #[global]
 Instance iffT_Reflexive : Reflexive iffT. 
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 85aa2f756726..ba06636d6c6d 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -24,7 +24,6 @@ Require Export Stdlib.Classes.Equivalence.
 Require Import Stdlib.Logic.Decidable.
 Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Arith.Peano_dec.
-Require Import Stdlib.Program.Program.
 
 Generalizable Variables A B R.
 
@@ -55,7 +54,7 @@ Local Open Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := 
+Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := 
           swap_sumbool (x == y).
 
 
@@ -80,80 +79,78 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
    which setoid we're talking about. *)
 
 #[global]
-Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
+Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
 
 #[global]
-Program Instance bool_eqdec : EqDec bool eq := bool_dec.
+Instance bool_eqdec : EqDec bool eq := bool_dec.
 
 #[global]
-Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
-
-  Next Obligation.
-  Proof.
-    do 2 match goal with [ x : () |- _ ] => destruct x end.
-    reflexivity.
-  Qed.
-
-#[global] Obligation Tactic := unfold complement, equiv ; program_simpl.
-#[export] Obligation Tactic := unfold complement, equiv ; program_simpl.
+Instance unit_eqdec : EqDec unit eq.
+Proof.
+  refine (fun x y => left _).
+  abstract (case x, y; reflexivity).
+Defined.
 
 #[global]
-Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
-  EqDec (prod A B) eq :=
-  { equiv_dec x y :=
+Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
+  EqDec (prod A B) eq.
+Proof.
+  refine (fun x y =>
     let '(x1, x2) := x in
     let '(y1, y2) := y in
     if x1 == y1 then
-      if x2 == y2 then in_left
-      else in_right
-    else in_right }.
+      if x2 == y2 then left _
+      else right _
+    else right _ ).
+  all : abstract (cbv [complement equiv] in *; congruence).
+Defined.
 
 #[global]
-Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
-  EqDec (sum A B) eq := {
-  equiv_dec x y :=
+Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
+  EqDec (sum A B) eq.
+Proof.
+  refine (fun x y =>
     match x, y with
-      | inl a, inl b => if a == b then in_left else in_right
-      | inr a, inr b => if a == b then in_left else in_right
-      | inl _, inr _ | inr _, inl _ => in_right
-    end }.
+      | inl a, inl b => if a == b then left _ else right _
+      | inr a, inr b => if a == b then left _ else right _
+      | inl _, inr _ | inr _, inl _ => right _
+    end ).
+  all : abstract (cbv [complement equiv] in *; congruence).
+Defined.
 
 (** Objects of function spaces with countable domains like bool have decidable
   equality. Proving the reflection requires functional extensionality though. *)
+Require Import FunctionalExtensionality.
 
 #[global]
-Program Instance bool_function_eqdec `(EqDec A eq) : EqDec (bool -> A) eq :=
-  { equiv_dec f g :=
+Instance bool_function_eqdec `(EqDec A eq) : EqDec (bool -> A) eq.
+Proof.
+  refine (fun f g =>
     if f true == g true then
-      if f false == g false then in_left
-      else in_right
-    else in_right }.
-
-  Next Obligation.
-  Proof.
-    extensionality x.
-    destruct x ; auto.
-  Qed.
+      if f false == g false then left _
+      else right _
+    else right _ ).
+  all : cbv [complement equiv] in *; try abstract congruence.
+  abstract (extensionality x; case x; trivial).
+Defined.
 
 Require Import List.
 
 #[global]
-Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
-  { equiv_dec :=
+Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq.
+  refine (
     fix aux (x y : list A) :=
     match x, y with
-      | nil, nil => in_left
+      | nil, nil => left _
       | cons hd tl, cons hd' tl' =>
         if hd == hd' then
-          if aux tl tl' then in_left else in_right
-          else in_right
-      | _, _ => in_right
-    end }.
-
-  Next Obligation.
-    match goal with y : list _ |- _ => destruct y end ;
-    unfold not in *; eauto.
-  Defined.
-
-  Solve Obligations with unfold equiv, complement in * ; 
-    program_simpl ; intuition (discriminate || eauto).
+          if aux tl tl' then left _ else right _
+          else right _
+      | _, _ => right _
+    end ).
+  all : abstract (cbv [complement equiv] in *; congruence).
+Defined.
+
+Require Import Stdlib.Program.Program. (* for compat *)
+#[global] Obligation Tactic := unfold complement, equiv ; program_simpl.
+#[export] Obligation Tactic := unfold complement, equiv ; program_simpl.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index b5a461284494..f1d0fd5aeb85 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -26,7 +26,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Generalizable Variables A R eqA B S eqB.
-Local Obligation Tactic := try solve [simpl_relation].
 
 Local Open Scope signature_scope.
 
@@ -54,19 +53,13 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 (** Shortcuts to make proof search easier. *)
 
 #[global]
- Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1.
+Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1 := _.
 
 #[global]
-Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1.
+Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1 := _.
 
 #[global]
-Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
-
-  Next Obligation.
-  Proof.
-    intros A R sa x y z Hxy Hyz.
-    now transitivity y.
-  Qed.
+Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1 := _.
 
 Arguments equiv_symmetric {A R} sa x y : rename.
 Arguments equiv_transitive {A R} sa x y z : rename.
@@ -120,14 +113,13 @@ Section Respecting.
                           eqb : Equivalence B (R' : relation B)) : Type :=
     { morph : A -> B | respectful R R' morph morph }.
 
-  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
+  Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => 
                    forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
-
-  Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl.
-
-  Next Obligation.
-  Proof. 
+  Proof.
+    split.
+    { unfold respecting in * ; simpl_relation ; program_simpl. }
+    { unfold respecting in * ; simpl_relation ; program_simpl. }
     intros. intros f g h H H' x y Rxy.
     unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
   Qed.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index ff7016c5097d..b66b6f77cb59 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -15,12 +15,10 @@
 *)
 
 Require Import Stdlib.Program.Basics.
-Require Import Stdlib.Program.Tactics.
 Require Import Stdlib.Relations.Relation_Definitions.
 Require Export Stdlib.Classes.RelationClasses.
 
 Generalizable Variables A eqA B C D R RA RB RC m f x y.
-Local Obligation Tactic := try solve [ simpl_relation ].
 
 (** * Morphisms.
 
@@ -337,11 +335,10 @@ Section GenericInstances.
   (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
   
-  Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
-
-  Next Obligation.
+  Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
   Proof with auto.
-    intros R H R' H0 x y z H1 H2 x0 y0 H3.
+    split. { simpl_relation. }
+    intros x y z H1 H2 x0 y0 H3.
     assert(R x0 x0).
     - transitivity y0... symmetry...
     - transitivity (y x0)...
@@ -349,91 +346,75 @@ Section GenericInstances.
 
   (** The complement of a relation conserves its proper elements. *)
   
-  Program Definition complement_proper
+  Definition complement_proper
           `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-    Proper (RA ==> RA ==> iff) (complement R) := _.
-  
-  Next Obligation.
+    Proper (RA ==> RA ==> iff) (complement R).
   Proof.
-    intros RA R mR x y H x0 y0 H0.
+    intros x y H x0 y0 H0.
     unfold complement.
     pose (mR x y H x0 y0 H0).
-    intuition.
+    intuition idtac.
   Qed.
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
 
-  Program Definition flip_proper
+  Definition flip_proper
           `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
-    Proper (RB ==> RA ==> RC) (flip f) := _.
-  
-  Next Obligation.
+    Proper (RB ==> RA ==> RC) (flip f).
   Proof.
-    intros RA RB RC f mor x y H x0 y0 H0; apply mor ; auto.
+    intros x y H x0 y0 H0; apply mor ; auto.
   Qed.
 
 
   (** Every Transitive relation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)
   
-  Global Program 
+  Global
   Instance trans_contra_co_morphism
     `(Transitive A R) : Proper (R --> R ++> impl) R.
-  
-  Next Obligation.
   Proof with auto.
-    intros R H x y H0 x0 y0 H1 H2.
+    intros x y H0 x0 y0 H1 H2.
     transitivity x...
     transitivity x0...
   Qed.
 
   (** Proper declarations for partial applications. *)
 
-  Global Program 
+  Global
   Instance trans_contra_inv_impl_morphism
   `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x x0 y H0 H1.
+    intros x0 y H0 H1.
     transitivity y...
   Qed.
 
-  Global Program 
+  Global
   Instance trans_co_impl_morphism
     `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x x0 y H0 H1.
+    intros x0 y H0 H1.
     transitivity x0...
   Qed.
 
-  Global Program 
+  Global
   Instance trans_sym_co_inv_impl_morphism
     `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x x0 y H0 H1.
+    intros x0 y H0 H1.
     transitivity y... symmetry...
   Qed.
 
-  Global Program Instance trans_sym_contra_impl_morphism
+  Global Instance trans_sym_contra_impl_morphism
     `(PER A R) {x} : Proper (R --> impl) (R x) | 3.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x x0 y H0 H1.
+    intros x0 y H0 H1.
     transitivity x0... symmetry...
   Qed.
 
-  Global Program Instance per_partial_app_morphism
+  Global Instance per_partial_app_morphism
   `(PER A R) {x} : Proper (R ==> iff) (R x) | 2.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x x0 y H0.
+    intros x0 y H0.
     split.
     - intros ; transitivity x0...
     - intros.
@@ -443,24 +424,20 @@ Section GenericInstances.
 
   (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
 
-  Global Program 
+  Global
   Instance trans_co_eq_inv_impl_morphism
   `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x y H0 y0 y1 e H2; destruct e.
+    intros x y H0 y0 y1 e H2; destruct e.
     transitivity y...
   Qed.
 
   (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-  Global Program 
+  Global
   Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
-
-  Next Obligation.
   Proof with auto.
-    intros R H x y H0 x0 y0 H1.
+    intros x y H0 x0 y0 H1.
     split ; intros.
     - transitivity x0... transitivity x... symmetry...
 
@@ -470,12 +447,10 @@ Section GenericInstances.
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
   Proof. firstorder. Qed.
 
-  Global Program Instance compose_proper RA RB RC :
+  Global Instance compose_proper RA RB RC :
     Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).
-
-  Next Obligation.
   Proof.
-    intros RA RB RC x y H x0 y0 H0 x1 y1 H1.
+    intros x y H x0 y0 H0 x1 y1 H1.
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
@@ -805,3 +780,5 @@ Register apply_subrelation as rewrite.prop.apply_subrelation.
 Register RewriteRelation as rewrite.prop.RewriteRelation.
 Register Proper as rewrite.prop.Proper.
 Register ProperProxy as rewrite.prop.ProperProxy.
+
+Require Stdlib.Program.Tactics. (* for compat *)
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index c6905df63e27..e6915cdae6ed 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -16,71 +16,81 @@
 
 Require Import Stdlib.Classes.Morphisms.
 Require Import Stdlib.Program.Basics.
-Require Import Stdlib.Program.Tactics.
-
-Local Obligation Tactic := try solve [simpl_relation | firstorder auto].
 
 (** Standard instances for [not], [iff] and [impl]. *)
 
 (** Logical negation. *)
 
 #[global]
-Program Instance not_impl_morphism :
+Instance not_impl_morphism :
   Proper (impl --> impl) not | 1.
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance not_iff_morphism :
+Instance not_iff_morphism :
   Proper (iff ++> iff) not.
+Proof. firstorder idtac. Qed.
 
 (** Logical conjunction. *)
 
 #[global]
-Program Instance and_impl_morphism :
+Instance and_impl_morphism :
   Proper (impl ==> impl ==> impl) and | 1.
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance and_iff_morphism :
+Instance and_iff_morphism :
   Proper (iff ==> iff ==> iff) and.
+Proof. firstorder idtac. Qed.
 
 (** Logical disjunction. *)
 
 #[global]
-Program Instance or_impl_morphism :
+Instance or_impl_morphism :
   Proper (impl ==> impl ==> impl) or | 1.
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance or_iff_morphism :
+Instance or_iff_morphism :
   Proper (iff ==> iff ==> iff) or.
+Proof. firstorder idtac. Qed.
 
 (** Logical implication [impl] is a morphism for logical equivalence. *)
 
 #[global]
-Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl.
+Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl.
+Proof. firstorder idtac. Qed.
 
 (** Morphisms for quantifiers *)
 
 #[global]
-Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A).
+Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A).
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance ex_impl_morphism {A : Type} :
+Instance ex_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@ex A) | 1.
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance ex_flip_impl_morphism {A : Type} :
+Instance ex_flip_impl_morphism {A : Type} :
   Proper (pointwise_relation A (flip impl) ==> flip impl) (@ex A) | 1.
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance all_iff_morphism {A : Type} :
+Instance all_iff_morphism {A : Type} :
   Proper (pointwise_relation A iff ==> iff) (@all A).
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance all_impl_morphism {A : Type} :
+Instance all_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
+Proof. firstorder idtac. Qed.
 
 #[global]
-Program Instance all_flip_impl_morphism {A : Type} :
+Instance all_flip_impl_morphism {A : Type} :
   Proper (pointwise_relation A (flip impl) ==> flip impl) (@all A) | 1.
+Proof. firstorder idtac. Qed.
 
 (** Equivalent points are simultaneously accessible or not *)
 
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index c38d34cefb9f..0f6481e17d3e 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -16,7 +16,7 @@
 
 Require Import Relation_Definitions.
 Require Import Stdlib.Classes.Morphisms.
-Require Import Stdlib.Program.Program.
+Require Import Stdlib.Program.Basics.
 
 Generalizable Variables A l.
 
@@ -59,3 +59,5 @@ Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))).
 Lemma flip_pointwise_relation A (R : relation A) :
   relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)).
 Proof. intros. split; firstorder. Qed.
+
+Require Stdlib.Program.Program. (* for compat *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index e46f9a14778c..6998dd2dbdd3 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -114,19 +114,19 @@ Section Defs.
     Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
     Proof. tauto. Qed.
     
-    Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
+    Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
       irreflexivity (R:=R).
     
-    Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
+    Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
       fun x y H => symmetry (R:=R) H.
     
-    Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
+    Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
       fun x y H H' => asymmetry (R:=R) H H'.
     
-    Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
+    Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
       fun x y z H H' => transitivity (R:=R) H' H.
 
-    Program Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
+    Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
       Antisymmetric eqA (flip R).
     Proof. firstorder. Qed.
 
@@ -179,7 +179,8 @@ Section Defs.
         The instance has low priority as it is always applicable
         if only the type is constrained. *)
     
-    Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+    Global Instance eq_equivalence : Equivalence (@eq A) | 10.
+    Proof. split; exact _. Defined.
   End Leibniz.
   
   (** Leibniz disequality. *)
@@ -289,14 +290,12 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ dintuition auto with relations ]).
 
-Local Obligation Tactic := try solve [ simpl_relation ].
-
 (** Logical implication. *)
 
 #[global]
-Program Instance impl_Reflexive : Reflexive impl.
+Instance impl_Reflexive : Reflexive impl. Proof. simpl_relation. Qed.
 #[global]
-Program Instance impl_Transitive : Transitive impl.
+Instance impl_Transitive : Transitive impl. Proof. simpl_relation. Qed.
 
 (** Logical equivalence. *)
 
@@ -310,7 +309,7 @@ Instance iff_Transitive : Transitive iff := iff_trans.
 (** Logical equivalence [iff] is an equivalence relation. *)
 
 #[global]
-Program Instance iff_equivalence : Equivalence iff.
+Instance iff_equivalence : Equivalence iff. Proof. split; exact _. Qed.
 
 (** We now develop a generalization of results on relations for arbitrary predicates.
    The resulting theory can be applied to homogeneous binary relations but also to
@@ -431,36 +430,28 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
 #[global]
-Program Instance predicate_equivalence_equivalence {l} :
+Instance predicate_equivalence_equivalence {l} :
   Equivalence (@predicate_equivalence l).
-
-  Next Obligation.
-    intro l; induction l ; firstorder.
-  Qed.
-  Next Obligation.
-    intro l; induction l ; firstorder.
-  Qed.
-  Next Obligation.
-    intro l.
-    fold pointwise_lifting.
-    induction l as [|T l IHl].
+Proof.
+  split.
+  { induction l ; firstorder. }
+  { induction l ; firstorder. }
+  { induction l as [|T l IHl].
     - firstorder.
     - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)).
-      firstorder.
-  Qed.
+      firstorder. }
+Qed.
 
 #[global]
-Program Instance predicate_implication_preorder {l} :
+Instance predicate_implication_preorder {l} :
   PreOrder (@predicate_implication l).
-  Next Obligation.
-    intro l; induction l ; firstorder.
-  Qed.
-  Next Obligation.
-    intro l.
-    induction l as [|T l IHl].
+Proof.
+  split.
+  { induction l ; firstorder. }
+  { induction l as [|T l IHl].
     - firstorder.
-    - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)). firstorder.
-  Qed.
+    - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)). firstorder. }
+Qed.
 
 (** We define the various operations which define the algebra on binary relations,
    from the general ones. *)
@@ -518,10 +509,8 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type
 (** The partial order defined by subrelation and relation equivalence. *)
 
 #[global]
-Program Instance subrelation_partial_order {A} :
+Instance subrelation_partial_order {A} :
   PartialOrder (@relation_equivalence A) subrelation.
-
-Next Obligation.
 Proof.
   unfold relation_equivalence in *. compute; firstorder.
 Qed.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 1f98a8769e75..8bdeef290ee9 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -119,8 +119,9 @@ Section RelProd_Instances.
            `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
   Proof. firstorder. Qed.
 
-  Global Program Instance RelProd_Equivalence 
+  Global Instance RelProd_Equivalence 
           `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
+  Proof. split; exact _. Qed.
 
   Lemma FstRel_ProdRel :
     relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index b17be647264b..f7441d1e0011 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -19,8 +19,6 @@ Unset Strict Implicit.
 
 Generalizable Variables A.
 
-Require Import Stdlib.Program.Program.
-
 Require Import Relation_Definitions.
 Require Export Stdlib.Classes.RelationClasses.
 Require Export Stdlib.Classes.Morphisms.
@@ -32,7 +30,7 @@ Class Setoid A := {
   #[global] setoid_equiv :: Equivalence equiv }.
 
 (* Too dangerous instance *)
-(* Program Instance [ eqa : Equivalence A eqA ] =>  *)
+(* Instance [ eqa : Equivalence A eqA ] =>  *)
 (*   equivalence_setoid : Setoid A := *)
 (*   equiv := eqA ; setoid_equiv := eqa. *)
 
@@ -56,11 +54,11 @@ Existing Instance setoid_trans.
 
 (** Standard setoids. *)
 
-(* Program Instance eq_setoid : Setoid A := *)
+(* Instance eq_setoid : Setoid A := *)
 (*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
 #[global]
-Program Instance iff_setoid : Setoid Prop :=
+Instance iff_setoid : Setoid Prop :=
   { equiv := iff ; setoid_equiv := iff_equivalence }.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
@@ -125,11 +123,11 @@ Ltac setoidify := repeat setoidify_tac.
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
 #[global]
-Program Instance setoid_morphism `(sa : Setoid A) : Proper (equiv ++> equiv ++> iff) equiv :=
+Instance setoid_morphism `(sa : Setoid A) : Proper (equiv ++> equiv ++> iff) equiv :=
   proper_prf.
 
 #[global]
-Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (equiv ++> iff) (equiv x) :=
+Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (equiv ++> iff) (equiv x) :=
   proper_prf.
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
@@ -141,7 +139,7 @@ Class PartialSetoid (A : Type) :=
 
 Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
+Require Stdlib.Program.Program. (* for compat *)
 (** Reset the default Program tactic. *)
-
-#[global] Obligation Tactic := program_simpl.
-#[export] Obligation Tactic := program_simpl.
+#[global] Obligation Tactic := Program.Tactics.program_simpl.
+#[export] Obligation Tactic := Program.Tactics.program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 7e6d9282d002..42f8f7100e7a 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -50,13 +50,11 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
     | right H => @left _ _ H
   end.
 
-Require Import Stdlib.Program.Program.
-
 Local Open Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -81,58 +79,58 @@ Require Import Stdlib.Arith.Arith.
   it by specifying which setoid we're talking about. *)
 
 #[global]
-Program Instance eq_setoid A : Setoid A | 10 :=
+Instance eq_setoid A : Setoid A | 10 :=
   { equiv := eq ; setoid_equiv := eq_equivalence }.
 
 #[global]
-Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
+Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
   eq_nat_dec.
 
 Require Import Stdlib.Bool.Bool.
 
 #[global]
-Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
+Instance bool_eqdec : EqDec (eq_setoid bool) :=
   bool_dec.
 
 #[global]
-Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
-  fun x y => in_left.
-
-  Next Obligation.
-  Proof.
-    do 2 match goal with x : () |- _ => destruct x end.
-    reflexivity.
-  Qed.
+Instance unit_eqdec : EqDec (eq_setoid unit).
+Proof.
+  refine (fun x y => left _).
+  abstract (case x, y; reflexivity).
+Defined.
 
 #[global]
-Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B))
- : EqDec (eq_setoid (prod A B)) :=
+Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B))
+ : EqDec (eq_setoid (prod A B)).
+Proof.
+  refine (
   fun x y =>
     let '(x1, x2) := x in
     let '(y1, y2) := y in
     if x1 == y1 then
-      if x2 == y2 then in_left
-      else in_right
-    else in_right.
-
-  Solve Obligations with unfold complement ; program_simpl.
+      if x2 == y2 then left _
+      else right _
+    else right _).
+  all : abstract (cbv [equiv eq_setoid] in *; congruence).
+Defined.
 
 (** Objects of function spaces with countable domains like bool
   have decidable equality. *)
+Require Import FunctionalExtensionality.
 
 #[global]
-Program Instance bool_function_eqdec `(! EqDec (eq_setoid A))
- : EqDec (eq_setoid (bool -> A)) :=
+Instance bool_function_eqdec `(! EqDec (eq_setoid A))
+ : EqDec (eq_setoid (bool -> A)).
+Proof.
+  refine (
   fun f g =>
     if f true == g true then
-      if f false == g false then in_left
-      else in_right
-    else in_right.
+      if f false == g false then left _
+      else right _
+    else right _).
 
-  Solve Obligations with try red ; unfold complement ; program_simpl.
+  all : cbv [equiv eq_setoid] in *; try abstract congruence.
+  abstract (extensionality x; destruct x; auto).
+Defined.
 
-  Next Obligation.
-  Proof.
-    extensionality x.
-    destruct x ; auto.
-  Qed.
+Require Stdlib.Program.Program. (* for compat *)
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index fc94e891e75f..0af10b5c3e2f 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -27,8 +27,8 @@
 
 *)
 
-Require Program.
 Require Import FMapInterface FMapList ZArith Int FMapAVL Lia.
+Require Program.Wf.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -686,28 +686,32 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Definition cardinal_e_2 ee :=
    (cardinal_e (fst ee) + cardinal_e (snd ee))%nat.
 
-  Local Unset Keyed Unification.
-
-  Program Fixpoint compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
-   { measure (cardinal_e_2 ee) } : comparison :=
-  match ee with
-  | (Raw.End _, Raw.End _) => Eq
-  | (Raw.End _, Raw.More _ _ _ _) => Lt
-  | (Raw.More _ _ _ _, Raw.End _) => Gt
-  | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
-      match X.compare x1 x2 with
-      | EQ _ => match D.compare d1 d2 with
-                | EQ _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2)
-                | LT _ => Lt
-                | GT _ => Gt
-                end
-      | LT _ => Lt
-      | GT _ => Gt
-      end
-  end.
-  Next Obligation.
-  intros; unfold cardinal_e_2; simpl;
-  abstract (do 2 rewrite cons_cardinal_e; lia ).
+  Definition compare_aux : Raw.enumeration D.t * Raw.enumeration D.t -> comparison.
+  Proof.
+    refine (@Init.Wf.Fix _ (Program.Wf.MR lt (cardinal_e_2 )) _ _
+      (fun ee (compare_aux : forall ee', cardinal_e_2 ee' < _ -> _) =>
+      (let (e, e0) as ee' return (ee' = ee -> _) := ee in
+      match e with
+      | Raw.End _ => match e0 with
+        | Raw.End _ => fun _ => Eq
+        | Raw.More _ _ _ _ => fun _ => Lt
+        end
+      | Raw.More x1 d1 r1 e => match e0 with
+        | Raw.End _ => fun _ => Gt
+        | Raw.More x2 d2 r2 e0 => fun H => match X.compare x1 x2 as c return c = _ -> _ with
+          | LT _ => fun _ => Lt
+          | EQ _ => fun _ => match D.compare d1 d2 as c return c = _ -> _ with
+            | LT _ => fun _ => Lt
+            | EQ _ => fun _ => compare_aux (Raw.cons r1 e, Raw.cons r2 e0) _
+            | GT _ => fun _ => Gt
+              end eq_refl
+          | GT _ => fun _ => Gt
+          end eq_refl
+        end
+      end) eq_refl)).
+    { apply Wf.measure_wf, Nat.lt_wf_0. }
+    { clear compare_aux e3 e4 e5 e6; intros; unfold cardinal_e_2; simpl;
+      abstract (subst; simpl; do 2 rewrite cons_cardinal_e; lia ). }
   Defined.
 
   Definition Cmp c :=
@@ -736,13 +740,8 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Lemma compare_aux_Cmp : forall e,
    Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).
   Proof.
-  intros e; unfold compare_aux.
-  match goal with [ |- context[Wf.Fix_sub _ _ _ _ ?f] ] => set (rec := f) end.
-  apply Wf.Fix_sub_rect.
-  + intros [[] []] g h Heq; simpl; try reflexivity.
-    repeat caseq; try reflexivity.
-    now apply Heq.
-  + intros [] IH wf; simpl.
+    induction e as [[]IH] using (well_founded_induction (Program.Wf.measure_wf Nat.lt_wf_0 cardinal_e_2));
+    cbv [compare_aux]; rewrite Fix_eq by (intros; repeat caseq; congruence).
     repeat caseq; simpl; try MX.elim_comp; auto.
     apply cons_Cmp; eauto.
     rewrite <- !cons_1; apply IH.
@@ -851,3 +850,4 @@ Module Make_ord (X: OrderedType)(D: OrderedType)
             with Module MapS.E := X
  :=IntMake_ord(Z_as_Int)(X)(D).
 
+Require Program. (* for compat *)
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index eb6f16cb2a6e..5e960fa9b1bf 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -70,17 +70,16 @@ Definition Odd n := exists m, n = 2*m+1.
 
 (** Proofs of morphisms, obvious since eq is Leibniz *)
 
-Local Obligation Tactic := simpl_relation.
-Program Definition succ_wd : Proper (eq==>eq) succ := _.
-Program Definition pred_wd : Proper (eq==>eq) pred := _.
-Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
-Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
-Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
-Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
-Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
-Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
-Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
-Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+Definition succ_wd : Proper (eq==>eq) succ := _.
+Definition pred_wd : Proper (eq==>eq) pred := _.
+Definition add_wd : Proper (eq==>eq==>eq) add := _.
+Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
+Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
+Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
+Definition div_wd : Proper (eq==>eq==>eq) div := _.
+Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
+Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
+Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
 (** Decidability of equality. *)
 
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 44d38c300038..f8b2d251df2b 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -65,18 +65,16 @@ Proof.
   intros x y z; apply eq_trans.
 Qed.
 
-Local Obligation Tactic := zcongruence.
-
 #[global]
-Program Instance succ_wd : Proper (eq ==> eq) succ.
+Instance succ_wd : Proper (eq ==> eq) succ. Proof. zcongruence. Qed.
 #[global]
-Program Instance pred_wd : Proper (eq ==> eq) pred.
+Instance pred_wd : Proper (eq ==> eq) pred. Proof. zcongruence. Qed.
 #[global]
-Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Instance add_wd : Proper (eq ==> eq ==> eq) add. Proof. zcongruence. Qed.
 #[global]
-Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Instance sub_wd : Proper (eq ==> eq ==> eq) sub. Proof. zcongruence. Qed.
 #[global]
-Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
+Instance mul_wd : Proper (eq ==> eq ==> eq) mul. Proof. zcongruence. Qed.
 
 Theorem gt_wB_1 : 1 < wB.
 Proof.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index e687b86fc6f2..02b70b427b07 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -234,7 +234,7 @@ Module WfExtensionality.
 
   (** For a function defined with Program using a well-founded order. *)
 
-  Program Lemma fix_sub_eq_ext :
+  Lemma fix_sub_eq_ext :
     forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
       (P : A -> Type)
       (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x),
diff --git a/theories/Strings/PString.v b/theories/Strings/PString.v
index 9d779b2eec3c..8d6b92639d8c 100644
--- a/theories/Strings/PString.v
+++ b/theories/Strings/PString.v
@@ -634,16 +634,18 @@ Module OT <: OrderedType.OrderedType with Definition t := string.
   Lemma lt_not_eq (s1 s2 : t) : lt s1 s2 -> not (eq s1 s2).
   Proof. unfold lt, eq. intros ->. discriminate. Qed.
 
-  #[program]
-  Definition compare (s1 s2 : t) : OrderedType.Compare lt eq s1 s2 :=
-    match compare s1 s2 with
-    | Eq => OrderedType.EQ _
-    | Lt => OrderedType.LT _
-    | Gt => OrderedType.GT _
-    end.
-  Next Obligation. symmetry. assumption. Defined.
-  Next Obligation. symmetry. assumption. Defined.
-  Next Obligation. unfold lt. rewrite compare_antisym, <-Heq_anonymous. reflexivity. Defined.
+  Definition compare (s1 s2 : t) : OrderedType.Compare lt eq s1 s2.
+  Proof.
+    refine (
+    match compare s1 s2 as c return c = _ -> _ with
+    | Eq => fun H => OrderedType.EQ _
+    | Lt => fun H => OrderedType.LT _
+    | Gt => fun H => OrderedType.GT _
+    end Logic.eq_refl).
+    { abstract (symmetry; assumption). }
+    { abstract (symmetry; assumption). }
+    { abstract (unfold lt; rewrite compare_antisym, <-H; reflexivity). }
+  Defined.
 
   Hint Immediate eq_sym : core.
   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 0930a8d0c1c9..fa8f66705afc 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -246,7 +246,7 @@ Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
 Definition t := O.t.
 Definition eq := O.eq.
 #[global]
-Program Instance eq_equiv : Equivalence eq.
+Instance eq_equiv : Equivalence eq. Proof. split; exact _. Qed.
 Definition eq_dec := O.eq_dec.
 
 Definition lt := flip O.lt.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 0f7dfc30cf09..a413a9aa6658 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -98,20 +98,19 @@ Defined.
 
 (** * Proofs of morphisms, obvious since eq is Leibniz *)
 
-Local Obligation Tactic := simpl_relation.
-Program Definition succ_wd : Proper (eq==>eq) succ := _.
-Program Definition pred_wd : Proper (eq==>eq) pred := _.
-Program Definition opp_wd : Proper (eq==>eq) opp := _.
-Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
-Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
-Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
-Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
-Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
-Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
-Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
-Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
-Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
-Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+Definition succ_wd : Proper (eq==>eq) succ := _.
+Definition pred_wd : Proper (eq==>eq) pred := _.
+Definition opp_wd : Proper (eq==>eq) opp := _.
+Definition add_wd : Proper (eq==>eq==>eq) add := _.
+Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
+Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
+Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
+Definition div_wd : Proper (eq==>eq==>eq) div := _.
+Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
+Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
+Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
+Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
+Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
 (** * Properties of [pos_sub] *)
 
diff --git a/theories/btauto/Algebra.v b/theories/btauto/Algebra.v
index 647eafff9d91..048db9d03c0e 100644
--- a/theories/btauto/Algebra.v
+++ b/theories/btauto/Algebra.v
@@ -128,23 +128,23 @@ End Definitions.
 
 Section Computational.
 
-Program Instance Decidable_PosEq : forall (p q : positive), Decidable (p = q) :=
-  { Decidable_witness := Pos.eqb p q }.
-Next Obligation.
-apply Pos.eqb_eq.
-Qed.
+Instance Decidable_PosEq : forall (p q : positive), Decidable (p = q).
+Proof.
+  intros; refine  {| Decidable_witness := Pos.eqb p q |}.
+  apply Pos.eqb_eq.
+Defined.
 
-Program Instance Decidable_PosLt : forall p q, Decidable (Pos.lt p q) :=
-  { Decidable_witness := Pos.ltb p q }.
-Next Obligation.
-apply Pos.ltb_lt.
-Qed.
+Instance Decidable_PosLt : forall p q, Decidable (Pos.lt p q).
+Proof.
+  intros; refine {| Decidable_witness := Pos.ltb p q |}.
+  apply Pos.ltb_lt.
+Defined.
 
-Program Instance Decidable_PosLe : forall p q, Decidable (Pos.le p q) :=
-  { Decidable_witness := Pos.leb p q }.
-Next Obligation.
-apply Pos.leb_le.
-Qed.
+Instance Decidable_PosLe : forall p q, Decidable (Pos.le p q).
+Proof.
+  intros; refine {| Decidable_witness := Pos.leb p q |}.
+  apply Pos.leb_le.
+Defined.
 
 (** * The core reflexive part. *)
 
@@ -167,26 +167,23 @@ match pl with
 end.
 
 (* We could do that with [decide equality] but dependency in proofs is heavy *)
-Program Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q) := {
-  Decidable_witness := beq_poly p q
-}.
-
-Next Obligation.
-split.
-- revert q; induction p; intros [] ?; simpl in *; bool; try_decide;
-    f_equal; first [intuition congruence|auto].
-- revert q; induction p; intros [] Heq; simpl in *; bool; try_decide; intuition;
-    try injection Heq; first[congruence|intuition].
-Qed.
-
-Program Instance Decidable_null : forall p, Decidable (null p) := {
-  Decidable_witness := match p with Cst false => true | _ => false end
-}.
-Next Obligation.
-split.
-- destruct p as [[]|]; first [discriminate|constructor].
-- inversion 1; trivial.
-Qed.
+Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q).
+Proof.
+  intros; refine {| Decidable_witness := beq_poly p q |}.
+  abstract (split; [
+  revert q; induction p; intros [] ?; simpl in *; bool; try_decide;
+    f_equal; first [intuition congruence|auto]
+| revert q; induction p; intros [] Heq; simpl in *; bool; try_decide; intuition;
+    try injection Heq; first[congruence|intuition] ]).
+Defined.
+
+Instance Decidable_null : forall p, Decidable (null p).
+Proof.
+  intros; refine {| Decidable_witness := match p with Cst false => true | _ => false end |}.
+  abstract ( split; [
+  destruct p as [[]|]; first [discriminate|constructor]
+| inversion 1; trivial ] ).
+Defined.
 
 Definition list_nth {A} p (l : list A) def :=
   Pos.peano_rect (fun _ => list A -> A)
@@ -209,14 +206,13 @@ match p with
     valid_dec i p && valid_dec (Pos.succ i) q
 end.
 
-Program Instance Decidable_valid : forall n p, Decidable (valid n p) := {
-  Decidable_witness := valid_dec n p
-}.
-Next Obligation.
-split.
-- revert n; induction p; unfold valid_dec in *; intuition; bool; try_decide; auto.
-- intros H; induction H; unfold valid_dec in *; bool; try_decide; auto.
-Qed.
+Instance Decidable_valid : forall n p, Decidable (valid n p).
+Proof.
+  intros; refine {| Decidable_witness := valid_dec n p |}.
+  abstract (split; [
+  revert n; induction p; unfold valid_dec in *; intuition; bool; try_decide; auto
+| intros H; induction H; unfold valid_dec in *; bool; try_decide; auto ] ).
+Defined.
 
 (** Basic algebra *)
 
diff --git a/theories/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v
index 15cb83fa619b..dc3d2130ab1e 100644
--- a/theories/micromega/ZifyComparison.v
+++ b/theories/micromega/ZifyComparison.v
@@ -35,8 +35,8 @@ Definition ZcompareZ (x y : Z) :=
   Z_of_comparison (Z.compare x y).
 
 #[global]
-Program Instance BinOp_Zcompare : BinOp Z.compare :=
-  { TBOp := ZcompareZ }.
+Instance BinOp_Zcompare : BinOp Z.compare.
+Proof. intros; refine  {| TBOp := ZcompareZ |}. reflexivity.  Defined.
 Add Zify BinOp BinOp_Zcompare.
 
 #[global]