(* roba seria ------------------------------------------------------------- *)
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp])
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))])
?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in