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.
---
 interp/impargs.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/impargs.ml')

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 8aa1e62504..e542b818f6 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -689,8 +689,8 @@ let check_rigidity isrigid =
     user_err  (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
 let projection_implicits env p impls = 
-  let pb = Environ.lookup_projection p env in
-    CList.skipn_at_least pb.Declarations.proj_npars impls
+  let npars = Projection.npars p in
+  CList.skipn_at_least npars impls
 
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
-- 
cgit v1.2.3