Patch to add a debugging string to HExtlib.split_nth reverted

[helm.git] / helm / software / components / tactics / eliminationTactics.ml

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index 6e0c223d26cf235ea2aa8b0085e91e69fc679f51..5a293bcafcd4683661b077eee638a24d7992e971 100644 (file)
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -155,7 +155,7 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* 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