From c98a165ddf5c74bb70ffaa4dc65fe89c20dba8b1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 30 Apr 2007 10:51:14 +0000 Subject: [PATCH] Even if we are at depth 0, we first check in the cache for a solution, before failing. In the other case the assert false at line 76 of autocache may fail. --- helm/software/components/tactics/auto.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index e85b89b95..c7cffc8af 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -854,10 +854,6 @@ let rec auto_main tables maxm context flags elems universe cache = let goalty = CicMetaSubst.apply_subst subst goalty in (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) (* FAILURE (euristic cut) *) - if depth <= 0 then - Fail (string_of_int goalno ^ "as depth <=0"), - tables,cache,maxm (*FAILURE(depth)*) - else match cache_examine cache goalty with | Failed_in d when d >= depth -> Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), @@ -898,7 +894,7 @@ let rec auto_main tables maxm context flags elems universe cache = elems, tables, cache, maxm, flags in aux flags tables maxm cache elems - | _ -> Fail "??",tables,cache,maxm + | _ -> Fail "depth = 0",tables,cache,maxm in aux flags tables maxm cache elems -- 2.39.2