- match superposition with
- | true ->
- (* this is the ugly hack to debug paramod *)
- Saturation.superposition_tac
- ~target ~table ~subterms_only ~demod_table (proof,goal)
- | false ->
- if not newauto then
- auto_tac_old ~depth ~width ~dbd () (proof,goal)
- else
- (* this is the real auto *)
- 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 *)
- cache
- else
- AutoCache.cache_add_library dbd proof [goal] cache
- in
- let oldmetasenv = metasenv in
- let flags = {
- AutoTypes.maxdepth =
- if use_only_paramod then 2 else depth;
- AutoTypes.maxwidth = width;
- AutoTypes.timeout =
- if timeout = 0 then float_of_int timeout
- else Unix.gettimeofday() +. (float_of_int timeout);
- AutoTypes.use_paramod = use_paramod;
- AutoTypes.use_only_paramod = use_only_paramod;
- AutoTypes.dont_cache_failures = false
- }
- in
- match Auto.auto dbd cache context metasenv [goal] flags with
- | None,cache ->
- raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
- | Some (subst,metasenv),cache ->
- let proof,metasenv =
- ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal (CicMetaSubst.apply_subst subst) metasenv
- in
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:metasenv
- in
- proof,opened
-;;
+ let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+ let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ if not newauto then
+ auto_tac_old ~depth ~width ~dbd () (proof,goal)
+ else
+ ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal)