API: documenting context_chop and removing a duplicate.

3 files changed, 10 insertions, 14 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)
diff --git a/engine/termops.mli b/engine/termops.mli
index 87f74f7435..6083f1ab59 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 *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8ea9a5f66a..3f21842e39 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -277,24 +277,13 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   in
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
 
-
-(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
-   variables *)
-let context_chop k ctx =
-  let rec chop_aux acc = function
-    | (0, l2) -> (List.rev acc, l2)
-    | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
-    | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
-    | (_, []) -> failwith "context_chop"
-  in chop_aux [] (k,ctx)
-
 (* Main function *)
 let mis_make_indrec env sigma listdepkind mib u =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let evdref = ref sigma in
   let lnonparrec,lnamesparrec =
-    context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in
+    Termops.context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in
   let nrec = List.length listdepkind in
   let depPvec =
     Array.make mib.mind_ntypes (None : (bool * constr) option) in