From 1a7d47ba610dc1b9775ba1b838d5b2238ce7df26 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 2 Feb 2016 16:32:37 +0100
Subject: fix compilation on 8.4

---
 mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
index 3686b0a..08f1780 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
@@ -621,8 +621,8 @@ let match_upats_HO upats env sigma0 ise c =
         raise (FoundUnif (ungen_upat lhs pt' u))
       with FoundUnif _ as sigma_u -> raise sigma_u 
       | NoProgress -> it_did_match := true
-      | Pretype_errors.PretypeError
-         (_,_,Pretype_errors.UnsatisfiableConstraints _) ->
+      | Typeclasses_errors.TypeClassError
+        (_,Typeclasses_errors.UnsatisfiableConstraints _) ->
           failed_because_of_TC:=true
       | e when Errors.noncritical e -> () in
     List.iter one_match fpats
-- 
cgit v1.2.3