exception AllSelectedTermsMustBeConvertible;;
exception GeneralizationInHypothesesNotImplementedYet;;
-(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
-e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
-contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
-
let generalize_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
pattern
=
+(*
let module PET = ProofEngineTypes in
let generalize_tac mk_fresh_name_callback
~pattern:(term,hyps_pat,concl_pat) status
status
in
PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
+*) assert false
;;