val interactive_user_uri_choice :
selection_mode:[`SINGLE | `MULTIPLE] ->
?ok:string ->
?enable_button_for_non_vars:bool ->
title:string -> msg:string -> id:string -> string list -> string list
val interactive_interpretation_choice :
val interactive_user_uri_choice :
selection_mode:[`SINGLE | `MULTIPLE] ->
?ok:string ->
?enable_button_for_non_vars:bool ->
title:string -> msg:string -> id:string -> string list -> string list
val interactive_interpretation_choice :
- (string * string) list list -> int
- val input_or_locate_uri : title:string -> UriManager.uri
+ (string * string) list list -> int list
+ val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri
- C.output_html (`Msg (`T "Result:"));
- MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" result;
+ HelmLogger.log (`Msg (`T "Result:"));
+ MQueryUtil.text_of_result (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
"Disambiguation phase started: up to %d cases will be tried"
tests_no)));
(* and now we compute the list of all possible assignments from *)
"Disambiguation phase started: up to %d cases will be tried"
tests_no)));
(* and now we compute the list of all possible assignments from *)
let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
- let term,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
+ let term,_,metasenv'',_ = (* TASSI: FIXME what are we doning here?*)
+ CicRefine.type_of_aux' metasenv' context expr CicUniv.empty_ugraph
- (known_ids @ dom', resolve_id'), metasenv',term
+ List.map
+ (fun (resolve_id',term,metasenv') ->
+ (known_ids @ dom', resolve_id'), metasenv',term
+ ) res