function
`Auto (l,params) ->
Tactics.auto ~dbd
- ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~automation_cache
+ ~params:(l,("skip_trie_filtering","1")::(*("skip_context","1")::*)params) ~automation_cache
| `Term t -> Tactics.apply t
;;
Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
| `Term just -> Tactics.apply just
| `SolveWith term ->
- Tactics.solve_rewrite ~automation_cache ~params:([term],["steps","1"]) ()
+ Tactics.demodulate ~automation_cache ~dbd
+ ~params:(Some [term],
+ ["all","1";"steps","1"; "use_context","false"])
| `Proof ->
Tacticals.id_tac
in
;;
let we_proceed_by_induction_on t pat =
- let pattern = None, [], Some pat in
+(* let pattern = None, [], Some pat in *)
Tactics.elim_intros ~depth:0 (*~pattern*) t
;;