(** 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";
| "/hint" -> "Hint"
| "/locate" -> "Locate"
| "/elim" -> "Elim"
+ | "/instance" -> "Instance"
| _ -> ""
(* given a uri with a query part in input try to find in it a string
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
let uris =
match req#path with
| "/match" -> MetadataQuery.match_term ~dbd term
+ | "/instance" -> MetadataQuery.instance ~dbd term
| "/hint" ->
let status = ProofEngineTypes.initial_status term metasenv in
let intros = PrimitiveTactics.intros_tac () in
(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 =
end
| "/hint"
| "/elim"
+ | "/instance"
| "/match" -> exec_action dbd req outchan
| invalid_request ->
Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))