diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index efd65ade15..552a4048b1 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -312,7 +312,8 @@ let iter_constr_LR f c = match kind c with | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ + | Int _) -> () (* The comparison used to determine which subterms matches is KEYED *) (* CONVERSION. This looks for convertible terms that either have the same *) |