diff options
| author | Gaëtan Gilbert | 2018-06-23 15:38:00 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:49:17 +0200 |
| commit | 0108db19c96e1b46346f032964f2cca3f8149cb3 (patch) | |
| tree | 6414910c08328fceeb45c82414bea1ee0b601c91 /plugins/extraction | |
| parent | 7817af48a554573fb649028263ecfc0fabe400d8 (diff) | |
Projections use index representation
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 71e09992cc..67c605ea1d 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1065,13 +1065,13 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Environ.is_projection kn env with - | false -> mk_typ (get_body c) - | true -> - let pb = lookup_projection (Projection.make kn false) env in - let ind = pb.Declarations.proj_ind in + (match Recordops.find_primitive_projection kn with + | None -> mk_typ (get_body c) + | Some p -> + let p = Projection.make p false in + let ind = Projection.inductive p in let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(pb.Declarations.proj_arg) in + let body = bodies.(Projection.arg p) in mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; @@ -1081,13 +1081,13 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Environ.is_projection kn env with - | false -> mk_def (get_body c) - | true -> - let pb = lookup_projection (Projection.make kn false) env in - let ind = pb.Declarations.proj_ind in + (match Recordops.find_primitive_projection kn with + | None -> mk_def (get_body c) + | Some p -> + let p = Projection.make p false in + let ind = Projection.inductive p in let bodies = Inductiveops.legacy_match_projection env ind in - let body = bodies.(pb.Declarations.proj_arg) in + let body = bodies.(Projection.arg p) in mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; |