From bba4a5f3d6a2a9ae1f95e92ed5a48935a052c418 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Mon, 25 Mar 2013 00:26:56 +0000
Subject:  Comments in mli

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

(limited to 'pretyping')

diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 3e0f0e0eb9..97ac881839 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -45,7 +45,11 @@ val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
-(** builds argument lists matching a block of binders or a context *)
+(** Functions that build argument lists matching a block of binders or a context.
+    [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
+    [extended_rel_vect n ctx] extends the [ctx] context of length [m]
+    with [n] elements.
+*)
 val rel_vect : int -> int -> constr array
 val rel_list : int -> int -> constr list
 val extended_rel_list : int -> rel_context -> constr list
-- 
cgit v1.2.3