equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature TEST_CODE = |
7 signature TEST_CODE = |
8 sig |
8 sig |
9 type NEW (* TODO: refactor "fun me" with calcstate and remove *) |
9 type NEW (* TODO: refactor "fun me" with calcstate and remove *) |
10 val f2str : Generate.mout -> UnparseC.cterm' |
10 val f2str : Generate.mout -> TermC.as_string |
11 val TESTg_form : Calc.T -> Generate.mout |
11 val TESTg_form : Calc.T -> Generate.mout |
12 val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree |
12 val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree |
13 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree -> |
13 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree -> |
14 Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree |
14 Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree |
15 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit |
15 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit |