From 56dc4da6ddafe885f6be0dcb300a6449541eab35 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 9 Sep 2012 20:45:06 +0000
Subject: Fixed bug #2895

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15785 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ec4ce59f8e..a593459384 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -255,7 +255,9 @@ and check_same_fix_binder bl1 bl2 =
           check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
       | _ -> failwith "not same binder") bl1 bl2
 
-let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false
+let is_same_type c d =
+  try let () = check_same_type c d in true
+  with Failure _ | Invalid_argument _ -> false
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
-- 
cgit v1.2.3