test-suite/stm/classify_set_proof_mode_9093.v


1
2
3
4
5
6
7
8
9

(* -*- coq-prog-args: ("-async-proofs" "on" "-noinit"); -*- *)

Declare ML Module "ltac_plugin".

Set Default Proof Mode "Classic".

Goal Prop.
  idtac.
Abort.