From 55a85358c4ecd29b415a542d2606854a63cc10a3 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 19 May 2011 17:08:53 +0000 Subject: Extraction: avoid lots of late mind_of_kn git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14142 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/ocaml.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/extraction/ocaml.ml') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 5bacddb97..902e8bbb3 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -439,7 +439,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -447,7 +447,7 @@ let pp_singleton kn packet = pr_id packet.ip_consnames.(0))) let pp_record kn projs ip_equiv packet = - let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let name = pp_global Type (IndRef (kn,0)) in let projnames = List.map (pp_global Term) projs in let l = List.combine projnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in @@ -469,20 +469,20 @@ let pp_ind co kn ind = let init= ref (str "type ") in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (IndRef (mind_of_kn kn,i))) + pp_global Type (IndRef (kn,i))) ind.ind_packets in let cnames = Array.mapi (fun i p -> if p.ip_logical then [||] else - Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1))) + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) p.ip_types) ind.ind_packets in let rec pp i = if i >= Array.length ind.ind_packets then mt () else - let ip = (mind_of_kn kn,i) in + let ip = (kn,i) in let ip_equiv = ind.ind_equiv, i in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) -- cgit v1.2.3