diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-15 14:03:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-15 14:34:07 +0100 |
| commit | a582737fc27da2c03c8c57c773fc4854c1e88d7a (patch) | |
| tree | 98436d432d725a556d630f07ee36bec41e0ab5e6 /engine/termops.mli | |
| parent | 003fe3d5e60b8d89b28e718e3d048818caceb56a (diff) | |
API: documenting context_chop and removing a duplicate.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 87f74f743..6083f1ab5 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -202,7 +202,14 @@ val ids_of_named_context : named_context -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context +(* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has + [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, + starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) val context_chop : int -> rel_context -> rel_context * rel_context + +(* [env_rel_context_chop n env] extracts out the [n] top declarations + of the rel_context part of [env], counting both local definitions and + hypotheses *) val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) |