Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]

Utility: Classical Itauto Tactic

This module contains a version of the itauto tactic that uses classical logic freely. See the comments in VLSM.Lib.Itauto for more details. 
Ltac gen_conflicts tac :=
  intros; unfold not in *; unfold iff in *;
  cdcl_nnpp; unfold not;
  (cdcl_conflicts tac).

Tactic Notation "itauto" tactic(tac) :=
  gen_conflicts tac ;
  vitautog.

Tactic Notation "itauto" :=
  itauto auto.

Ltac itautor tac := let t := solve[tac | itauto tac] in itauto t.

(* required for documentation generation *)
Definition iYC2 := True.