From 4d3fd35d44844d054417294cdbb2421c8e37fb65 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Aug 2011 10:07:05 +0000
Subject: Patch to simplify is_open_canonical_projection (courtesy from
 François Garillot)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/recordops.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index ccedf1520d..0f1b9ac970 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -332,8 +332,7 @@ let lookup_canonical_conversion (proj,pat) =
 
 let is_open_canonical_projection sigma (c,args) =
   try
-    let l = Refmap.find (global_of_constr c) !object_table in
-    let n = (snd (List.hd l)).o_NPARAMS in
+    let n = find_projection_nparams (global_of_constr c) in                                                           
     try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false
   with Not_found -> false
 
-- 
cgit v1.2.3