X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.mli;h=34c7ba670216e332a02711e7b0c112d67a7991e2;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=3cc482a8ca9fe9faa6d09d971c46126200c2e198;hpb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index 3cc482a8c..34c7ba670 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -53,16 +53,19 @@ type step = Note of note | Statement of flavour * name * what * body * note | Qed of note | Id of note + | Exact of what * note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note | Rewrite of how * what * where * pattern * note | Elim of what * using option * pattern * note + | Cases of what * pattern * note | Apply of what * note | Change of inferred * what * where * pattern * note | Clear of hyp list * note | ClearBody of hyp * note | Branch of step list list * note + | Reflexivity of note val render_steps: (what, inferred, [> `Whd] as 'b, what CicNotationPt.obj, hyp) GrafiteAst.statement list -> @@ -74,3 +77,6 @@ val count_steps: val count_nodes: int -> step list -> int + +val note_of_step: + step -> note