diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 2e5522b83..e3e34616b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -502,16 +502,16 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in - try match kind_of_term f with - | Prod _ -> na Prod_cs - | Sort s -> na (Sort_cs (family_of_sort s)) - | Const (c',_) when Constant.equal c' pc -> - begin match kind_of_term u.up_f with + let nargs_of_proj t = match kind_of_term t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be the number of arguments including the projected *) - | _ -> assert false - end + | _ -> assert false in + try match kind_of_term f with + | Prod _ -> na Prod_cs + | Sort s -> na (Sort_cs (family_of_sort s)) + | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) | _ -> -1 with Not_found -> -1 |