+
+ command: [[
+ [ IDENT "set" ]; n = QSTRING; v = QSTRING ->
+ TacticAst.Set (loc, n, v)
+ | [ IDENT "drop" ] -> TacticAst.Drop loc
+ | [ IDENT "qed" ] -> TacticAst.Qed loc
+ | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))
+ | flavour = theorem_flavour; name = IDENT;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body))
+ | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
+ defs = let_defs ->
+ let name,ty =
+ match defs with
+ | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
+ | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
+ | _ -> assert false
+ in
+ let body = CicAst.Ident (name,None) in
+ TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty,
+ Some (CicAst.LetRec (ind_kind, defs, body))))
+
+ | [ IDENT "inductive" ]; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
+ | [ IDENT "coinductive" ]; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ let ind_types = (* set inductive flags to false (coinductive) *)
+ List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
+ ind_types
+ in
+ TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
+ | IDENT "coercion" ; name = IDENT ->
+ TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
+ | IDENT "coercion" ; name = URI ->
+ TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
+ | IDENT "alias" ; spec = alias_spec ->
+ TacticAst.Alias (loc, spec)
+ | IDENT "record" ; (params,name,ty,fields) = record_spec ->
+ TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
+ | IDENT "include" ; path = QSTRING ->
+ TacticAst.Include (loc,path)
+ | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
+ let uris = List.map UriManager.uri_of_string uris in
+ TacticAst.Default (loc,what,uris)
+ ]];
+
+ executable: [
+ [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
+ | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
+ | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)