From d8d3e9cea631d253a30dc42760d7bdde72e01c60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 1 Jun 2018 17:09:22 +0200
Subject: Use projection indices in native compilation rather than constant
 names.

---
 kernel/declarations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 913c13173..7bd70c050 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -52,7 +52,7 @@ type inline = int option
 type projection_body = {
   proj_ind : MutInd.t;
   proj_npars : int;
-  proj_arg : int;
+  proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
   proj_eta : constr * types; (* Eta-expanded term and type *)
   proj_body : constr; (* For compatibility with VMs only, the match version *)
-- 
cgit v1.2.3