API: documenting context_chop and removing a duplicate.

1 files changed, 2 insertions, 2 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index db0f1e4db5..c10c55220b 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)