exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
exception TheSelectedTermsMustLiveInTheGoalContext
exception AllSelectedTermsMustBeConvertible;;
-exception CannotGeneralizeInHypotheses;;
-
-(* 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'?????? *)
+exception GeneralizationInHypothesesNotImplementedYet;;
let generalize_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
let generalize_tac mk_fresh_name_callback
~pattern:(term,hyps_pat,concl_pat) status
=
- if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ;
+ if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
let (proof, goal) = status in
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let terms_with_context =
- ProofEngineHelpers.select ~context ~term:ty ~pattern:(term,concl_pat) in
+ let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+ let selected_hyps,terms_with_context =
+ ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
let typ,term =
match terms_with_context, term with
[], None ->