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.
---
 engine/eConstr.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 005ef16351..3dc1933a14 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -565,9 +565,8 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   | App (f, args), Proj (p, c) -> 
       (match kind_upto sigma f with
       | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
-          let pb = Environ.lookup_projection p env in
-          let npars = pb.Declarations.proj_npars in
-	  if Array.length args == npars + 1 then
+          let npars = Projection.npars p in
+          if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
 	  else false
       | _ -> false)
-- 
cgit v1.2.3