Quelle  auto_order.out   Sprache: unbekannt

Non-discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: none
Unfoldable projection definitions: none
Cut: emp
For any goal ->   (*external*) (idtac "second"; fail) (cost 1, id 0)
                  (*external*) (idtac "first"; fail) (cost 1, id 0)
                  (*external*) (idtac "fourth"; fail) (cost 2, id 0)
                  (*external*) (idtac "third"; fail) (cost 2, id 0)

(* info auto: *)
second
first
fourth
third
fifth, different hintDb
idtac.
(* info eauto: *)
second
first
fifth, different hintDb
fourth
third
idtac.
second
first
fifth, different hintDb
fourth
third
File "./output/auto_order.v", line 16, characters 5-45:
The command has indeed failed with message:
Tactic failure: Proof search failed.