From 2891805f46435d70ef14e81cc2df7c729fe258ad Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 15:19:25 +0000 Subject: [PATCH] auto always uses the context (even if paramodulation) to try to close goals left open by paramod --- helm/software/components/tactics/autoTactic.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index dd9e8c186..4b713d464 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -80,17 +80,18 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = let _, metasenv, _, _ = proof in let _, context, goalty = CicUtil.lookup_meta goal metasenv in let cache = + let cache = + AutoCache.cache_add_context context metasenv AutoCache.cache_empty + in if use_only_paramod then (* only paramod *) - AutoCache.cache_empty + cache else - let cache = - AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty - in - AutoCache.cache_add_context context metasenv cache + AutoCache.cache_add_library dbd proof [goal] cache in let oldmetasenv = metasenv in let flags = { - AutoTypes.maxdepth = depth; + AutoTypes.maxdepth = + if use_only_paramod then 2 else depth; AutoTypes.maxwidth = width; AutoTypes.timeout = if timeout = 0 then float_of_int timeout -- 2.39.2