val mk_arel: int -> string -> Cic.annterm
+val is_atomic:Cic.annterm -> bool
+
(****************************************************************************)
type name = string
| Rewrite of how * what * where * note
| Elim of what * using option * note
| Apply of what * note
+ | Whd of count * note
| Branch of step list list * note
val render_steps:
- (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list ->
+ (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list ->
step list ->
(what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list