type cic_id = string
+(*
type term_info =
{ sort: (cic_id, Ast.sort_kind) Hashtbl.t;
uri: (cic_id, NReference.reference) Hashtbl.t;
}
+*)
module IntMap = Map.Make(struct type t = int let compare = compare end);;
module StringMap = Map.Make(String);;
method interp_db = match interp_db with None -> assert false | Some x -> x
method set_interp_db v = {< interp_db = Some v >}
method set_interp_status
- : 'status. #g_status as 'status -> 'self
+ : 'status. (#g_status as 'status) -> 'self
= fun o -> {< interp_db = Some o#interp_db >}#set_coercion_status o
initializer
interp_db <- Some (initial_db self)
dsc, args, appl_pattern
) (StringMap.find symbol status#interp_db.interpretations)
in
- if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+ if sorted then HExtlib.list_uniq (List.sort Stdlib.compare raw)
else raw
with Not_found -> raise Interpretation_not_found
;;
let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) =
- let module K = Content in
let nast_of_cic =
nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
let context' = nmap_context0 status ~idref ~metasenv ~subst context in