Answering comments.

Author: herbelin

kernel/inductive.ml

@@ -1118,11 +1118,10 @@ let filter_stack_domain env nr p stack =
   in
   filter_stack env ar stack
 
-let merge_filter l l' =
-  let n = List.length l in
-  let n' = List.length l' in
-  if n < n' then List.map2 (&&) l (List.firstn n l')
-  else List.map2 (&&) (List.firstn n' l) l'
+let rec merge_filter l l' =
+  match l, l' with
+  | [], _ | _, [] -> []
+  | a::l, a'::l' -> (a && a') :: merge_filter l l'
 
 let find_uniform_parameters recindx nargs bodies =
   let nbodies = Array.length bodies in
@@ -1148,6 +1147,12 @@ let find_uniform_parameters recindx nargs bodies =
   in
   Array.fold_left_i (fun i -> aux i 0) argsign bodies
 
+(** Given a fixpoint [fix f x y z n {struct n} := phi(f x u z t, ..., f x u' z t')]
+    with [y] not uniform we build in context [x:A, y:B(x), z:C(x,y)] a term
+    [fix f y n := phi(f u t, ..., f u' t')], say [psi], of some type
+    [forall (y:B(x)) (n:I(x,y,z)), T(x,y,z,n)], so that
+    [fun x y z => psi y] is of same type as the original term *)
+
 let drop_uniform_parameters argsign bodies =
   let nbodies = Array.length bodies in
   let nargs = List.length argsign in