*)
exception Eof;;
+exception LexerFailure of string;;
type uri =
ConUri of UriManager.uri
| IndConUri of UriManager.uri * int * int
;;
-let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
+type interpretation_domain_item =
+ Id of string
+ | Symbol of string * (string * (interpretation -> Cic.term)) list
+and interpretation_codomain_item =
+ Uri of uri
+ | Implicit
+ | Term of (interpretation -> Cic.term)
+and interpretation =
+ interpretation_domain_item -> interpretation_codomain_item option
+;;
+
let binders = ref ([] : (Cic.name option) list);;
let metasenv = ref ([] : Cic.metasenv);;
-let locate_object = ref ((fun _ -> None):string->uri option);;
-
-let set_locate_object f =
- locate_object := f