From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 Jun 2018 16:23:29 +0200
Subject: Getting rid of the const_proj field in the kernel.

This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
---
 plugins/extraction/extraction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5aee70194d..b1ee215367 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1065,7 +1065,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
@@ -1078,7 +1078,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-- 
cgit v1.2.3


From e43710b391c278ac7fcb808ec28d720b4317660c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Jun 2018 15:26:20 +0200
Subject: Remove the proj_body field from the kernel.

This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.

Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.

Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
---
 plugins/extraction/extraction.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b1ee215367..3a61c7747d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,7 +1069,11 @@ let extract_constant env kn cb =
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_typ (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_typ (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_typ (get_opaque env c)
@@ -1082,7 +1086,11 @@ let extract_constant env kn cb =
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_def (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_def (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_def (get_opaque env c)
-- 
cgit v1.2.3