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)
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
let instantiate32 idrefs env symbol args =
- let rec instantiate_arg = function
+ let instantiate_arg = function
| Ast.IdentArg (n, name) ->
let t =
try List.assoc name env
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
| NCic.Lambda (n,s,t) ->
idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)),
k ~context:((n,NCic.Decl s)::context) t))
- | NCic.LetIn (n,s,ty,NCic.Rel 1) ->
+ | NCic.LetIn (_n,s,ty,NCic.Rel 1) ->
idref (Ast.Cast (k ~context ty, k ~context s))
| NCic.LetIn (n,s,ty,t) ->
idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context
in
let rec eat_branch n ctx ty pat =
match (ty, pat) with
- | NCic.Prod (name, s, t), _ when n > 0 ->
+ | NCic.Prod (_name, _s, t), _ when n > 0 ->
eat_branch (pred n) ctx t pat
| NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
) context ([],[]))
;;
-let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
- let module K = Content in
+let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) =
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
res
;;
-let build_def_item seed context metasenv id n t ty =
+let build_def_item seed _context _metasenv id n t ty =
let module K = Content in
(*
try
K.inductive_constructors = build_constructors seed cl
}
in
-let build_fixpoint b seed =
+let build_fixpoint _b seed =
fun (_,n,_,ty,t) ->
let t = nast_of_cic ~context:[] t in
let ty = nast_of_cic ~context:[] ty in
n, is_ind, ty, List.map (build_constractor lno context) cl
in
match kind with
- | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+ | NCic.Constant (_, n, xbo, ty, attrs) ->
let ty = nast_of_cic ~context:[] ty in
let xbo = match xbo with
| Some bo -> Some (nast_of_cic ~context:[] bo)
| None -> None
in
- N.Theorem (flavour, n, ty, xbo, pragma)
- | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->
+ N.Theorem (n, ty, xbo, attrs)
+ | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) ->
let captures, context = build_captures lno itl in
- N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
+ N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src)
| _ -> assert false (* NCic.Fixpoint (is_rec, ifl, _) -> *)
let nmap_obj status = with_idrefs nmap_obj0 status