From 4aa1a49628876bf1d72d44537d545d1b5562df0f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 1 Oct 2006 13:02:29 +0000 Subject: [PATCH 1/1] when use_only_paramod is true do not calculate the universe for applicative reasoning --- helm/software/components/tactics/autoTactic.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index bb5399197..dd9e8c186 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -33,11 +33,11 @@ let bool params name default = try let s = List.assoc name params in - if s = "" || s = "1" || s = "true" || s = "yes" then true - else if s = "0" || s = "false" || s = "no" then false + if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true + else if s = "0" || s = "false" || s = "no" || s= "off" then false else let msg = "Unrecognized value for parameter "^name^"\n" in - let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in + let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in raise (ProofEngineTypes.Fail (lazy msg)) with Not_found -> default ;; @@ -80,9 +80,14 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = let _, metasenv, _, _ = proof in let _, context, goalty = CicUtil.lookup_meta goal metasenv in let cache = - AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty + if use_only_paramod then (* only paramod *) + AutoCache.cache_empty + else + let cache = + AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty + in + AutoCache.cache_add_context context metasenv cache in - let cache = AutoCache.cache_add_context context metasenv cache in let oldmetasenv = metasenv in let flags = { AutoTypes.maxdepth = depth; -- 2.39.2