- [Tactics.auto ~dbd ~params ~universe ;
- Tactics.auto ~dbd ~params:params' ~universe]
- | `Term just ->
- let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context just
- CicUniv.empty_ugraph
- in
- Tactics.solve_rewrite
- ~universe:(Universe.index Universe.empty
- (Universe.key ty) just) ~steps:1 ()
- (* Tactics.apply just *)
+ [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ;
+ Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
+ | `Term just -> Tactics.apply just
+ | `SolveWith term ->
+ Tactics.demodulate ~automation_cache ~dbd
+ ~params:(Some [term],
+ ["all","1";"steps","1"; "use_context","false"])
+ | `Proof ->
+ Tacticals.id_tac