diff options
| author | ppedrot | 2012-09-17 20:46:20 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-17 20:46:20 +0000 |
| commit | 7208928de37565a9e38f9540f2bfb1e7a3b877e6 (patch) | |
| tree | 7d51cd24c406d349f4b7410c81ee66c210df49cd /pretyping/termops.mli | |
| parent | a6dac9962929d724c08c9a74a8e05de06469a1a0 (diff) | |
More cleaning on Utils and CList. Some parts of the code being
peculiarly messy, I hope I did not introduce too many bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index b3e00ebaa1..b6bb438680 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -40,7 +40,10 @@ val print_env : env -> std_ppcmds val push_rel_assum : name * types -> env -> env val push_rels_assum : (name * types) list -> env -> env val push_named_rec_types : name array * types array * 'a -> env -> env + val lookup_rel_id : identifier -> 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 *) val rel_vect : int -> int -> constr array |