let term_str = req#param "expression" in
let (context, metasenv) = ([], []) in
let id_to_uris_raw =
let term_str = req#param "expression" in
let (context, metasenv) = ([], []) in
let id_to_uris_raw =
let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
let (id_to_uris, metasenv, term) =
match
let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
let (id_to_uris, metasenv, term) =
match
- | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
+ | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
| "/hint" ->
let status = ProofEngineTypes.initial_status term metasenv in
let intros = PrimitiveTactics.intros_tac () in
| "/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
(match subgoals with
| proof, [goal] ->
let (uri,metasenv,bo,ty) = proof in
| Chat_unfinished -> ()
| Http_types.Param_not_found attr_name ->
bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
| Chat_unfinished -> ()
| Http_types.Param_not_found attr_name ->
bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
| Unbound_identifier id ->
send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
| Unbound_identifier id ->
send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
- let dbh =
- new DB.connection ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
+ let dbd =
+ Mysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~database:(Helm_registry.get "db.database")
+ ~user:(Helm_registry.get "db.user")
+ ()