]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tactics/tactics.ml
new compose tactic, still undocumented.
[helm.git] / components / tactics / tactics.ml
index 527a8abb3bbb4b531a32bf95344ee767432ec2d1..1ccd2adcb0ab0d655438ca858d56770ceec76e0b 100644 (file)
@@ -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;;