Fix index bug in computing implicit signature of abbrev. in pattern printing.

1 files changed, 1 insertions, 1 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 008e84cd9c..b05ca8e5a6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -537,7 +537,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
-          match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+          match drop_implicits_in_patt gr nb_to_drop l2 with
             |Some true_args -> true_args
             |None -> raise No_match
       in