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 (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let selected_hyps,terms_with_context =
ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
- assert (selected_hyps = []);
let typ,term =
match terms_with_context, term with
[], None ->