| Intros of count option * name list * note
| Cut of name * what * note
| LetIn of name * what * note
+ | LApply of name * what * note
| Rewrite of how * what * where * pattern * note
| Elim of what * using option * pattern * note
| Cases of what * pattern * note
let mk_statement flavour name t v =
let name = match name with Some name -> name | None -> assert false in
- let obj = N.Theorem (flavour, name, t, v) in
+ let obj = N.Theorem (flavour, name, t, v, `Regular) in
G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
let mk_qed =
let tactic = G.LetIn (floc, what, name) in
mk_tactic tactic punctation
+let mk_lapply name what punctation =
+ let tactic = G.LApply (floc, false, None, [], what, name) in
+ mk_tactic tactic punctation
+
let mk_rewrite direction what where pattern punctation =
let direction = if direction then `RightToLeft else `LeftToRight in
let pattern, rename = match where with
| Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a
| Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a
| LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
+ | LApply (n, t, s) -> mk_lapply n t sep :: mk_tacnote s a
| Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
| Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
| Cases (t, e, s) -> mk_cases t e sep :: mk_tacnote s a
| Exact (t, _)
| Cut (_, t, _)
| LetIn (_, t, _)
+ | LApply (_, t, _)
| Apply (t, _) -> count a (H.cic t)
| Rewrite (_, t, _, p, _)
| Elim (t, _, p, _)
| Intros (_, _, s)
| Cut (_, _, s)
| LetIn (_, _, s)
+ | LApply (_, _, s)
| Rewrite (_, _, _, _, s)
| Elim (_, _, _, s)
| Cases (_, _, s)