diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1918ddc0cb..1b460b060b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -984,7 +984,7 @@ let match_pat refresh lmatch hyp gl = function let lmeta = extended_matches t hyp in let lmeta = verify_metas_coherence gl lmatch lmeta in let ans = { e_ctx = Id.Map.empty; e_sub = lmeta; } in - IStream.cons ans IStream.lempty + IStream.cons ans IStream.empty with PatternMatchingFailure | Not_coherent_metas -> IStream.empty end | Subterm (b,ic,t) -> |