diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-09 20:45:06 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-09 20:45:06 +0000 |
| commit | 56dc4da6ddafe885f6be0dcb300a6449541eab35 (patch) | |
| tree | 91b0a98f39158b5772ebd4263c8ae67ab36a729c | |
| parent | b373c5b329230e517d0c5c92379e09b5e4566f9c (diff) | |
Fixed bug #2895
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15785 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ec4ce59f8..a59345938 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 *) |