diff options
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2match.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml index 22f65507c1..86c7b0e3be 100644 --- a/user-contrib/Ltac2/tac2match.ml +++ b/user-contrib/Ltac2/tac2match.ml @@ -131,7 +131,9 @@ module PatternMatching (E:StaticEnvironment) = struct { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx } (** Failure of the pattern-matching monad: no success. *) - let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error } + let fail (type a) : a m = { stream = fun _ _ -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info matching_error } let run (m : 'a m) = let ctx = { @@ -150,7 +152,11 @@ module PatternMatching (E:StaticEnvironment) = struct let put_subst subst : unit m = let s = { subst } in - { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } + { stream = fun k ctx -> match merge s ctx with + | None -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info matching_error + | Some s -> k () s } (** {6 Pattern-matching} *) |