From ecb8a1b6b6bd0a1e9757d2aadc14cf34a47b97ff Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 15:13:43 +0000
Subject: [PATCH] if parameter type is given, this assert is false

---
 helm/software/components/tactics/auto.ml | 1 -
 1 file changed, 1 deletion(-)

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
-- 
2.39.2