diff options
| author | Pierre-Marie Pédrot | 2017-02-01 10:52:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-01 10:54:53 +0100 |
| commit | c17c3faee20251cd5c7168246e9ffcd12d557f85 (patch) | |
| tree | 02635866b73d7595fad009cc17535a6bbf06c2fc /ltac | |
| parent | f86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff) | |
| parent | 568b38e1d599f8bac5adf140f5a114f2871bc436 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index ddeab733e5..32bcdfb6a4 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -948,7 +948,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> - raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern")) + user_err ~loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) | Some (ArgArg (loc,l)) -> let sigma,l = interp_or_and_intro_pattern ist env sigma l in sigma, Some (loc,l) |