diff options
| -rw-r--r-- | contrib/ring/quote.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index c82ccecb00..9984183319 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -393,7 +393,7 @@ let quote_terms ivs lc gl= let s1 = matches rhs c in let s2 = List.map (fun (i,c_i) -> (i,aux c_i)) s1 in Term.subst_meta s2 lhs - with UserError("somatch", _) -> auxl tail + with PatternMatchingFailure -> auxl tail end | [] -> begin match ivs.variable_lhs with |