diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 39ae1f41d..ad76ef9c6 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -340,8 +340,8 @@ type 'a extra_genarg_printer = let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = - match ty with - Constrexpr.CProdN(_,bll,a) -> + match snd ty with + Constrexpr.CProdN(bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in let bll = List.map (fun (x, _, y) -> x, y) bll in |