(** raised by elim when a MutInd is required but not found *)
exception Not_a_MutInd
-let daemon_name = "Moogle"
-let configuration_file = "/projects/helm/etc/moogle.conf.xml"
+let daemon_name = "Whelp"
+let configuration_file = "/projects/helm/etc/whelp.conf.xml"
let placeholders = [
"ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
let (id_to_uris, metasenv, term) =
match
- Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
+ Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+ ~aliases:id_to_uris ast
with
| [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
| _ -> assert false
(match subgoals with
| proof, [goal] ->
let (uri,metasenv,bo,ty) = proof in
- List.map fst (MetadataQuery.hint ~dbd (proof, goal))
+ List.map fst (MetadataQuery.experimental_hint ~dbd (proof, goal))
| _ -> assert false)
| "/elim" ->
let uri =