X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=ba80608d21b992ca6f0c2ef3d816565c160dc233;hb=5fccdd2191e822f5ed140336bd15308e499d9dda;hp=6a1ab20e6b798a4153720d54c1a5d6f1804dfbeb;hpb=66faca1dc849662e27d760b950294ef66a5741b3;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 6a1ab20e6..ba80608d2 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -992,7 +992,6 @@ let add_to_cache_and_del_from_orlist_if_green_cut
   | None -> assert false
   | Some (canonical_ctx , gty) ->
       let goalno,depth,sort = g in
-      assert (sort = P);
       let irl = mk_irl canonical_ctx in
       let goal = Cic.Meta(goalno, irl) in
       let proof = CicMetaSubst.apply_subst s goal in