Merge PR #7908: Projections use index representation

3 files changed, 15 insertions, 15 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4a691e442c..ce620d5312 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -460,7 +460,7 @@ let rec canonize_name sigma c =
           mkApp (func ct,Array.Smart.map func l)
       | Proj(p,c) ->
 	let p' = Projection.map (fun kn ->
-          Constant.make1 (Constant.canonical kn)) p in 
+          MutInd.make1 (MutInd.canonical kn)) p in
 	  (mkProj (p', func c))
       | _ -> c
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 04ff11fc49..2eaa6146e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -84,8 +84,8 @@ let rec decompose_term env sigma t=
 	let canon_const = Constant.make1 (Constant.canonical c) in 
 	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
-	let canon_const kn = Constant.make1 (Constant.canonical kn) in 
-	let p' = Projection.map canon_const p in
+        let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
+        let p' = Projection.map canon_mind p in
 	let c = Retyping.expand_projection env sigma p' c [] in
 	decompose_term env sigma c
     | _ ->
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;