From 2f562f15a72d4a379d559ea1987e74c1c24d1391 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 10 Jun 2003 21:02:46 +0000
Subject: Ajout notation c.(f) en v8 pour les projections de Record

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

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index e5ffe4fd2..f758776de 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -37,6 +37,9 @@ val add_new_struc :
    [isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
 val find_structure : inductive -> struc_typ
 
+(* raise [Not_found] if not a projection *)
+val find_projection_nparams : global_reference -> int
+
 type obj_typ = {
   o_DEF : constr;
   o_TABS : constr list; (* dans l'ordre *)
-- 
cgit v1.2.3