(* ANCORA DA DEBUGGARE *)
+(* 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 *)
let generalize_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
let module P = PrimitiveTactics in
~what:term
~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
~where:ty)
- )))
+ )))
~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
~status
;;