Bad hack to avoid failure of conversion (unfolding) in "unfold t in H" where

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

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 6a1ab20e6b798a4153720d54c1a5d6f1804dfbeb..ba80608d21b992ca6f0c2ef3d816565c160dc233 100644 (file)
--- 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