The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

with the kind help from Laurent Théry, I came up with the below solution for 
printing the "Case stack" of the SF Case, SCase, ... tacticals.

This solution has the flaw that it prints all local string variables, but I 
guess such variables are not widely used in the context of a proof, so I 
think this solution is preferable over a solution with modified Case, SCase 
tactics.

Best regards,

Michael

(* Print the name and value of all local string variables.
   When using teh SF Case, SCase, ... tacticals, this prints the current 
"Case stack".
   This is usefull whane using automated tactics which solve many goals.
   "description" is an arbitrary descriptive string *)

Ltac print_cases description:=
  try (
    match goal with
    | Case : String.string |- _ => 
      (let v := eval lazy delta[Case] in Case in idtac description ":" Case 
":=" v );
      revert Case;
      print_cases;
      intro Case
    end
  ).

(* duplicate the current goal *)

Theorem duplicate_goal : forall A, A -> True -> A.
  intros; assumption.
Qed.

(* Same as print_cases, but also works if the tactic solves the current goal 
*)

Ltac print_cases_solve tactic description :=
  apply duplicate_goal; [tactic; fail | print_cases description; trivial].