From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 plugins/extraction/extraction.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'plugins/extraction/extraction.ml')

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;
-- 
cgit v1.2.3