API: documenting context_chop and removing a duplicate.

2 files changed, 9 insertions, 2 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index db0f1e4db..c10c55220 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -992,8 +992,8 @@ let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
 let on_judgment_value f j = { j with uj_val = f j.uj_val }
 let on_judgment_type f j = { j with uj_type = f j.uj_type }
 
-(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
-     variables; skips let-in's *)
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
+     variables skips let-in's; let-in's in the middle are put in ctx2 *)
 let context_chop k ctx =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
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 *)