Merge branch 'v8.5' into trunk

12 files changed, 141 insertions, 85 deletions

diff --git a/CHANGES b/CHANGES
index 5b3043fdfe..19683f8e39 100644
--- a/CHANGES
+++ b/CHANGES
@@ -112,8 +112,8 @@ Tactics
     (i.e. it selects the first success of a).
   * Tactic "constructor" is now fully backtracking, thus deprecating
     the need of the undocumented "constructor <tac>" syntax which is
-    now equivalent to "once (constructor; tac)". (potential source of
-    rare incompatibilities).
+    now equivalent to "[> once (constructor; tac) ..]". (potential
+    source of rare incompatibilities).
   * New "multimatch" variant of "match" tactic which backtracks to
     new branches in case of a later failure. The "match" tactic is
     equivalent to "once multimatch".
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 107b98f010..37cbd1eac1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -427,9 +427,11 @@ To know to which notations a given symbol belongs to, use the command
 \begin{quote}
 \tt Locate {\symbolentry}
 \end{quote}
-where symbol is any (composite) symbol surrounded by quotes. To locate
+where symbol is any (composite) symbol surrounded by double quotes. To locate
 a particular notation, use a string where the variables of the
-notation are replaced by ``\_''.
+notation are replaced by ``\_'' and where possible single quotes
+inserted around identifiers or tokens starting with a single quote are
+dropped.
 
 \Example
 \begin{coq_example}
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 3fded66385..52dc49bf8e 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -13,6 +13,7 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
+#include <stdint.h>
 #include <caml/config.h>
 #include <caml/misc.h>
 #include <caml/mlvalues.h>
@@ -146,7 +147,7 @@ value coq_tcode_of_code (value code, value size) {
     };
     *q++ = VALINSTR(instr);
     if (instr == SWITCH) {
-      uint32 i, sizes, const_size, block_size;
+      uint32_t i, sizes, const_size, block_size;
       COPY32(q,p); p++;
       sizes=*q++;
       const_size = sizes & 0xFFFF;
@@ -154,13 +155,13 @@ value coq_tcode_of_code (value code, value size) {
       sizes = const_size + block_size;
       for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
     } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
-      uint32 i, n;
+      uint32_t i, n;
       COPY32(q,p); p++; /* ndefs */
       n = 3 + 2*(*q);  /* ndefs, nvars, start, typlbls,lbls*/
       q++;
       for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
     } else {
-      uint32 i, ar;
+      uint32_t i, ar;
       ar = arity[instr]; 
       for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
     }
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index f9e0dc7f11..d74affdea9 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -15,6 +15,7 @@
 
 #include <stdio.h>
 #include <signal.h>
+#include <stdint.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -30,9 +31,9 @@
 #endif
 
 /* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) (((uint32)val >> 1))
-#define value_of_uint32(i)   ((value)(((uint32)(i) << 1) | 1))
-#define UI64_of_uint32(lo)  ((uint64)(I64_literal(0,(uint32)(lo))))
+#define uint32_of_value(val) (((uint32_t)val >> 1))
+#define value_of_uint32(i)   ((value)(((uint32_t)(i) << 1) | 1))
+#define UI64_of_uint32(lo)  ((uint64_t)(I64_literal(0,(uint32_t)(lo))))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
@@ -788,7 +789,7 @@ value coq_interprete
 /* Access to components of blocks */
         
       Instruct(SWITCH) {
-	uint32 sizes = *pc++;
+	uint32_t sizes = *pc++;
 	print_instr("SWITCH");
 	print_int(sizes & 0xFFFF);
 	if (Is_block(accu)) {
@@ -1054,7 +1055,7 @@ value coq_interprete
            the one ontop of the stack (which is poped)*/
         print_instr("ADDINT31");
         accu = 
-           (value)((uint32) accu + (uint32) *sp++ - 1); 
+           (value)((uint32_t) accu + (uint32_t) *sp++ - 1); 
         /* nota,unlike CaML we don't want
            to have a different behavior depending on the 
            architecture. Thus we cast the operand to uint32 */
@@ -1064,9 +1065,9 @@ value coq_interprete
       Instruct (ADDCINT31) {
 	print_instr("ADDCINT31");
 	/* returns the sum with a carry */
-	uint32 s;
-	s = (uint32)accu + (uint32)*sp++ - 1;
-        if( (uint32)s < (uint32)accu ) {
+	uint32_t s;
+	s = (uint32_t)accu + (uint32_t)*sp++ - 1;
+        if( (uint32_t)s < (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1081,10 +1082,10 @@ value coq_interprete
       Instruct (ADDCARRYCINT31) {
 	print_instr("ADDCARRYCINT31");
 	/* returns the sum plus one with a carry */
-	uint32 s;
-	s = (uint32)accu + (uint32)*sp++ + 1;
+	uint32_t s;
+	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
 	value block;
-        if( (uint32)s <= (uint32)accu ) {
+        if( (uint32_t)s <= (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1100,18 +1101,18 @@ value coq_interprete
 	print_instr("SUBINT31");
 	/* returns the subtraction */
 	accu = 
-	  (value)((uint32) accu - (uint32) *sp++ + 1); 
+	  (value)((uint32_t) accu - (uint32_t) *sp++ + 1); 
         Next;
       }
 
       Instruct (SUBCINT31) {
 	print_instr("SUBCINT31");
 	/* returns the subtraction with a carry */
-	uint32 b;
-	uint32 s;
-	b = (uint32)*sp++;
-	s = (uint32)accu - b + 1;
-        if( (uint32)accu < b ) {
+	uint32_t b;
+	uint32_t s;
+	b = (uint32_t)*sp++;
+	s = (uint32_t)accu - b + 1;
+        if( (uint32_t)accu < b ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1126,11 +1127,11 @@ value coq_interprete
       Instruct (SUBCARRYCINT31) {
 	print_instr("SUBCARRYCINT31");
 	/* returns the subtraction minus one with a carry */
-	uint32 b;
-	uint32 s;
-	b = (uint32)*sp++;
-	s = (value)((uint32)accu - b - 1);
-        if( (uint32)accu <= b ) {
+	uint32_t b;
+	uint32_t s;
+	b = (uint32_t)*sp++;
+	s = (value)((uint32_t)accu - b - 1);
+        if( (uint32_t)accu <= b ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1154,7 +1155,7 @@ value coq_interprete
         /*returns the multiplication on a double size word
           (special case for 0) */
         print_instr("MULCINT31");
-	uint64 p;
+	uint64_t p;
         /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
         p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
 	if ( I64_is_zero(p) ) {
@@ -1177,10 +1178,10 @@ value coq_interprete
 	/* spiwack: takes three int31 (the two first ones represent an
                     int62) and performs the euclidian division of the
                     int62 by the int31 */
-        uint64 bigint;
+        uint64_t bigint;
         bigint = UI64_of_value(accu);
         bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
-        uint64 divisor;
+        uint64_t divisor;
         divisor = UI64_of_value(*sp++);
         Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
         if (I64_is_zero (divisor)) {
@@ -1188,7 +1189,7 @@ value coq_interprete
           Field(accu, 1) = 1; /* 2*0+1 */
 	}
 	else {
-	  uint64 quo, mod;
+	  uint64_t quo, mod;
           I64_udivmod(bigint, divisor, &quo, &mod);
           Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
 	  Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
@@ -1201,7 +1202,7 @@ value coq_interprete
         /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
                     since it probably only concerns negative number.
                     needs to be checked at this point */
-        uint32 divisor;
+        uint32_t divisor;
         divisor = uint32_of_value(*sp++);
         if (divisor == 0) { 
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
@@ -1209,7 +1210,7 @@ value coq_interprete
           Field(accu, 1) = 1; /* 2*0+1 */
         }
         else {
-          uint32 modulus;
+          uint32_t modulus;
           modulus = uint32_of_value(accu);
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
 	  Field(accu, 0) = value_of_uint32(modulus/divisor);
@@ -1221,7 +1222,7 @@ value coq_interprete
       Instruct (ADDMULDIVINT31) {
         print_instr("ADDMULDIVINT31");
         /* higher level shift (does shifts and cycles and such) */
-        uint32 shiftby;
+        uint32_t shiftby;
         shiftby = uint32_of_value(accu);
         if (shiftby > 31) {
           if (shiftby < 62) {
@@ -1236,7 +1237,7 @@ value coq_interprete
         /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
         accu = (value)(((*sp++)^1) << shiftby);
         /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
-        accu = (value)((accu | (((uint32)(*sp++)) >> (31-shiftby)))|1);
+        accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
 	}
         Next;
       }
@@ -1245,11 +1246,11 @@ value coq_interprete
 	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
 	/* assumes Inudctive _ : _ := Eq | Lt | Gt */
 	print_instr("COMPAREINT31");
-	if ((uint32)accu == (uint32)*sp) {
+	if ((uint32_t)accu == (uint32_t)*sp) {
 	  accu = 1;  /* 2*0+1 */
 	  sp++;
 	}
-	else{if ((uint32)accu < (uint32)(*sp++)) {
+	else{if ((uint32_t)accu < (uint32_t)(*sp++)) {
 	  accu = 3;  /* 2*1+1 */
 	}
 	else{
@@ -1260,9 +1261,9 @@ value coq_interprete
  
       Instruct (HEAD0INT31) {
 	int r = 0;
-        uint32 x;
+        uint32_t x;
         print_instr("HEAD0INT31");
-	x = (uint32) accu;
+	x = (uint32_t) accu;
         if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; }
         if (!(x & 0xFF000000)) { x <<= 8;  r += 8; }
         if (!(x & 0xF0000000)) { x <<= 4;  r += 4; }
@@ -1275,9 +1276,9 @@ value coq_interprete
         
       Instruct (TAIL0INT31) {
 	int r = 0;
-        uint32 x;
+        uint32_t x;
         print_instr("TAIL0INT31");
-	x = (((uint32) accu >> 1) | 0x80000000);
+	x = (((uint32_t) accu >> 1) | 0x80000000);
         if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
         if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
         if (!(x & 0x000F)) { x >>= 4;  r += 4; }
@@ -1327,7 +1328,7 @@ value coq_interprete
         /*accu=accu or accu = (value)((unsigned long)1-accu) if bool
 	               is used for the bits */
         for(i=0; i < 30; i++) {
-	  accu = (value) ((((uint32)accu-1) << 1) | *sp++);
+	  accu = (value) ((((uint32_t)accu-1) << 1) | *sp++);
           /* -1 removes the tag bit, << 1 multiplies the value by 2, 
               | *sp++ pops the last value and add it (no carry involved)
 	      not that it reintroduces a tag bit */
@@ -1347,7 +1348,7 @@ value coq_interprete
         for(i = 30; i >= 0; i--) {
           Field(block, i) = (value)(accu & 3); /* two last bits of the accumulator */
           //Field(block, i) = 3;
-          accu = (value) ((uint32)accu >> 1) | 1;  /* last bit must be a one */
+          accu = (value) ((uint32_t)accu >> 1) | 1;  /* last bit must be a one */
         };
 	accu = block;
         Next;
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
index 8a6a266457..657d0a07e0 100644
--- a/kernel/byterun/int64_native.h
+++ b/kernel/byterun/int64_native.h
@@ -18,9 +18,9 @@
 #ifndef CAML_INT64_NATIVE_H
 #define CAML_INT64_NATIVE_H
 
-#define I64_literal(hi,lo) ((int64)(hi) << 32 | (lo))
+#define I64_literal(hi,lo) ((int64_t)(hi) << 32 | (lo))
 #define I64_compare(x,y) (((x) > (y)) - ((x) < (y)))
-#define I64_ult(x,y) ((uint64)(x) < (uint64)(y))
+#define I64_ult(x,y) ((uint64_t)(x) < (uint64_t)(y))
 #define I64_neg(x) (-(x))
 #define I64_add(x,y) ((x) + (y))
 #define I64_sub(x,y) ((x) - (y))
@@ -30,19 +30,19 @@
 #define I64_div(x,y) ((x) / (y))
 #define I64_mod(x,y) ((x) % (y))
 #define I64_udivmod(x,y,quo,rem) \
-  (*(rem) = (uint64)(x) % (uint64)(y), \
-   *(quo) = (uint64)(x) / (uint64)(y))
+  (*(rem) = (uint64_t)(x) % (uint64_t)(y), \
+   *(quo) = (uint64_t)(x) / (uint64_t)(y))
 #define I64_and(x,y) ((x) & (y))
 #define I64_or(x,y) ((x) | (y))
 #define I64_xor(x,y) ((x) ^ (y))
 #define I64_lsl(x,y) ((x) << (y))
 #define I64_asr(x,y) ((x) >> (y))
-#define I64_lsr(x,y) ((uint64)(x) >> (y))
+#define I64_lsr(x,y) ((uint64_t)(x) >> (y))
 #define I64_to_intnat(x) ((intnat) (x))
 #define I64_of_intnat(x) ((intnat) (x))
-#define I64_to_int32(x) ((int32) (x))
-#define I64_of_int32(x) ((int64) (x))
+#define I64_to_int32(x) ((int32_t) (x))
+#define I64_of_int32(x) ((int64_t) (x))
 #define I64_to_double(x) ((double)(x))
-#define I64_of_double(x) ((int64)(x))
+#define I64_of_double(x) ((int64_t)(x))
 
 #endif /* CAML_INT64_NATIVE_H */
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc1372..07df7c7f09 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -89,25 +89,22 @@ let get_info sigma gl=
 let try_get_info sigma gl =
   Store.get (Goal.V82.extra sigma gl) info
 
-let get_stack pts =
+let get_goal_stack pts =
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
 
 
 let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
 
 let focus p =
-  let inf = get_stack p in
+  let inf = get_goal_stack p in
   Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
 
 let unfocus () =
   Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
 
-let maximal_unfocus () = 
-  Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
-
 let get_top_stack pts =
   try
     Proof.get_at_focus proof_focus pts
@@ -116,6 +113,8 @@ let get_top_stack pts =
     let info = get_info sigma gl in
     info.pm_stack
 
+let get_stack pts = Proof.get_at_focus proof_focus pts
+
 let get_last env = match Environ.named_context env with
   | (id,_,_)::_ -> id
   | [] -> error "no previous statement to use"
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 2864ba18ee..e12c4c9237 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -75,5 +75,3 @@ val get_last:  Environ.env -> Id.t
 val focus : Proof.proof -> unit
 
 val unfocus : unit -> unit
-
-val maximal_unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c61079e636..ab5282e791 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -131,12 +131,13 @@ let daimon_tac gls =
 
 (* post-instruction focus management *)
 
-(* spiwack: This used to fail if there was no focusing command
-   above, but I don't think it ever happened. I hope it doesn't mess
-   things up*)
 let goto_current_focus () = 
-  Decl_mode.maximal_unfocus ()
+  Decl_mode.unfocus ()
 
+(* spiwack: used to catch errors indicating lack of "focusing command"
+   in the proof tree. In the current implementation, however, entering
+   the declarative mode puts a focus first, there should, therefore,
+   never be exception raised here. *)
 let goto_current_focus_or_top () =
   goto_current_focus ()
 
@@ -1444,12 +1445,19 @@ let rec postprocess pts instr =
 				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
 		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
-    | Pend _ ->
-	goto_current_focus_or_top ()
+    | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
+    | Pend _ -> ()
 
 let do_instr raw_instr pts =
   let has_tactic = preprocess pts raw_instr.instr in
-  begin
+  (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
+     current proof (and, actually so does [do_instr] later one, so
+     it's ok to do the same here. Ideally the proof should be properly
+     threaded through the commands here, but since the are interleaved
+     with actions on the proof mode, which is attached to the global
+     proof environment, it is not possible without heavy lifting. *)
+  let pts = Proof_global.give_me_the_proof () in
+  let pts =
     if has_tactic then
             let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma; } in
@@ -1458,13 +1466,13 @@ let do_instr raw_instr pts =
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) env sigma glob_instr in
-      ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)))
-    else () end;
-  postprocess pts raw_instr.instr;
-  (* spiwack: this should restore a compatible semantics with
-     v8.3 where we never stayed focused on 0 goal. *)
-  Proof_global.set_proof_mode "Declarative" ;
-  Decl_mode.maximal_unfocus ()
+      let (pts',_) = Proof.run_tactic (Global.env())
+        (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
+      pts'
+    else pts
+  in
+  Proof_global.simple_with_current_proof (fun _ _ -> pts);
+  postprocess pts raw_instr.instr
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index ef9d3159d2..2bd88d5aea 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -57,23 +57,18 @@ let vernac_decl_proof () =
   else
     begin
       Decl_proof_instr.go_to_proof_mode () ;
-      Proof_global.set_proof_mode "Declarative" ;
-      Vernacentries.print_subgoals ()
+      Proof_global.set_proof_mode "Declarative"
     end
 
 (* spiwack: some bureaucracy is not performed here *)
 let vernac_return () =
   begin
     Decl_proof_instr.return_from_tactic_mode () ;
-    Proof_global.set_proof_mode "Declarative" ;
-    Vernacentries.print_subgoals ()
+    Proof_global.set_proof_mode "Declarative"
   end
 
 let vernac_proof_instr instr =
-  begin
-    Decl_proof_instr.proof_instr instr;
-    Vernacentries.print_subgoals ()
-  end
+  Decl_proof_instr.proof_instr instr
 
 (* Before we can write an new toplevel command (see below) 
     which takes a [proof_instr] as argument, we need to declare
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 18159288de..a8372195d4 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -81,6 +81,7 @@ let init_channels () =
 
 let get_channels () =
   match !channels with
-  | None -> Errors.anomaly(Pp.str "init_channels not called")
+  | None ->
+    Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
+    exit 1
   | Some(ic, oc) -> ic, oc
-
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index d00a707bd5..ae3e50d7ee 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -122,6 +122,7 @@ Section GraphObj.
 
   Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
     GraphIndex_Morphism s d'.
+  Proof using.  (* This makes no sense, but it makes this test behave as before the no admit commit *)
   Admitted.
 
    Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
diff --git a/test-suite/success/tryif.v b/test-suite/success/tryif.v
new file mode 100644
index 0000000000..4394bddb3d
--- /dev/null
+++ b/test-suite/success/tryif.v
@@ -0,0 +1,50 @@
+Require Import TestSuite.admit.
+
+(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
+Tactic Notation "not" tactic3(tac) :=
+  (tryif tac then fail 0 tac "succeeds" else idtac); (* error if the tactic solved all goals *) [].
+
+(** Test if a tactic succeeds, but always roll-back the results *)
+Tactic Notation "test" tactic3(tac) := tryif not tac then fail 0 tac "fails" else idtac.
+
+Goal Set.
+Proof.
+  not fail.
+  not not idtac.
+  not fail 0.
+  (** Would be nice if we could get [not fail 1] to pass, maybe *)
+  not not admit.
+  not not test admit.
+  not progress test admit.
+  (* test grouping *)
+  not (not idtac; fail).
+  assert True.
+  all:not fail.
+  2:not fail.
+  all:admit.
+Defined.
+
+Goal Set.
+Proof.
+  test idtac.
+  test try fail.
+  test admit.
+  test match goal with |- Set => idtac end.
+  test (idtac; match goal with |- Set => idtac end).
+  (* test grouping *)
+  first [ (test idtac; fail); fail 1 | idtac ].
+  try test fail.
+  try test test fail.
+  test test idtac.
+  test test admit.
+  Fail test fail.
+  test (idtac; []).
+  test (assert True; [|]).
+  (* would be nice, perhaps, if we could catch [fail 1] and not just [fail 0] this *)
+  try ((test fail); fail 1).
+  assert True.
+  all:test idtac.
+  all:test admit.
+  2:test admit.
+  all:admit.
+Defined.