diff options
| author | Pierre-Marie Pédrot | 2021-03-30 14:02:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-30 14:02:16 +0200 |
| commit | f0c6a1de3eef85ab0787be7e87cb8509e8df43d5 (patch) | |
| tree | 05f3cc7ece9e0a77f841b37a12db909ff6362be0 /plugins/extraction | |
| parent | 303afeab9c946bdba15e1984231ae5066bf37af6 (diff) | |
| parent | d9c80dadd353bd8b0eb90ce290048a2538f1a41a (diff) | |
Merge PR #13958: [recordops] complete API rewrite; the module is now called [structures]
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0cad192332..ca4f5429a2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -22,7 +22,6 @@ open Reductionops open Inductive open Termops open Inductiveops -open Recordops open Namegen open Miniml open Table @@ -531,7 +530,7 @@ and extract_really_ind env kn mib = let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in - List.iter (Option.iter check_proj) (lookup_projections ip) + List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip) with Not_found -> () end; Record field_glob @@ -1129,7 +1128,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_typ (get_body c) | Some p -> let body = fake_match_projection env p in @@ -1142,7 +1141,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_def (get_body c) | Some p -> let body = fake_match_projection env p in |