* http://cs.unibo.it/helm/.
*)
-val injection_tac: term:Cic.term -> ProofEngineTypes.tactic
-val discriminate_tac: term:Cic.term -> ProofEngineTypes.tactic
-val decide_equality_tac: ProofEngineTypes.tactic
-val compare_tac: term:Cic.term -> ProofEngineTypes.tactic
-
+(* Performs a recursive comparisons of the two sides of an equation
+ looking for constructors. If the two sides differ on two constructors,
+ it closes the current goal. If they differ by other two terms it introduces
+ an equality. *)
+val destruct_tac: term:Cic.term -> ProofEngineTypes.tactic