* http://cs.unibo.it/helm/.
*)
-val assumption_tac: ProofEngineTypes.tactic
+exception AllSelectedTermsMustBeConvertible;;
-val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic
+val assumption_tac: ProofEngineTypes.tactic
+val generalize_tac: terms:Cic.term list -> ProofEngineTypes.tactic
(*
val decide_equality_tac: ProofEngineTypes.tactic