(** See dev/doc/parsing.md for mlg doc *)

DECLARE PLUGIN "rocq-plugin-tutorial.tuto3"

{

open Ltac_plugin

open Construction_game

(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg

}

VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
| [ "Tuto3_1" ] ->
  { let env = Global.env () in
    let sigma = Evd.from_env env in
    let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
    let new_type_2 = EConstr.mkSort s in
    let sigma, _ =
      Typing.type_of env (Evd.from_env env) new_type_2 in
    Feedback.msg_notice
      (Printer.pr_econstr_env env sigma new_type_2) }
END

VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
END

TACTIC EXTEND collapse_hyps
| [ "pack" "hypothesis" ident(i) ] ->
  { Tuto_tactic.pack_tactic i }
END

(* More advanced examples, where automatic proof happens but
   no tactic is being called explicitly.  The first one uses
   type classes. *)
VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> { example_classes n }
END

(* The second one uses canonical structures. *)
VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
| [ "Tuto3_4" int(n) ] -> { example_canonical n }
END