fact: Definition print_goal (g : goal gs_open) : t unit := let repeat c := (fix repeat s n := match n with | 0 => s | S n => repeat (c++s)%string n end) ""%string in sg <- match g with | Metavar _ G _ => pretty_print G end; let sep := repeat "="%string 20 in print_hyps;; print sep;; print sg;; ret tt.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)