diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
| commit | 4c1260299b707bd27765b0ab365092046b134a69 (patch) | |
| tree | 22331e8562bee137a5d2eea79c0d8e3d43cb94c1 /plugins/quote | |
| parent | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff) | |
| parent | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff) | |
Merge PR#512: [cleanup] Unify all calls to the error function.
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index def9ff3a7..7412de1e8 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -184,7 +184,7 @@ type inversion_scheme = { goal [gl]. This function uses the auxiliary functions [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) -let i_can't_do_that () = error "Quote: not a simple fixpoint" +let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) |