exception Not_a_MutInd
let daemon_name = "Whelp"
-let configuration_file = "/projects/helm/etc/whelp.conf.xml"
+let configuration_file = "searchEngine.conf.xml"
let placeholders = [
"ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
| "/match" -> Whelp.match_term ~dbd term
| "/instance" -> Whelp.instance ~dbd term
| "/hint" ->
- let status = ProofEngineTypes.initial_status term metasenv in
+ let status = ProofEngineTypes.initial_status term metasenv [] in
let intros = PrimitiveTactics.intros_tac () in
let subgoals = ProofEngineTypes.apply_tactic intros status in
(match subgoals with