(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

{

open Pp
open Genarg
open Stdarg
open Tacarg
open Extraargs
open Mod_subst
open Names
open CErrors
open Util
open Equality
open Tactypes
open Proofview.Notations
open Attributes
open Vernacextend
open G_redexpr

}

DECLARE PLUGIN "coq-core.plugins.ltac"

TACTIC EXTEND assert_succeeds
| [ "assert_succeeds" tactic3(tac) ]
  -> { Internals.assert_succeeds (Tacinterp.tactic_of_value ist tac) }
END

TACTIC EXTEND replace
| [ "replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
  -> { Internals.replace_in_clause_maybe_by ist None c1 c2 cl tac }
END

TACTIC EXTEND replace_term_left
| [ "replace"  "->" uconstr(c) clause(cl) ]
  -> { Internals.replace_term ist (Some true) c cl }
END

TACTIC EXTEND replace_left
| ["replace" "->" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
  -> { Internals.replace_in_clause_maybe_by ist (Some true) c1 c2 cl tac }
END

TACTIC EXTEND replace_term_right
| [ "replace"  "<-" uconstr(c) clause(cl) ]
  -> { Internals.replace_term ist (Some false) c cl }
END

TACTIC EXTEND replace_right
| [ "replace" "<-" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
  -> { Internals.replace_in_clause_maybe_by ist (Some false) c1 c2 cl tac }
END

TACTIC EXTEND replace_term
| [ "replace" uconstr(c) clause(cl) ]
  -> { Internals.replace_term ist None c cl }
END

TACTIC EXTEND simplify_eq
| [ "simplify_eq" ] -> { dEq ~keep_proofs:None false None }
| [ "simplify_eq" destruction_arg(c) ] -> { Internals.mytclWithHoles (dEq ~keep_proofs:None) false c }
END
TACTIC EXTEND esimplify_eq
| [ "esimplify_eq" ] -> { dEq ~keep_proofs:None true None }
| [ "esimplify_eq" destruction_arg(c) ] -> { Internals.mytclWithHoles (dEq ~keep_proofs:None) true c }
END

TACTIC EXTEND discriminate
| [ "discriminate" ] -> { discr_tac false None }
| [ "discriminate" destruction_arg(c) ] ->
    { Internals.mytclWithHoles discr_tac false c }
END
TACTIC EXTEND ediscriminate
| [ "ediscriminate" ] -> { discr_tac true None }
| [ "ediscriminate" destruction_arg(c) ] ->
    { Internals.mytclWithHoles discr_tac true c }
END

{

let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None

let decode_inj_ipat ?loc = function
  (* For the "as [= pat1 ... patn ]" syntax *)
  | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat
  (* For the "as pat1 ... patn" syntax *)
  | ([] | [_]) as ipat -> ipat
  | pat1::pat2::_ as ipat ->
  (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs
     in the non-singleton list of patterns *)
  match isInjPat pat1 with
  | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.")
  | None ->
  match List.map_filter isInjPat ipat with
  | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.")
  | [] -> ipat

}

TACTIC EXTEND injection
| [ "injection" ] -> { injClause None None false None }
| [ "injection" destruction_arg(c) ] -> { Internals.mytclWithHoles (injClause None None) false c }
END
TACTIC EXTEND einjection
| [ "einjection" ] -> { injClause None None true None }
| [ "einjection" destruction_arg(c) ] -> { Internals.mytclWithHoles (injClause None None) true c }
END
TACTIC EXTEND injection_as
| [ "injection" "as" simple_intropattern_list(ipat)] ->
    { injClause None (Some (decode_inj_ipat ipat)) false None }
| [ "injection" destruction_arg(c) "as" simple_intropattern_list(ipat)] ->
    { Internals.mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c }
END
TACTIC EXTEND einjection_as
| [ "einjection" "as" simple_intropattern_list(ipat)] ->
    { injClause None (Some (decode_inj_ipat ipat)) true None }
| [ "einjection" destruction_arg(c) "as" simple_intropattern_list(ipat)] ->
    { Internals.mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c }
END
TACTIC EXTEND simple_injection
| [ "simple" "injection" ] -> { simpleInjClause None false None }
| [ "simple" "injection" destruction_arg(c) ] -> { Internals.mytclWithHoles (simpleInjClause None) false c }
END

TACTIC EXTEND dependent_rewrite
| [ "dependent" "rewrite" orient(b) constr(c) ] -> { rewriteInConcl b c }
| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
    -> { rewriteInHyp b c id }
END

(**********************************************************************)
(* Decompose                                                          *)

TACTIC EXTEND decompose_sum
| [ "decompose" "sum" constr(c) ] -> { Elim.h_decompose_or c }
END

TACTIC EXTEND decompose_record
| [ "decompose" "record" constr(c) ] -> { Elim.h_decompose_and c }
END

(**********************************************************************)
(* Contradiction                                                      *)

{

open Contradiction

}

TACTIC EXTEND absurd
| [ "absurd" constr(c) ] -> { absurd c }
END

TACTIC EXTEND contradiction
| [ "contradiction" constr_with_bindings_opt(c) ] ->
    { Internals.onSomeWithHoles contradiction c }
END

(**********************************************************************)
(* AutoRewrite                                                        *)

{

open Autorewrite

}

TACTIC EXTEND autorewrite
| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] ->
    { auto_multi_rewrite  l ( cl) }
| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
    {
      auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl
   }
END

TACTIC EXTEND autorewrite_star
| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
    { auto_multi_rewrite ~conds:AllMatches l cl }
| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
  { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl }
END

(**********************************************************************)
(* Rewrite star                                                       *)

{

let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
  let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
  Internals.with_delayed_uconstr ist c
    (fun c -> general_rewrite ~where:clause ~l2r:orient occs ?tac:tac' ~freeze:true ~dep:true ~with_evars:true (c,NoBindings))

}

TACTIC EXTEND rewrite_star
| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
    { rewrite_star ist (Some id) o (occurrences_of occ) c tac }
| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
    { rewrite_star ist (Some id) o (occurrences_of occ) c tac }
| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] ->
    { rewrite_star ist (Some id) o Locus.AllOccurrences c tac }
| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
    { rewrite_star ist None o (occurrences_of occ) c tac }
| [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] ->
    { rewrite_star ist None o Locus.AllOccurrences c tac }
    END

(**********************************************************************)
(* Hint Rewrite                                                       *)

{

let add_rewrite_hint ~locality ~poly bases ort t lcsr =
  let env = Global.env() in
  let sigma = Evd.from_env env in
  let f ce =
    let c, ctx = Constrintern.interp_constr env sigma ce in
    let c = EConstr.to_constr sigma c in
    let ctx =
      let ctx = UState.context_set ctx in
        if poly then ctx
        else (* This is a global universe context that shouldn't be
                refreshed at every use of the hint, declare it globally. *)
          (Global.push_context_set ~strict:true ctx;
           Univ.ContextSet.empty)
    in
      CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
  let eqs = List.map f lcsr in
  let add_hints base = add_rew_rules ~locality base eqs in
  List.iter add_hints bases

let classify_hint _ = VtSideff ([], VtLater)

}

VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint }
| #[ polymorphic; locality = hint_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
  { add_rewrite_hint ~locality ~poly:polymorphic bl o None l }
| #[ polymorphic; locality = hint_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
    ":" preident_list(bl) ] ->
  { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l }
| #[ polymorphic; locality = hint_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
  { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l }
| #[ polymorphic; locality = hint_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
  { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l }
END

(**********************************************************************)
(* Refine                                                             *)

TACTIC EXTEND refine
| [ "refine" uconstr(c) ] ->
   { Internals.refine_tac ist ~simple:false ~with_classes:true c }
END

TACTIC EXTEND simple_refine
| [ "simple" "refine" uconstr(c) ] ->
   { Internals.refine_tac ist ~simple:true ~with_classes:true c }
END

TACTIC EXTEND notcs_refine
| [ "notypeclasses" "refine" uconstr(c) ] ->
   { Internals.refine_tac ist ~simple:false ~with_classes:false c }
END

TACTIC EXTEND notcs_simple_refine
| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
   { Internals.refine_tac ist ~simple:true ~with_classes:false c }
END

(* Solve unification constraints using heuristics or fail if any remain *)
TACTIC EXTEND solve_constraints
| [ "solve_constraints" ] -> { Refine.solve_constraints }
END

(**********************************************************************)
(* Inversion lemmas (Leminv)                                          *)

{

open Inv
open Leminv

let seff id = VtSideff ([id], VtLater)

}

(*VERNAC ARGUMENT EXTEND sort_family
| [ "Set" ] -> { InSet }
| [ "Prop" ] -> { InProp }
| [ "Type" ] -> { InType }
END*)

VERNAC COMMAND EXTEND DeriveInversionClear
| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
  => { seff na }
  -> {
      add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac }

| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
  -> {
      add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac }
END

VERNAC COMMAND EXTEND DeriveInversion
| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
  => { seff na }
  -> {
      add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac }

| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
  -> {
      add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac }
END

VERNAC COMMAND EXTEND DeriveDependentInversion
| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
  => { seff na }
  -> {
      add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac }
END

VERNAC COMMAND EXTEND DeriveDependentInversionClear
| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
  => { seff na }
  -> {
      add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac }
END

(**********************************************************************)
(* Subst                                                              *)

TACTIC EXTEND subst
| [ "subst" ne_hyp_list(l) ] -> { subst l }
| [ "subst" ] -> { subst_all () }
END

{

let simple_subst_tactic_flags =
  { only_leibniz = true; rewrite_dependent_proof = false }

}

TACTIC EXTEND simple_subst
| [ "simple" "subst" ] -> { subst_all ~flags:simple_subst_tactic_flags () }
END

{

open Evar_tactics

}

(**********************************************************************)
(* Evar creation                                                      *)

(* TODO: add support for some test similar to g_constr.name_colon so that
   expressions like "evar (list A)" do not raise a syntax error *)
TACTIC EXTEND evar
| [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> { let_evar (Name.Name id) typ }
| [ "evar" constr(typ) ] -> { let_evar Name.Anonymous typ }
END

TACTIC EXTEND instantiate
| [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] ->
    { instantiate_tac_by_name id c }
| [ "instantiate" "(" natural(i) ":=" lglob(c) ")" hloc(hl) ] ->
    { instantiate_tac i c hl }
END

(**********************************************************************)
(** Nijmegen "step" tactic for setoid rewriting                       *)

{

open Tactics
open Libobject

(* Registered lemmas are expected to be of the form
     x R y -> y == z -> x R z    (in the right table)
     x R y -> x == z -> z R y    (in the left table)
*)

let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r"
let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l"

(* [step] tries to apply a rewriting lemma; then apply [tac] intended to
   complete to proof of the last hypothesis (assumed to state an equality) *)

let step left x tac =
  let l =
    List.map (fun lem ->
      let lem = EConstr.of_constr lem in
      Tacticals.tclTHENLAST
        (apply_with_bindings (lem, ImplicitBindings [x]))
        tac)
      !(if left then transitivity_left_table else transitivity_right_table)
  in
  Tacticals.tclFIRST l

(* Main function to push lemmas in persistent environment *)

let cache_transitivity_lemma (left,lem) =
  if left then
    transitivity_left_table  := lem :: !transitivity_left_table
  else
    transitivity_right_table := lem :: !transitivity_right_table

let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)

let inTransitivity : bool * Constr.t -> obj =
  declare_object @@ global_object_nodischarge "TRANSITIVITY-STEPS"
    ~cache:cache_transitivity_lemma
    ~subst:(Some subst_transitivity_lemma)

(* Main entry points *)

let add_transitivity_lemma left lem =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in
  let lem' = EConstr.to_constr sigma lem' in
  Lib.add_leaf (inTransitivity (left,lem'))

}

(* Vernacular syntax *)

TACTIC EXTEND stepl
| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) }
| ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) }
END

TACTIC EXTEND stepr
| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) }
| ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) }
END

VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF
| [ "Declare" "Left" "Step" constr(t) ] ->
    { add_transitivity_lemma true t }
END

VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
| [ "Declare" "Right" "Step" constr(t) ] ->
    { add_transitivity_lemma false t }
END

(**********************************************************************)
(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
  defined by Conor McBride *)
TACTIC EXTEND generalize_eqs
| ["generalize_eqs" hyp(id) ] -> { Generalize.abstract_generalize ~generalize_vars:false id }
END
TACTIC EXTEND dep_generalize_eqs
| ["dependent" "generalize_eqs" hyp(id) ] -> { Generalize.abstract_generalize ~generalize_vars:false ~force_dep:true id }
END
TACTIC EXTEND generalize_eqs_vars
| ["generalize_eqs_vars" hyp(id) ] -> { Generalize.abstract_generalize ~generalize_vars:true id }
END
TACTIC EXTEND dep_generalize_eqs_vars
| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { Generalize.abstract_generalize ~force_dep:true ~generalize_vars:true id }
END

(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T]
    where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated
    during dependent induction. For internal use. *)

TACTIC EXTEND specialize_eqs
| [ "specialize_eqs" hyp(id) ] -> { specialize_eqs id }
END

TACTIC EXTEND destauto DEPRECATED { Deprecation.make ~since:"8.20" () }
| [ "destauto" ] -> { Internals.destauto }
| [ "destauto" "in" hyp(id) ] -> { Internals.destauto_in id }
END

(**********************************************************************)

(**********************************************************************)
(* A version of abstract constructing transparent terms               *)
(* Introduced by Jason Gross and Benjamin Delaware in June 2016       *)
(**********************************************************************)

TACTIC EXTEND transparent_abstract
| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
    Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; }
| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
    Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; }
END

(* ********************************************************************* *)

TACTIC EXTEND constr_eq
| [ "constr_eq" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:false x y }
END

TACTIC EXTEND constr_eq_strict
| [ "constr_eq_strict" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:true x y }
END

TACTIC EXTEND constr_eq_nounivs
| [ "constr_eq_nounivs" constr(x) constr(y) ] -> {
    Proofview.tclEVARMAP >>= fun sigma ->
    if EConstr.eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.tclFAIL (str "Not equal") }
END

TACTIC EXTEND is_evar
| [ "is_evar" constr(x) ] -> { Internals.is_evar x }
END

TACTIC EXTEND has_evar
| [ "has_evar" constr(x) ] -> { Internals.has_evar x }
END

TACTIC EXTEND is_hyp
| [ "is_var" constr(x) ] -> { Internals.is_var x }
END

TACTIC EXTEND is_fix
| [ "is_fix" constr(x) ] -> { Internals.is_fix x }
END

TACTIC EXTEND is_cofix
| [ "is_cofix" constr(x) ] -> { Internals.is_cofix x }
END

TACTIC EXTEND is_ind
| [ "is_ind" constr(x) ] -> { Internals.is_ind x }
END

TACTIC EXTEND is_constructor
| [ "is_constructor" constr(x) ] -> { Internals.is_constructor x }
END

TACTIC EXTEND is_proj
| [ "is_proj" constr(x) ] -> { Internals.is_proj x }
END

TACTIC EXTEND is_const
| [ "is_const" constr(x) ] -> { Internals.is_const x }
END

(* Shelves all the goals under focus. *)
TACTIC EXTEND shelve
| [ "shelve" ] -> { Proofview.shelve }
END

(* Shelves the unifiable goals under focus, i.e. the goals which
   appear in other goals under focus (the unfocused goals are not
   considered). *)
TACTIC EXTEND shelve_unifiable
| [ "shelve_unifiable" ] -> { Proofview.shelve_unifiable }
END

(* Unshelves the goal shelved by the tactic. *)
TACTIC EXTEND unshelve
| [ "unshelve" tactic1(t) ] -> { Internals.unshelve ist t }
END

(* Command to add every unshelved variables to the focus *)
VERNAC COMMAND EXTEND Unshelve STATE proof
| [ "Unshelve" ]
  => { classify_as_proofstep }
  -> { fun ~pstate -> Declare.Proof.map ~f:(fun p  -> Proof.unshelve p) pstate  }
END

(* Gives up on the goals under focus: the goals are considered solved,
   but the proof cannot be closed until the user goes back and solve
   these goals. *)
TACTIC EXTEND give_up
| [ "give_up" ] ->
    { Proofview.give_up }
END

(* cycles [n] goals *)
TACTIC EXTEND cycle
| [ "cycle" int_or_var(n) ] -> { Proofview.cycle n }
END

(* swaps goals number [i] and [j] *)
TACTIC EXTEND swap
| [ "swap" int_or_var(i) int_or_var(j) ] -> { Proofview.swap i j }
END

(* reverses the list of focused goals *)
TACTIC EXTEND revgoals
| [ "revgoals" ] -> { Proofview.revgoals }
END

{

type cmp =
  | Eq
  | Lt | Le
  | Gt | Ge

type 'i test =
  | Test of cmp * 'i * 'i

let pr_cmp = function
  | Eq -> Pp.str"="
  | Lt -> Pp.str"<"
  | Le -> Pp.str"<="
  | Gt -> Pp.str">"
  | Ge -> Pp.str">="

let pr_cmp' _prc _prlc _prt = pr_cmp

let pr_test_gen f (Test(c,x,y)) =
  Pp.(f x ++ pr_cmp c ++ f y)

let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int)

let pr_test' _prc _prlc _prt = pr_test

let pr_itest = pr_test_gen Pp.int

let pr_itest' _prc _prlc _prt = pr_itest

}

ARGUMENT EXTEND comparison PRINTED BY { pr_cmp' }
| [ "="  ] -> { Eq }
| [ "<"  ] -> { Lt }
| [ "<=" ] -> { Le }
| [ ">"  ] -> { Gt }
| [ ">=" ] -> { Ge }
    END

{

let interp_test ist env sigma = function
  | Test (c,x,y) ->
      Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y)

}

ARGUMENT EXTEND test
  PRINTED BY { pr_itest' }
  INTERPRETED BY { interp_test }
  RAW_PRINTED BY { pr_test' }
  GLOB_PRINTED BY { pr_test' }
| [ int_or_var(x) comparison(c) int_or_var(y) ] -> { Test(c,x,y) }
END

{

let interp_cmp = function
  | Eq -> Int.equal
  | Lt -> ((<):int->int->bool)
  | Le -> ((<=):int->int->bool)
  | Gt -> ((>):int->int->bool)
  | Ge -> ((>=):int->int->bool)

let run_test = function
  | Test(c,x,y) -> interp_cmp c x y

let guard tst =
  if run_test tst then
    Proofview.tclUNIT ()
  else
    let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in
    Tacticals.tclZEROMSG msg

}

TACTIC EXTEND guard
| [ "guard" test(tst) ] -> { guard tst }
END

TACTIC EXTEND decompose
| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> { Internals.decompose l c }
END

(** library/keys *)

VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> { Internals.declare_equivalent_keys c c' }
END

VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) }
END

VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
  { fun ~pstate -> Declare.Proof.compact pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
  { Gc.compact () }
END

TACTIC EXTEND optimize_heap
| [ "optimize_heap" ] -> { Internals.tclOPTIMIZE_HEAP }
END

VERNAC COMMAND EXTEND infoH CLASSIFIED AS QUERY
| ![ proof_query ] [ "infoH" tactic(tac) ] -> { Internals.infoH tac }
END

(** Tactic analogous to [Strategy] vernacular *)

TACTIC EXTEND with_strategy
| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> {
  with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac)
}
END