blob: d6b9592176fb0fbdc337265cb5f513df94e2cda9 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Compat API / *)
let get_current_context = Declare.get_current_context
let solve = Proof.solve
let by = Declare.by
let refine_by_tactic = Proof.refine_by_tactic
(* We don't want to export this anymore, but we do for now *)
let build_by_tactic = Declare.build_by_tactic
let build_constant_by_tactic = Declare.build_constant_by_tactic
|
