Merge PR #9501: Sphinx: fail when a command fails + other stuff

Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego

2 files changed, 15 insertions, 24 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index cc788b3595..b474c51f17 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -627,14 +627,10 @@ logical equivalence:
    Instance all_iff_morphism (A : Type) :
             Proper (pointwise_relation A iff ==> iff) (@all A).
 
-.. coqtop:: all
+.. coqtop:: all abort
 
    Proof. simpl_relation.
 
-.. coqtop:: none
-
-   Abort.
-
 One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
 declared such a morphism, it will be used by the setoid rewriting
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 43d302114e..c7ea7e326f 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is:
       eqb_leibniz x y H :=
             match x, y return x = y with tt, tt => eq_refl tt end }.
 
-If one does not give all the members in the Instance declaration, Coq
-enters the proof-mode and the user is asked to build inhabitants of
-the remaining fields, e.g.:
+Using :cmd:`Program Instance`, if one does not give all the members in
+the Instance declaration, Coq generates obligations for the remaining
+fields, e.g.:
 
 .. coqtop:: in
 
-   Instance eq_bool : EqDec bool :=
+   Require Import Program.Tactics.
+   Program Instance eq_bool : EqDec bool :=
    { eqb x y := if x then y else negb y }.
 
 .. coqtop:: all
 
-   Proof. intros x y H.
-
-.. coqtop:: all
-
-   destruct x ; destruct y ; (discriminate || reflexivity).
-
-.. coqtop:: all
-
+   Next Obligation.
+     destruct x ; destruct y ; (discriminate || reflexivity).
    Defined.
 
 One has to take care that the transparency of every field is
@@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.:
 
 .. coqtop:: in
 
-   Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
+   Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
    { eqb x y := match x, y with
                 | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
                 end }.
 
 .. coqtop:: none
 
-   Abort.
+   Admit Obligations.
 
 These instances are used just as well as lemmas in the instance hint
 database.
@@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example:
 
      Context `{EA : EqDec A}.
 
-     Global Instance option_eqb : EqDec (option A) :=
+     Global Program Instance option_eqb : EqDec (option A) :=
      { eqb x y := match x, y with
             | Some x, Some y => eqb x y
             | None, None => true
             | _, _ => false
             end }.
-     Admitted.
+   Admit Obligations.
 
    End EqDec_defs.
 
@@ -564,12 +559,12 @@ Settings
    This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
-   + When it is on (the default), instances that have unsolved holes in
+   + When it is off (the default), they fail with an error instead.
+
+   + When it is on, instances that have unsolved holes in
      their proof-term silently open the proof mode with the remaining
      obligations to prove.
 
-   + When it is off, they fail with an error instead.
-
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~