g_tactic.mlg

(************************************************************************)
(*         *   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)         *)
(************************************************************************)

DECLARE PLUGIN "coq-core.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 Pcoq


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 Pcoq.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 Pcoq.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 Pcoq.Lookahead in
  to_entry "test_lpar_idnum_coloneq" begin
    lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":="
  end

let test_leftsquarebracket_equal =
  let open Pcoq.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 =
  Pcoq.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 Pcoq.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 *)

open Pvernac.Vernac_

}

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

  int_or_var:
    [ [ n = integer  -> { ArgArg n }
      | id = identref -> { ArgVar id } ] ]
  ;
  nat_or_var:
    [ [ n = natural  -> { ArgArg n }
      | id = identref -> { ArgVar id } ] ]
  ;
  (* 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) } ] ]
  ;
  occs_nums:
    [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
      | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ]
  ;
  occs:
    [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
  ;
  pattern_occ:
    [ [ c = constr; nl = occs -> { (nl,c) } ] ]
  ;
  ref_or_pattern_occ:
    (* If a string, it is interpreted as a ref
       (anyway a Coq string does not reduce) *)
    [ [ c = smart_global; nl = occs -> { nl,Inl c }
      | c = constr; nl = occs -> { nl,Inr c } ] ]
  ;
  unfold_occ:
    [ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
  ;
  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 } ] ]
  ;
  red_flag:
    [ [ IDENT "beta" -> { [FBeta] }
      | IDENT "iota" -> { [FMatch;FFix;FCofix] }
      | IDENT "match" -> { [FMatch] }
      | IDENT "fix" -> { [FFix] }
      | IDENT "cofix" -> { [FCofix] }
      | IDENT "zeta" -> { [FZeta] }
      | IDENT "delta"; d = delta_flag -> { [d] }
      | IDENT "head" -> { [FHead] }
    ] ]
  ;
  delta_flag:
    [ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl }
      | "["; idl = LIST1 smart_global; "]" -> { FConst idl }
      | -> { FDeltaBut [] }
    ] ]
  ;
  strategy_flag:
    [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
      | h = OPT [ IDENT "head" -> { () } ]; d = delta_flag -> { all_with ~head:(Option.has_some h) d }
    ] ]
  ;
  red_expr:
    [ [ IDENT "red" -> { Red }
      | IDENT "hnf" -> { Hnf }
      | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ];
        d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with ~head:(Option.has_some h) d,po) }
      | IDENT "cbv"; s = strategy_flag -> { Cbv s }
      | IDENT "cbn"; s = strategy_flag -> { Cbn s }
      | IDENT "lazy"; s = strategy_flag -> { Lazy s }
      | IDENT "compute"; delta = delta_flag -> { Cbv (all_with ~head:false delta) }
      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po }
      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po }
      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul }
      | IDENT "fold"; cl = LIST1 constr -> { Fold cl }
      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl }
      | s = IDENT -> { ExtraRedExpr s } ] ]
  ;
  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