gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
| GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
- ~universe:status.GrafiteTypes.universe
+ ~automation_cache:status.GrafiteTypes.automation_cache
| GrafiteAst.Assumption _ -> Tactics.assumption
| GrafiteAst.AutoBatch (_,params) ->
Tactics.auto ~params ~dbd:(LibraryDb.instance ())
- ~universe:status.GrafiteTypes.universe
+ ~automation_cache:status.GrafiteTypes.automation_cache
| GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
~pattern what
| GrafiteAst.Demodulate (_, params) ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~params
- ~universe:status.GrafiteTypes.universe
+ ~automation_cache:status.GrafiteTypes.automation_cache
| GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
| GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
| GrafiteAst.By_just_we_proved (_, just, ty, id, t1) ->
Declarative.by_just_we_proved ~dbd:(LibraryDb.instance())
- ~universe:status.GrafiteTypes.universe just ty id t1
+ ~automation_cache:status.GrafiteTypes.automation_cache just ty id t1
| GrafiteAst.We_need_to_prove (_, t, id, t2) ->
Declarative.we_need_to_prove t id t2
| GrafiteAst.Bydone (_, t) ->
Declarative.bydone ~dbd:(LibraryDb.instance())
- ~universe:status.GrafiteTypes.universe t
+ ~automation_cache:status.GrafiteTypes.automation_cache t
| GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
Declarative.we_proceed_by_cases_on t t1
| GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
| GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
| GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) ->
Declarative.existselim ~dbd:(LibraryDb.instance())
- ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2
+ ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
| GrafiteAst.Case (_,id,params) -> Declarative.case id params
| GrafiteAst.AndElim(_,just,id1,t1,id2,t2) ->
Declarative.andelim ~dbd:(LibraryDb.instance ())
- ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2
+ ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
| GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
- ~universe:status.GrafiteTypes.universe termine t1 t2 cont
+ ~automation_cache:status.GrafiteTypes.automation_cache termine t1 t2 cont
let classify_tactic tactic =
match tactic with
| GrafiteAst.Index (loc,None,uri) ->
assert false (* TODO: for user input *)
| GrafiteAst.Index (loc,Some key,uri) ->
- let universe = Universe.index
- status.GrafiteTypes.universe key (CicUtil.term_of_uri uri) in
- let status = {status with GrafiteTypes.universe = universe} in
+ let universe =
+ status.GrafiteTypes.automation_cache.AutomationCache.univ
+ in
+ let universe = Universe.index universe key (CicUtil.term_of_uri uri) in
+ let cache = {
+ status.GrafiteTypes.automation_cache with AutomationCache.univ = universe }
+ in
+ let status = { status with GrafiteTypes.automation_cache = cache } in
(* debug
let msg =
let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
in
let universe,status =
List.fold_left add_to_universe
- (status.GrafiteTypes.universe,status)
+ (status.GrafiteTypes.automation_cache.AutomationCache.univ,status)
uris_to_index
in
+ let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in
{status with
GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
- GrafiteTypes.universe = universe},
+ GrafiteTypes.automation_cache = cache },
lemmas
let add_coercion ~pack_coercion_obj ~add_composites status uri arity
proof_status = GrafiteTypes.No_proof;
objects = [];
coercions = CoercDb.empty_coerc_db;
- universe = Universe.empty;
+ automation_cache = AutomationCache.empty;
baseuri = baseuri;
ng_status = GrafiteTypes.CommandMode lexicon_status;
}
proof_status: proof_status;
objects: UriManager.uri list;
coercions: CoercDb.coerc_db;
- universe:Universe.universe;
+ automation_cache:AutomationCache.cache;
baseuri: string;
ng_status: ng_status;
}
proof_status: proof_status;
objects: UriManager.uri list;
coercions: CoercDb.coerc_db;
- universe:Universe.universe;
+ automation_cache:AutomationCache.cache;
baseuri: string;
ng_status: ng_status;
}
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+proofEngineTypes.cmi:
proofEngineHelpers.cmi: proofEngineTypes.cmi
+proofEngineReduction.cmi:
continuationals.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
+hashtbl_equiv.cmi:
metadataQuery.cmi: proofEngineTypes.cmi
+universe.cmi:
autoTypes.cmi: proofEngineTypes.cmi
+autoCache.cmi:
+paramodulation/utils.cmi:
+closeCoercionGraph.cmi:
+paramodulation/subst.cmi:
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
paramodulation/founif.cmi: paramodulation/subst.cmi
paramodulation/equality.cmi
paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
paramodulation/indexing.cmi paramodulation/equality.cmi
+automationCache.cmi: universe.cmi paramodulation/saturation.cmi
variousTactics.cmi: proofEngineTypes.cmi
compose.cmi: proofEngineTypes.cmi
introductionTactics.cmi: proofEngineTypes.cmi
auto.cmi: universe.cmi proofEngineTypes.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
+inversion_principle.cmi:
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
+fourier.cmi:
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
+history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
paramodulation/indexing.cmx paramodulation/founif.cmx \
paramodulation/equality.cmx paramodulation/saturation.cmi
+automationCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
+ automationCache.cmi
+automationCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \
+ automationCache.cmi
variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
variousTactics.cmi
variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
paramodulation/equality_indexing.mli\
paramodulation/indexing.mli \
paramodulation/saturation.mli \
+ automationCache.mli \
variousTactics.mli \
compose.mli \
introductionTactics.mli eliminationTactics.mli negationTactics.mli \
(***************** applyS *******************)
let new_metasenv_and_unify_and_t
- dbd flags universe proof goal ?tables newmeta' metasenv'
+ dbd flags automation_cache proof goal ?tables newmeta' metasenv'
context term' ty termty goal_arity
=
- let ppterm = ppterm context in
+(* let ppterm = ppterm context in *)
let (consthead,newmetasenv,arguments,_) =
TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
let term'' =
(PrimitiveTactics.apply_tac term'')
(proof''',goal)
in
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
let (active, passive,bag), cache, maxm =
init_cache_and_tables ~dbd flags.use_library false (* was true *)
true false universe
| _ -> 0
let apply_smart
- ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal)
+ ~dbd ~term ~subst ~automation_cache ?tables ~params:(univ,params) (proof, goal)
=
let module T = CicTypeChecker in
let module R = CicReduction in
let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params ~for_applyS:true () in
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
let universe = universe_of_params metasenv context universe univ in
+ let automation_cache = { automation_cache with AutomationCache.univ = universe } in
+
let newmeta = CicMkImplicit.new_meta metasenv subst in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
let goal_arity = count_prods context ty in
let proof, gl, active, passive =
- new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
+ new_metasenv_and_unify_and_t dbd flags automation_cache proof goal ?tables
newmeta' metasenv' context term' ty termty goal_arity
in
proof, gl, active, passive
None,cache
;;
-let applyS_tac ~dbd ~term ~params ~universe =
+let applyS_tac ~dbd ~term ~params ~automation_cache =
ProofEngineTypes.mk_tactic
(fun status ->
try
let proof, gl,_,_ =
- apply_smart ~dbd ~term ~subst:[] ~params ~universe status
+ apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status
in
proof, gl
with
| CicTypeChecker.TypeCheckerFailure msg ->
raise (ProofEngineTypes.Fail msg))
-let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
+let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
let _,metasenv,_subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params () in
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
let universe = universe_of_params metasenv context universe univ in
let use_library = flags.use_library in
let tables,cache,newmeta =
raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
;;
-let auto_tac ~dbd ~params ~universe =
- ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
+let auto_tac ~dbd ~params ~automation_cache =
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);;
let eq_of_goal = function
| Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
(* performs steps of rewrite with the universe, obtaining if possible
* a trivial goal *)
-let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)=
+let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)=
let _,metasenv,_subst,_,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let steps = int_of_string (string params "steps" "1") in
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
let universe = universe_of_params metasenv context universe univ in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
(ProofEngineTypes.Fail (lazy
("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
;;
-let solve_rewrite_tac ~params ~universe () =
- ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params)
+let solve_rewrite_tac ~params ~automation_cache () =
+ ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params)
;;
(* Demodulate thorem *)
) None candidates
;;
-let demodulate_theorem ~universe uri =
+let demodulate_theorem ~automation_cache uri =
let eq_uri =
match LibraryObjects.eq_URI () with
| Some (uri) -> uri
MetadataQuery.close_with_types set [] context
in
(* retrieve equations from the universe universe *)
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
let equations =
retrieve_equations true signature universe AutoCache.cache_empty context []
in
(* NEW DEMODULATE *)
-let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)=
+let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
let universe = universe_of_params metasenv context universe univ in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let initgoal = [], metasenv, ty in
~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
;;
-let demodulate_tac ~dbd ~params ~universe =
- ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);;
+let demodulate_tac ~dbd ~params ~automation_cache =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);;
let pp_proofterm = Equality.pp_proofterm;;
val auto_tac:
dbd:HSql.dbd ->
params:auto_params ->
- universe:Universe.universe ->
+ automation_cache:AutomationCache.cache ->
ProofEngineTypes.tactic
val applyS_tac:
dbd:HSql.dbd ->
term: Cic.term ->
params:auto_params ->
- universe:Universe.universe ->
+ automation_cache:AutomationCache.cache ->
ProofEngineTypes.tactic
val demodulate_tac :
dbd:HSql.dbd ->
params:auto_params ->
- universe:Universe.universe ->
+ automation_cache:AutomationCache.cache ->
ProofEngineTypes.tactic
val demodulate_theorem :
- universe:Universe.universe ->
+ automation_cache:AutomationCache.cache ->
UriManager.uri ->
Cic.term * Cic.term
val solve_rewrite_tac:
params:auto_params ->
- universe:Universe.universe ->
+ automation_cache:AutomationCache.cache ->
unit -> ProofEngineTypes.tactic
type auto_status =
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+type cache = {
+ univ : Universe.universe;
+ tables : Saturation.active_table * Saturation.passive_table;
+}
+
+
+let empty = {
+ univ = Universe.empty;
+ tables = (Saturation.make_active [], Saturation.make_passive []);
+}
+
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+type cache = {
+ univ : Universe.universe;
+ tables : Saturation.active_table * Saturation.passive_table;
+}
+
+
+val empty : cache
+
type just = [ `Term of Cic.term | `Auto of Auto.auto_params ]
-let mk_just ~dbd ~universe =
+let mk_just ~dbd ~automation_cache =
function
`Auto (l,params) ->
Tactics.auto ~dbd
- ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~universe
+ ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~automation_cache
| `Term t -> Tactics.apply t
;;
(fun _ metasenv ugraph -> ty,metasenv,ugraph))
;;
-let by_just_we_proved ~dbd ~universe just ty id ty' =
- let just = mk_just ~dbd ~universe just in
+let by_just_we_proved ~dbd ~automation_cache just ty id ty' =
+ let just = mk_just ~dbd ~automation_cache just in
match id with
None ->
(match ty' with
~continuations:[ Tacticals.id_tac ; continuation ]
;;
-let bydone ~dbd ~universe just =
- mk_just ~dbd ~universe just
+let bydone ~dbd ~automation_cache just =
+ mk_just ~dbd ~automation_cache just
;;
let we_need_to_prove t id ty =
ProofEngineTypes.mk_tactic aux
;;
-let existselim ~dbd ~universe just id1 t1 id2 t2 =
+let existselim ~dbd ~automation_cache just id1 t1 id2 t2 =
let aux (proof, goal) =
let (n,metasenv,_subst,bo,ty,attrs) = proof in
let metano,context,_ = CicUtil.lookup_meta goal metasenv in
fun _ _ _ ~typ ->
incr i;
if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
- (mk_just ~dbd ~universe just)
+ (mk_just ~dbd ~automation_cache just)
]) (proof', goal)
in
ProofEngineTypes.mk_tactic aux
;;
-let andelim ~dbd ~universe just id1 t1 id2 t2 =
+let andelim ~dbd ~automation_cache just id1 t1 id2 t2 =
Tacticals.thens
~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
~continuations:
fun _ _ _ ~typ ->
incr i;
if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
- (mk_just ~dbd ~universe just) ]
+ (mk_just ~dbd ~automation_cache just) ]
;;
-let rewritingstep ~dbd ~universe lhs rhs just last_step =
+let rewritingstep ~dbd ~automation_cache lhs rhs just last_step =
let aux ((proof,goal) as status) =
let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
let _,context,gty = CicUtil.lookup_meta goal metasenv in
else params
in
if params = params' then
- Tactics.auto ~dbd ~params:(univ, params) ~universe
+ Tactics.auto ~dbd ~params:(univ, params) ~automation_cache
else
Tacticals.first
- [Tactics.auto ~dbd ~params:(univ, params) ~universe ;
- Tactics.auto ~dbd ~params:(univ, params') ~universe]
+ [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ;
+ Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
| `Term just -> Tactics.apply just
| `SolveWith term ->
- Tactics.solve_rewrite ~universe ~params:([term],["steps","1"]) ()
+ Tactics.solve_rewrite ~automation_cache ~params:([term],["steps","1"]) ()
| `Proof ->
Tacticals.id_tac
in
val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
val by_just_we_proved :
- dbd:HSql.dbd -> universe:Universe.universe ->
+ dbd:HSql.dbd -> automation_cache:AutomationCache.cache ->
just -> Cic.term -> string option -> Cic.term option ->
ProofEngineTypes.tactic
-val bydone : dbd:HSql.dbd -> universe:Universe.universe ->
+val bydone : dbd:HSql.dbd -> automation_cache:AutomationCache.cache ->
just -> ProofEngineTypes.tactic
val we_need_to_prove :
val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
val existselim :
- dbd:HSql.dbd -> universe:Universe.universe -> just ->
+ dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> just ->
string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic
val andelim :
- dbd:HSql.dbd -> universe:Universe.universe -> just ->
+ dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> just ->
string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
val rewritingstep :
- dbd:HSql.dbd -> universe:Universe.universe ->
+ dbd:HSql.dbd -> automation_cache:AutomationCache.cache ->
(string option * Cic.term) option -> Cic.term ->
[ `Term of Cic.term | `Auto of Auto.auto_params
| `Proof | `SolveWith of Cic.term] ->
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jul 2 19:37:38 CEST 2008 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 16 11:28:06 CEST 2009 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyP : term:Cic.term -> ProofEngineTypes.tactic
dbd:HSql.dbd ->
term:Cic.term ->
params:Auto.auto_params ->
- universe:Universe.universe -> ProofEngineTypes.tactic
+ automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic
val assumption : ProofEngineTypes.tactic
val auto :
dbd:HSql.dbd ->
params:Auto.auto_params ->
- universe:Universe.universe -> ProofEngineTypes.tactic
+ automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic
val cases_intros :
?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
val demodulate :
dbd:HSql.dbd ->
params:Auto.auto_params ->
- universe:Universe.universe -> ProofEngineTypes.tactic
+ automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic
val destruct : Cic.term list option -> ProofEngineTypes.tactic
val elim_intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val solve_rewrite :
params:Auto.auto_params ->
- universe:Universe.universe -> unit -> ProofEngineTypes.tactic
+ automation_cache:AutomationCache.cache -> unit -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
- ~universe:grafite_status.GrafiteTypes.universe) proof_status
+ ~automation_cache:grafite_status.GrafiteTypes.automation_cache)
+ proof_status
in
let proof_term =
let irl =
projects / helm.git / commitdiff