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
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 ->
status
in
PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
+*) assert false
;;