| Symbol of string * int (* literal, instance num *)
| Num of int (* instance num *)
-exception Invalid_choice of string Lazy.t
+exception Invalid_choice of (Stdpp.location * string) Lazy.t
module OrderedDomain =
struct
Symbol (sym,n) ->
(try find k env
with Not_found -> find (Symbol (sym,0)) env)
+ | Num n ->
+ (try find k env
+ with Not_found -> find (Num 0) env)
| _ -> find k env
let cons k v env =
end
-type codomain_item =
+type 'term codomain_item =
string * (* description *)
- (environment -> string -> Cic.term list -> Cic.term)
+ ('term environment -> string -> 'term list -> 'term)
(* environment, literal number, arguments as needed *)
-and environment = codomain_item Environment.t
+and 'term environment = 'term codomain_item Environment.t
-type multiple_environment = codomain_item list Environment.t
+type 'term multiple_environment = 'term codomain_item list Environment.t
(** adds a (name,uri) list l to a disambiguation environment e **)
UriManager.uri list
val interactive_interpretation_choice:
string -> int ->
- (Token.flocation list * string * string) list list -> int list
+ (Stdpp.location list * string * string) list list -> int list
val input_or_locate_uri:
title:string -> ?id:string -> unit -> UriManager.uri option
end