From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 15:13:43 +0000 (+0000)
Subject: if parameter type is given, this assert is false
X-Git-Tag: make_still_working~5736
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ecb8a1b6b6bd0a1e9757d2aadc14cf34a47b97ff;p=helm.git

if parameter type is given, this assert is false
---

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