Added Decompose tactic

[helm.git] / helm / gTopLevel / equalityTactics.ml

diff --git a/helm/gTopLevel/equalityTactics.ml b/helm/gTopLevel/equalityTactics.ml
index afa210119fe9ce50304b53b90a2820d800290e7c..79b5b1dbe499e50a6b2d26788a023bcf30081554 100644 (file)
--- a/helm/gTopLevel/equalityTactics.ml
+++ b/helm/gTopLevel/equalityTactics.ml
@@ -182,6 +182,8 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
 ;;
 
 
+(* All these tacs do is applying the right constructor/theorem *)
+
 let reflexivity_tac =
   IntroductionTactics.constructor_tac ~n:1
 ;;