method disambiguate_db = disambiguate_db
method set_disambiguate_db v = {< disambiguate_db = v >}
method set_disambiguate_status
- : 'status. #g_status as 'status -> 'self
+ : 'status. (#g_status as 'status) -> 'self
= fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
end
let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
desc, `Num_interp
(fun num -> match f with `Num_interp f -> f num | _ -> assert false)
- | GrafiteAst.Ident_alias (name, uri) ->
+ | GrafiteAst.Ident_alias (_name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
let nref = NReference.reference_of_string uri in
;;
let nlookup_in_library
- interactive_user_uri_choice input_or_locate_uri item
+ _interactive_user_uri_choice _input_or_locate_uri item
=
match item with
| DisambiguateTypes.Id id ->
(wanted, hyp_paths, goal_path)
;;
-let disambiguate_reduction_kind text prefix_len = function
- | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
+let disambiguate_reduction_kind _text _prefix_len = function
+ | `Unfold (Some _t) -> assert false (* MATITA 1.0 *)
| `Normalize
| `Simpl
| `Unfold None