new compose tactic, still undocumented.

[helm.git] / components / tactics / tactics.ml

diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml
index 527a8abb3bbb4b531a32bf95344ee767432ec2d1..1ccd2adcb0ab0d655438ca858d56770ceec76e0b 100644 (file)
--- a/components/tactics/tactics.ml
+++ b/components/tactics/tactics.ml
@@ -71,3 +71,7 @@ let symmetry = EqualityTactics.symmetry_tac
 let transitivity = EqualityTactics.transitivity_tac
 let unfold = ReductionTactics.unfold_tac
 let whd = ReductionTactics.whd_tac
+let compose = Compose.compose_tac
+
+(* keep linked *)
+let _ = CloseCoercionGraph.close_coercion_graph;;