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 /vernac/indschemes.ml | |
| parent | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff) | |
| parent | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff) | |
Merge PR#512: [cleanup] Unify all calls to the error function.
Diffstat (limited to 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 885769143..f57b1bba0 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -418,7 +418,7 @@ let get_common_underlying_mutual_inductive = function raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) | [] -> if not (List.distinct_f Int.compare (List.map snd (List.map snd all))) - then error "A type occurs twice"; + then user_err Pp.(str "A type occurs twice"); mind, List.map_filter (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all @@ -429,7 +429,7 @@ let do_scheme l = tried to declare different schemes at once *) if not (List.is_empty ischeme) && not (List.is_empty escheme) then - error "Do not declare equality and induction scheme at the same time." + user_err Pp.(str "Do not declare equality and induction scheme at the same time.") else ( if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme else @@ -498,7 +498,7 @@ let do_combined_scheme name schemes = let refe = Ident x in let qualid = qualid_of_reference refe in try Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")) + with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in let body,typ = build_combined_scheme (Global.env ()) csts in |