Check arity match in [unmbind2] + doc fix.

bindlib.ml

@@ -745,9 +745,12 @@ let unmbind : ('a,'b) mbinder -> 'a mvar * 'b = fun b ->
   (x, msubst b (Array.map b.mb_mkfree x))
 
 (** [unmbind2 mkfree f g] is similar to [unmbind mkfree f], but it substitutes
-    both [f] and [g] using the same fresh variables. *)
+    both [f] and [g] using the same fresh variables. Note that the two binders
+    must have the same arity. *)
 let unmbind2 : ('a,'b) mbinder -> ('a,'c) mbinder -> 'a mvar * 'b * 'c =
   fun b1 b2 ->
+    if mbinder_arity b1 <> mbinder_arity b2 then
+      invalid_arg "Arity missmatch in unmbind2";
     let xs = new_mvar b1.mb_mkfree (mbinder_names b1) in
     let vs = Array.map b1.mb_mkfree xs in
     (xs, msubst b1 vs, msubst b2 vs)

bindlib.mli

@@ -120,16 +120,17 @@ val eq_binder : ('b -> 'b -> bool) -> ('a,'b) binder -> ('a,'b) binder -> bool
 val unmbind : ('a,'b) mbinder -> 'a mvar * 'b
 
 (** [unmbind2 f g] is similar to [unmbind f],  but it substitutes two multiple
-    binder [f] and [g] at once, using the same fresh variables.  This function
-    may have an unexpected results in some cases, for reasons explained in the
-    documentation of [unbind2]. *)
+    binder [f] and [g] at once, using the same fresh variables.  Note that the
+    two binders must have the same arity. This function may have an unexpected
+    results in some cases (see the documentation of [unbind2]). *)
 val unmbind2 : ('a,'b) mbinder -> ('a,'c) mbinder -> 'a mvar * 'b * 'c
 
 (** [eq_mbinder eq f g] tests the equality of the two multiple binders [f] and
     [g]. They are substituted with the same fresh variables (using [unmbind2])
     and [eq] is called on the resulting values. This function may not have the
     expected result in some cases,  for reasons explained in the documentation
-    of [eq_binder]. *)
+    of [eq_binder]. It is safe to use this function on multiple binders with a
+    different arity (they are considered different). *)
 val eq_mbinder : ('b -> 'b -> bool) -> ('a,'b) mbinder -> ('a,'b) mbinder
   -> bool