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
;;
| `Term just -> Tactics.apply just
| `SolveWith term ->
Tactics.demodulate ~automation_cache ~dbd
- ~params:([term],
+ ~params:(Some [term],
["all","1";"steps","1"; "use_context","false"])
| `Proof ->
Tacticals.id_tac