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

1 files changed, 3 insertions, 0 deletions

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 *)