diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-15 20:48:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-27 22:35:10 +0200 |
| commit | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (patch) | |
| tree | 78c30edd51e65c8e7014ac360c5027da77ff20b2 /plugins/funind/glob_termops.ml | |
| parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
[cleanup] Unify all calls to the error function.
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5abcb100f..0361e8cb1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - CAst.map (function + CAst.map_with_loc (fun ?loc -> function | GRef _ as x -> x | GVar id -> let new_id = @@ -172,7 +172,7 @@ let change_vars = change_vars mapping lhs, change_vars mapping rhs ) - | GRec _ -> error "Local (co)fixes are not supported" + | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported") | GSort _ as x -> x | GHole _ as x -> x | GCast(b,c) -> @@ -352,7 +352,7 @@ let rec alpha_rt excluded rt = alpha_rt excluded lhs, alpha_rt excluded rhs ) - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ | GHole _ as rt -> rt | GCast (b,c) -> @@ -408,7 +408,7 @@ let is_free_in id = | GIf(cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError(None,str "Not handled GRec")) + | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -695,7 +695,7 @@ let expand_as = | GIf(e,(na,po),br1,br2) -> GIf(expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, Miscops.map_cast_type (expand_as map) c) |