+ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+ | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+ | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit
+ | [ IDENT "qed" | IDENT "Qed" ] ->
+ return_command loc (TacticAst.Qed None)
+ | [ IDENT "print" | IDENT "Print" ];
+ print_kind = print_kind ->
+ return_command loc (TacticAst.Print print_kind)
+ | [ IDENT "save" | IDENT "Save" ]; name = IDENT ->
+ return_command loc (TacticAst.Qed (Some name))
+ | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (flavour, name, typ, 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),_,_) :: _ ->
+ fail loc ("No type given for " ^ name)
+ | _ -> assert false
+ in
+ let body = CicAst.Ident (name,None) in
+ TacticAst.Theorem(`Definition, Some name, ty,
+ Some (CicAst.LetRec (ind_kind, defs, body)))
+
+ | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ return_command loc (TacticAst.Inductive (params, ind_types))
+ | [ IDENT "coinductive" | 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
+ return_command loc (TacticAst.Inductive (params, ind_types))
+ | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT ->
+ return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some [])))
+ | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI ->
+ return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some [])))
+ | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
+ | [ IDENT "undo" | IDENT "Undo" ]; steps = OPT NUM ->
+ return_command loc (TacticAst.Undo (int_opt steps))
+ | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
+ return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING ->
+ return_command loc (TacticAst.Baseuri uri)
+ | [ IDENT "basedir" | IDENT "Basedir" ]; uri = OPT QSTRING ->
+ return_command loc (TacticAst.Basedir uri)
+ | [ IDENT "check" | IDENT "Check" ]; t = term ->
+ return_command loc (TacticAst.Check t)
+(*
+ | [ IDENT "alias" | IDENT "Alias" ]; spec = alias_spec ->
+ return_command loc (TacticAst.Alias spec)
+*)