DECLARE PLUGIN "coinduction_plugin"

{

let coind_version_string = "CoInduction (dev) for Coq 8.10"

open Feedback

let () = Mltop.add_known_plugin (fun () ->
  Flags.if_verbose msg_info Pp.(str coind_version_string))
  "CoInduction"
;;

open Ltac_plugin
open Stdarg
open Extraargs
open Coinduction_main

let classify_proof_start_cmd _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater)

}

VERNAC COMMAND EXTEND Coinduction_cmd CLASSIFIED BY { classify_proof_start_cmd }
| ![ proof ] [ "CoInduction" ident(id) ":" lconstr(t) ] ->
  { fun ~pstate -> Some (do_coinduction id t) }
END

VERNAC COMMAND EXTEND Coinduction_declare_peek_cmd CLASSIFIED AS SIDEFF
| [ "Declare_peek" ident(id) ] -> { do_declare_peek id }
END

TACTIC EXTEND Coinduction_peek_tac
| [ "rewrite_peek" lconstr(t) ] -> { do_rewrite_peek t }
END
