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 eval_with_new_aliases status f =
let status =
status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
- new_aliases,res
+ let new_status = f status in
+ let new_aliases = new_status#disambiguate_db.new_aliases in
+ new_aliases,new_status
;;
let dump_aliases out msg status =
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
in
let name =
match obj with
- | NotationPt.Inductive (_,(name,_,_,_)::_)
- | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | NotationPt.Inductive (_,(name,_,_,_)::_,_)
+ | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind"
| NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
+ | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con"
+ | NotationPt.LetRec _
| NotationPt.Inductive _ -> assert false
in
NUri.uri_of_string (baseuri ^ "/" ^ name)