Quelle  g_tactic.mlg   Sprache: unbekannt

(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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)         *)
(************************************************************************)

DECLARE PLUGIN "rocq-runtime.plugins.ltac"

{

open Pp
open CErrors
open Util
open Names
open Namegen
open Tacexpr
open Genredexpr
open Constrexpr
open Libnames
open Tok
open Tactypes
open Tactics
open Inv
open Locus
open G_redexpr

open Procq


let all_with ~head delta =
  let all = [FBeta;FMatch;FFix;FCofix;FZeta;delta] in
  Redops.make_red_flag (if head then FHead :: all else all)

let err () = raise Gramlib.Stream.Failure

(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
let test_lpar_id_coloneq =
  let open Procq.Lookahead in
  to_entry "lpar_id_coloneq" begin
    lk_kw "(" >> lk_ident >> lk_kw ":="
  end

(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
  let open Procq.Lookahead in
  to_entry "lpar_id_coloneq" begin
    lk_kw "(" >> lk_ident >> lk_kw ")"
  end

(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
  let open Procq.Lookahead in
  to_entry "test_lpar_idnum_coloneq" begin
    lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":="
  end

let test_leftsquarebracket_equal =
  let open Procq.Lookahead in
  to_entry "test_leftsquarebracket_equal" begin
    lk_kw "[" >> lk_kw "=" >> check_no_space
  end

(* idem for (x:t) *)
open Extraargs

(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
  Procq.Entry.(of_parser "lpar_id_colon"
    { parser_fun = fun kwstate strm ->
      let rec skip_to_rpar p n =
        match List.last (Gramlib.LStream.npeek kwstate n strm) with
        | KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
        | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
        | KEYWORD "." -> err ()
        | _ -> skip_to_rpar p (n+1) in
      let rec skip_names n =
        match List.last (Gramlib.LStream.npeek kwstate n strm) with
        | IDENT _ | KEYWORD "_" -> skip_names (n+1)
        | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
        | _ -> err () in
      let rec skip_binders n =
        match List.last (Gramlib.LStream.npeek kwstate n strm) with
        | KEYWORD "(" -> skip_binders (skip_names (n+1))
        | IDENT _ | KEYWORD "_" -> skip_binders (n+1)
        | KEYWORD ":=" -> ()
        | _ -> err () in
      match Gramlib.LStream.peek_nth kwstate 0 strm with
      | KEYWORD "(" -> skip_binders 2
      | _ -> err () })

let lookup_at_as_comma =
  let open Procq.Lookahead in
  to_entry "lookup_at_as_comma" begin
    lk_kws [",";"at";"as"]
  end

open Constr
open Prim
open Pltac

let mk_fix_tac (loc,id,bl,ann,ty) =
  let n =
    match bl,ann with
        [([_],_,_)], None -> 1
      | _, Some x ->
          let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
          (try List.index Names.Name.equal x.CAst.v ids
          with Not_found -> user_err ~loc Pp.(str "No such fix variable."))
      | _ -> user_err ~loc Pp.(str "Cannot guess decreasing argument of fix.") in
  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,None,bk,t)) bl in
  (id,n, CAst.make ~loc @@ CProdN(bl,ty))

let mk_cofix_tac (loc,id,bl,ann,ty) =
  let () = Option.iter (fun { CAst.loc = aloc } ->
      user_err ?loc:aloc
        (Pp.str"Annotation forbidden in cofix expression."))
      ann
  in
  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,None,bk,t)) bl in
  (id,if bl = [] then ty else CAst.make ~loc @@ CProdN(bl,ty))

(* Functions overloaded by quotifier *)
let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
  | NoBindings ->
    begin
      try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v)
      with e when CErrors.noncritical e -> ElimOnConstr clbind
    end
  | _ -> ElimOnConstr clbind

let mkNumber n =
  Number (NumTok.Signed.of_int_string (string_of_int n))

let mkTacCase with_evar = function
  | [(clear,ElimOnConstr cl),(None,None),None],None ->
      TacCase (with_evar,(clear,cl))
  (* Reinterpret numbers as a notation for terms *)
  | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
      TacCase (with_evar,
        (clear,(CAst.make @@ CPrim (mkNumber n),
         NoBindings)))
  (* Reinterpret ident as notations for variables in the context *)
  (* because we don't know if they are quantified or not *)
  | [(clear,ElimOnIdent id),(None,None),None],None ->
      TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings)))
  | ic ->
      if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
      then
        user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
      TacInductionDestruct (false,with_evar,ic)

let rec mkCLambdaN_simple_loc ?loc bll c =
  match bll with
  | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll ->
      CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,None,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
  | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
  | [] -> c

let mkCLambdaN_simple bl c = match bl with
  | [] -> c
  | h :: _ ->
    let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in
    mkCLambdaN_simple_loc ?loc bl c

let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc

let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }

let merge_occurrences loc cl = function
  | None ->
      if Locusops.clause_with_generic_occurrences cl then (None, cl)
      else
        user_err ~loc (str "Found an \"at\" clause without \"with\" clause.")
  | Some (occs, p) ->
    let ans = match occs with
    | AllOccurrences -> cl
    | _ ->
      begin match cl with
      | { onhyps = Some []; concl_occs = AllOccurrences } ->
        { onhyps = Some []; concl_occs = occs }
      | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } ->
        { cl with onhyps = Some [(occs, id), l] }
      | _ ->
        if Locusops.clause_with_generic_occurrences cl then
          user_err ~loc  (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
        else
          user_err ~loc  (str "Cannot use clause \"at\" twice.")
      end
    in
    (Some p, ans)

let deprecated_conversion_at_with =
  CWarnings.create
    ~name:"conversion_at_with" ~category:Deprecation.Version.v8_14
    (fun () -> Pp.str "The syntax [at ... with ...] is deprecated. Use [with ... at ...] instead.")

(* Auxiliary grammar rules *)

}

GRAMMAR EXTEND Gram
  GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
  bindings open_constr uconstr
  simple_intropattern in_clause clause_dft_concl hypident destruction_arg;

  (* An identifier or a quotation meta-variable *)
  id_or_meta:
    [ [ id = identref -> { id } ] ]
  ;
  open_constr:
    [ [ c = constr -> { c } ] ]
  ;
  uconstr:
    [ [ c = constr -> { c } ] ]
  ;
  destruction_arg:
    [ [ n = natural -> { (None,ElimOnAnonHyp n) }
      | test_lpar_id_rpar; c = constr_with_bindings ->
        { (Some false,destruction_arg_of_constr c) }
      | c = constr_with_bindings_arg -> { on_snd destruction_arg_of_constr c }
    ] ]
  ;
  constr_with_bindings_arg:
    [ [ c = constr_with_bindings -> { (None,c) } ] ]
  ;
  quantified_hypothesis:
    [ [ id = ident -> { NamedHyp (CAst.make ~loc id) }
      | n = natural -> { AnonHyp n } ] ]
  ;
  conversion:
    [ [ c = constr -> { (None, c) }
      | c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) }
      | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
          { deprecated_conversion_at_with ();  (* 8.14 *)
          (Some (occs,c1), c2) } ] ]
  ;
  intropatterns:
    [ [ l = LIST0 intropattern -> { l } ] ]
  ;
  ne_intropatterns:
    [ [ l = LIST1 intropattern -> { l } ] ]
  ;
  or_and_intropattern:
    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc }
      | "()" -> { IntroAndPattern [] }
      | "("; si = simple_intropattern; ")" -> { IntroAndPattern [si] }
      | "("; si = simple_intropattern; ",";
             tc = LIST1 simple_intropattern SEP "," ; ")" ->
             { IntroAndPattern (si::tc) }
      | "("; si = simple_intropattern; "&";
             tc = LIST1 simple_intropattern SEP "&" ; ")" ->
          (* (A & B & C) is translated into (A,(B,C)) *)
          { let rec pairify = function
            | ([]|[_]|[_;_]) as l -> l
            | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
          in IntroAndPattern (pairify (si::tc)) } ] ]
  ;
  equality_intropattern:
    [ [ "->" -> { IntroRewrite true }
      | "<-" -> { IntroRewrite false }
      | test_leftsquarebracket_equal; "["; "="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
  ;
  naming_intropattern:
    [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
      | "?" -> { IntroAnonymous }
      | id = ident -> { IntroIdentifier id } ] ]
  ;
  intropattern:
    [ [ l = simple_intropattern -> { l }
      | "*"  -> { CAst.make ~loc @@ IntroForthcoming true }
      | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ]
  ;
  simple_intropattern:
    [ [ pat = simple_intropattern_closed;
        l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] ->
          { let {CAst.loc=loc0;v=pat} = pat in
          let f c pat =
            let loc1 = Constrexpr_ops.constr_loc c in
            let loc = Loc.merge_opt loc0 loc1 in
            IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in
          CAst.make ~loc @@ List.fold_right f l pat } ] ]
  ;
  simple_intropattern_closed:
    [ [ pat = equality_intropattern -> { CAst.make ~loc @@ IntroAction pat }
      | pat = or_and_intropattern   -> { CAst.make ~loc @@ IntroAction (IntroOrAndPattern pat) }
      | "_" -> { CAst.make ~loc @@ IntroAction IntroWildcard }
      | pat = naming_intropattern -> { CAst.make ~loc @@ IntroNaming pat } ] ]
  ;
  simple_binding:
    [ [ "("; id = identref; ":="; c = lconstr; ")" -> { CAst.make ~loc (NamedHyp id, c) }
      | "("; n = natural; ":="; c = lconstr; ")" -> { CAst.make ~loc (AnonHyp n, c) } ] ]
  ;
  bindings:
    [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
          { ExplicitBindings bl }
      | bl = LIST1 constr -> { ImplicitBindings bl } ] ]
  ;
  constr_with_bindings:
    [ [ c = constr; l = with_bindings -> { (c, l) } ] ]
  ;
  with_bindings:
    [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ]
  ;
  hypident:
    [ [ id = id_or_meta ->
        { let id : lident = id in
        id,InHyp }
      | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
        { let id : lident = id in
        id,InHypTypeOnly }
      | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
        { let id : lident = id in
        id,InHypValueOnly }
    ] ]
  ;
  hypident_occ:
    [ [ h=hypident; occs=occs ->
        { let (id,l) = h in
        let id : lident = id in
        ((occs,id),l) } ] ]
  ;
  in_clause:
    [ [ "*"; occs=occs ->
          { {onhyps=None; concl_occs=occs} }
      | "*"; "|-"; occs=concl_occ ->
          { {onhyps=None; concl_occs=occs} }
      | "|-"; occs=concl_occ ->
          { {onhyps=Some []; concl_occs=occs} }
      | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ ->
          { {onhyps=Some hl; concl_occs=occs} }
      | hl = LIST1 hypident_occ SEP "," ->
          { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ]
  ;
  clause_dft_concl:
    [ [ "in"; cl = in_clause -> { cl }
      | occs=occs -> { {onhyps=Some[]; concl_occs=occs} }
      | -> { all_concl_occs_clause } ] ]
  ;
  clause_dft_all:
    [ [ "in"; cl = in_clause -> { cl }
      | -> { {onhyps=None; concl_occs=AllOccurrences} } ] ]
  ;
  opt_clause:
    [ [ "in"; cl = in_clause -> { Some cl }
      | "at"; occs = occs_nums -> { Some {onhyps=Some[]; concl_occs=occs} }
      | -> { None } ] ]
  ;
  concl_occ:
    [ [ "*"; occs = occs -> { occs }
      | -> { NoOccurrences } ] ]
  ;
  in_hyp_list:
    [ [ "in"; idl = LIST1 id_or_meta -> { idl }
      | -> { [] } ] ]
  ;
  in_hyp_as:
    [ [ "in"; l = LIST1 [id = id_or_meta; ipat = as_ipat -> { (id,ipat) } ] SEP "," -> { l }
      | -> { [] } ] ]
  ;
  orient_rw:
    [ [ "->" -> { true }
      | "<-" -> { false }
      | -> { true } ] ]
  ;
  simple_binder:
    [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@
                    CHole (Some (GBinderType na.CAst.v))) }
      | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) }
    ] ]
  ;
  fixdecl:
    [ [ "("; id = ident; bl=LIST0 simple_binder; ann=struct_annot;
        ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ]
  ;
  struct_annot:
    [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id }
      | -> { None } ] ]
  ;
  cofixdecl:
    [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" ->
        { (loc, id, bl, None, ty) } ] ]
  ;
  bindings_with_parameters:
    [ [ check_for_coloneq; "(";  id = ident; bl = LIST0 simple_binder;
        ":="; c = lconstr; ")" -> { (id, mkCLambdaN_simple bl c) } ] ]
  ;
  eliminator:
    [ [ "using"; el = constr_with_bindings -> { el } ] ]
  ;
  as_ipat:
    [ [ "as"; ipat = simple_intropattern -> { Some ipat }
      | -> { None } ] ]
  ;
  or_and_intropattern_loc:
    [ [ ipat = or_and_intropattern -> { ArgArg (CAst.make ~loc ipat) }
      | locid = identref -> { ArgVar locid } ] ]
  ;
  as_or_and_ipat:
    [ [ "as"; ipat = equality_intropattern ->
        { match ipat with
          | IntroRewrite _ -> user_err ~loc Pp.(str "Disjunctive/conjunctive pattern expected.")
          | IntroInjection _ -> user_err ~loc Pp.(strbrk "Found an injection pattern while a disjunctive/conjunctive pattern was expected; use " ++ str "\"injection as pattern\"" ++ strbrk " instead.")
          | _ -> assert false }
      | "as"; ipat = or_and_intropattern_loc -> { Some ipat }
      | -> { None } ] ]
  ;
  eqn_ipat:
    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) }
      | -> { None } ] ]
  ;
  as_name:
    [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
  ;
  by_tactic:
    [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac }
    | -> { None } ] ]
  ;
  rewriter :
    [ [ "!"; c = constr_with_bindings_arg -> { (Equality.RepeatPlus,c) }
      | ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.RepeatStar,c) }
      | n = natural; "!"; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) }
      | n = natural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.UpTo n,c) }
      | n = natural; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) }
      | c = constr_with_bindings_arg -> { (Equality.Precisely 1, c) }
      ] ]
  ;
  oriented_rewriter :
    [ [ b = orient_rw; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
  ;
  induction_clause:
    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
        cl = opt_clause -> { (c,(eq,pat),cl) } ] ]
  ;
  induction_clause_list:
    [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator;
        cl_tolerance = opt_clause ->
        (* Condition for accepting "in" at the end by compatibility *)
        { match ic,el,cl_tolerance with
        | [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el)
        | _,_,Some _ -> err ()
        | _,_,None -> (ic,el) } ] ]
  ;
  simple_tactic:
    [ [
      (* Basic tactics *)
        IDENT "intros"; pl = ne_intropatterns ->
          { CAst.make ~loc @@ TacAtom (TacIntroPattern (false,pl)) }
      | IDENT "intros" ->
          { CAst.make ~loc @@ TacAtom (TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
      | IDENT "eintros"; pl = ne_intropatterns ->
          { CAst.make ~loc @@ TacAtom (TacIntroPattern (true,pl)) }
      | IDENT "eintros" ->
          { CAst.make ~loc @@ TacAtom (TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) }

      | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
          inhyp = in_hyp_as -> { CAst.make ~loc @@ TacAtom (TacApply (true,false,cl,inhyp)) }
      | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
          inhyp = in_hyp_as -> { CAst.make ~loc @@ TacAtom (TacApply (true,true,cl,inhyp)) }
      | IDENT "simple"; IDENT "apply";
          cl = LIST1 constr_with_bindings_arg SEP ",";
          inhyp = in_hyp_as -> { CAst.make ~loc @@ TacAtom (TacApply (false,false,cl,inhyp)) }
      | IDENT "simple"; IDENT "eapply";
          cl = LIST1 constr_with_bindings_arg SEP",";
          inhyp = in_hyp_as -> { CAst.make ~loc @@ TacAtom (TacApply (false,true,cl,inhyp)) }
      | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
          { CAst.make ~loc @@ TacAtom (TacElim (false,cl,el)) }
      | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
          { CAst.make ~loc @@ TacAtom (TacElim (true,cl,el)) }
      | IDENT "case"; icl = induction_clause_list -> { CAst.make ~loc @@ TacAtom (mkTacCase false icl) }
      | IDENT "ecase"; icl = induction_clause_list -> { CAst.make ~loc @@ TacAtom (mkTacCase true icl) }
      | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
          { CAst.make ~loc @@ TacAtom (TacMutualFix (id,n,List.map mk_fix_tac fd)) }
      | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
          { CAst.make ~loc @@ TacAtom (TacMutualCofix (id,List.map mk_cofix_tac fd)) }

      | IDENT "pose"; bl = bindings_with_parameters ->
          { let (id,b) = bl in CAst.make ~loc @@ TacAtom (TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
      | IDENT "pose"; b = constr; na = as_name ->
          { CAst.make ~loc @@ TacAtom (TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
      | IDENT "epose"; bl = bindings_with_parameters ->
          { let (id,b) = bl in CAst.make ~loc @@ TacAtom (TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
      | IDENT "epose"; b = constr; na = as_name ->
          { CAst.make ~loc @@ TacAtom (TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
      | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl ->
          { let (id,c) = bl in CAst.make ~loc @@ TacAtom (TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
      | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacLetTac (false,na,c,p,true,None)) }
      | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl ->
          { let (id,c) = bl in CAst.make ~loc @@ TacAtom (TacLetTac (true,Names.Name id,c,p,true,None)) }
      | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacLetTac (true,na,c,p,true,None)) }
      | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
          p = clause_dft_all ->
          { CAst.make ~loc @@ TacAtom (TacLetTac (false,na,c,p,false,e)) }
      | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
          p = clause_dft_all ->
          { CAst.make ~loc @@ TacAtom (TacLetTac (true,na,c,p,false,e)) }

      (* Alternative syntax for "pose proof c as id" *)
      | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
          c = lconstr; ")" ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
      | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
          c = lconstr; ")" ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }

      (* Alternative syntax for "assert c as id by tac" *)
      | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
          c = lconstr; ")"; tac=by_tactic ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
      | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
          c = lconstr; ")"; tac=by_tactic ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }

      (* Alternative syntax for "enough c as id by tac" *)
      | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
          c = lconstr; ")"; tac=by_tactic ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
      | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
          c = lconstr; ")"; tac=by_tactic ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }

      | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
          { CAst.make ~loc @@ TacAtom (TacAssert (false,true,Some tac,ipat,c)) }
      | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
          { CAst.make ~loc @@ TacAtom (TacAssert (true,true,Some tac,ipat,c)) }

      (* Alternative syntax for "pose proof c as id by tac" *)
      | IDENT "pose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":=";
          c = lconstr; ")" ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom (TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
      | IDENT "epose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":=";
          c = lconstr; ")" ->
          { let { CAst.loc = loc; v = id } = lid in
          CAst.make ?loc @@ TacAtom ( TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
      | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
          { CAst.make ~loc @@ TacAtom (TacAssert (false,true,None,ipat,c)) }
      | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
          { CAst.make ~loc @@ TacAtom (TacAssert (true,true,None,ipat,c)) }
      | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
          { CAst.make ~loc @@ TacAtom (TacAssert (false,false,Some tac,ipat,c)) }
      | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
          { CAst.make ~loc @@ TacAtom (TacAssert (true,false,Some tac,ipat,c)) }

      | IDENT "generalize"; c = constr ->
          { CAst.make ~loc @@ TacAtom (TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
      | IDENT "generalize"; c = constr; l = LIST1 constr ->
          { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
          CAst.make ~loc @@ TacAtom (TacGeneralize (List.map gen_everywhere (c::l))) }
      | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
          na = as_name;
          l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] ->
          { CAst.make ~loc @@ TacAtom (TacGeneralize (((nl,c),na)::l)) }

      (* Derived basic tactics *)
      | IDENT "induction"; ic = induction_clause_list ->
          { CAst.make ~loc @@ TacAtom (TacInductionDestruct (true,false,ic)) }
      | IDENT "einduction"; ic = induction_clause_list ->
          { CAst.make ~loc @@ TacAtom (TacInductionDestruct(true,true,ic)) }
      | IDENT "destruct"; icl = induction_clause_list ->
          { CAst.make ~loc @@ TacAtom (TacInductionDestruct(false,false,icl)) }
      | IDENT "edestruct";  icl = induction_clause_list ->
          { CAst.make ~loc @@ TacAtom (TacInductionDestruct(false,true,icl)) }

      (* Equality and inversion *)
      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
          cl = clause_dft_concl; t=by_tactic -> { CAst.make ~loc @@ TacAtom (TacRewrite (false,l,cl,t)) }
      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
          cl = clause_dft_concl; t=by_tactic -> { CAst.make ~loc @@ TacAtom (TacRewrite (true,l,cl,t)) }
      | IDENT "dependent"; k =
          [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion }
          | IDENT "inversion" -> { FullInversion }
          | IDENT "inversion_clear" -> { FullInversionClear } ];
          hyp = quantified_hypothesis;
          ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] ->
            { CAst.make ~loc @@ TacAtom (TacInversion (DepInversion (k,co,ids),hyp)) }
      | IDENT "simple"; IDENT "inversion";
          hyp = quantified_hypothesis; ids = as_or_and_ipat;
          cl = in_hyp_list ->
            { CAst.make ~loc @@ TacAtom (TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
      | IDENT "inversion";
          hyp = quantified_hypothesis; ids = as_or_and_ipat;
          cl = in_hyp_list ->
            { CAst.make ~loc @@ TacAtom (TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
      | IDENT "inversion_clear";
          hyp = quantified_hypothesis; ids = as_or_and_ipat;
          cl = in_hyp_list ->
            { CAst.make ~loc @@ TacAtom (TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
      | IDENT "inversion"; hyp = quantified_hypothesis;
          "using"; c = constr; cl = in_hyp_list ->
            { CAst.make ~loc @@ TacAtom (TacInversion (InversionUsing (c,cl), hyp)) }

      (* Conversion *)
      | IDENT "red"; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Red, cl)) }
      | IDENT "hnf"; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Hnf, cl)) }
      | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ]; d = delta_flag;
        po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Simpl (all_with ~head:(Option.has_some h) d, po), cl)) }
      | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Cbv s, cl)) }
      | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Cbn s, cl)) }
      | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Lazy s, cl)) }
      | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Cbv (all_with ~head:false delta), cl)) }
      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (CbvVm po, cl)) }
      | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (CbvNative po, cl)) }
      | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Unfold ul, cl)) }
      | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Fold l, cl)) }
      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
          { CAst.make ~loc @@ TacAtom (TacReduce (Pattern pl, cl)) }

      (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
      | IDENT "change"; c = conversion; cl = clause_dft_concl ->
          { let (oc, c) = c in
          let p,cl = merge_occurrences loc cl oc in
          CAst.make ~loc @@ TacAtom (TacChange (true,p,c,cl)) }
      | IDENT "change_no_check"; c = conversion; cl = clause_dft_concl ->
          { let (oc, c) = c in
          let p,cl = merge_occurrences loc cl oc in
          CAst.make ~loc @@ TacAtom (TacChange (false,p,c,cl)) }
    ] ]
  ;
END