From a1e4318a8e1fc249693142ab68745562ca9f411f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 19:18:00 +0200 Subject: ssr: fix canonical strucut key comparison with primproj on --- plugins/ssrmatching/ssrmatching.ml4 | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'plugins/ssrmatching') 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 -- cgit v1.2.3