(* $Id$ *)
+module PEH = ProofEngineHelpers
+
exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
- | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
+ | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
~pattern what
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
| GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Subst _ -> Tactics.subst
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
(* Implementazioni Aggiunte *)
| _ -> false
let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
- let module PEH = ProofEngineHelpers in
(* let print_m name metasenv =
prerr_endline (">>>>> " ^ name);
prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)