+
+(* helpers ******************************************************************)
+
+let rec note_of_step = function
+ | Note s
+ | Statement (_, _, _, _, s)
+ | Inductive (_, _, s)
+ | Qed s
+ | Exact (_, s)
+ | Id s
+ | Intros (_, _, s)
+ | Cut (_, _, s)
+ | LetIn (_, _, s)
+ | Rewrite (_, _, _, _, s)
+ | Elim (_, _, _, s)
+ | Cases (_, _, s)
+ | Apply (_, s)
+ | Change (_, _, _, _, s)
+ | Clear (_, s)
+ | ClearBody (_, s)
+ | Reflexivity s
+ | Branch (_, s) -> s