From 2b09b02c136d3d68fa19e4493d5b5ad28c4f16db Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Feb 2013 18:51:57 +0000 Subject: Names: Modularize constant and mutual_inductive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/table.ml | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index aabbdc7a4..17303d80c 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -165,29 +165,27 @@ let record_fields_of_type = function (*s Recursors table. *) (* NB: here we can use the equivalence between canonical - and user constant names : Cset is fine, no need for [Cset_env] *) + and user constant names. *) -let recursors = ref Cset.empty -let init_recursors () = recursors := Cset.empty +let recursors = ref KNset.empty +let init_recursors () = recursors := KNset.empty -let add_recursors env kn = - let mk_con id = - make_con_equiv - (modpath (user_mind kn)) - (modpath (canonical_mind kn)) - DirPath.empty (Label.of_id id) +let add_recursors env ind = + let kn = MutInd.canonical ind in + let mk_kn id = + KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id) in - let mib = Environ.lookup_mind kn env in + let mib = Environ.lookup_mind ind env in Array.iter (fun mip -> let id = mip.mind_typename in - let c_rec = mk_con (Nameops.add_suffix id "_rec") - and c_rect = mk_con (Nameops.add_suffix id "_rect") in - recursors := Cset.add c_rec (Cset.add c_rect !recursors)) + let kn_rec = mk_kn (Nameops.add_suffix id "_rec") + and kn_rect = mk_kn (Nameops.add_suffix id "_rect") in + recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) mib.mind_packets let is_recursor = function - | ConstRef kn -> Cset.mem kn !recursors + | ConstRef c -> KNset.mem (Constant.canonical c) !recursors | _ -> false (*s Record tables. *) -- cgit v1.2.3