+ | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+ G.UnificationHint (loc, t, n)
+ | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
+ G.NObj (loc, N.Record (params,name,ty,fields))
+ ]];
+
+ grafite_command: [ [
+ IDENT "set"; n = QSTRING; v = QSTRING ->
+ G.Set (loc, n, v)
+ | IDENT "drop" -> G.Drop loc
+ | IDENT "print"; s = IDENT -> G.Print (loc,s)
+ | IDENT "qed" -> G.Qed loc
+ | IDENT "variant" ; name = IDENT; SYMBOL ":";
+ typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
+ G.Obj (loc,
+ N.Theorem
+ (`Variant,name,typ,Some (N.Ident (newname, None))))
+ | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ G.Obj (loc, N.Theorem (flavour, name, typ, body))
+ | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ body = term ->
+ G.Obj (loc,
+ N.Theorem (flavour, name, N.Implicit, Some body))
+ | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
+ G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
+ | LETCOREC ; defs = let_defs ->
+ mk_rec_corec `CoInductive defs loc
+ | LETREC ; defs = let_defs ->
+ mk_rec_corec `Inductive defs loc
+ | IDENT "inductive"; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ G.Obj (loc, N.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
+ G.Obj (loc, N.Inductive (params, ind_types))