diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 00:37:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 00:37:27 +0100 |
| commit | fc302b7a32387005f2b7b090d90d8cc3e4a800cd (patch) | |
| tree | 97fdd37058159ffbb0cd0c6a2f743a1f8ea13e2e /pretyping/constr_matching.ml | |
| parent | e914f29ff02cfc065d6b3e8f45259341198fef5d (diff) | |
Fixing bug #3900.
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index a6e2bc19d..cf6ac619d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -441,7 +441,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = try let term = Retyping.expand_projection env sigma p c' [] in aux env term mk_ctx next - with Retyping.RetypeError _ -> raise PatternMatchingFailure + with Retyping.RetypeError _ -> next () else try_aux [env] [c'] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next |