pumpkin-pi/plugin/src/lib/ornerrors.mli at master · uwplse/pumpkin-pi · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
open Environ
open Evd
open Constr

(*
 * Errors and error messages
 *)

(* --- Exceptions --- *)

exception NotEliminators
exception NotInductive
exception NotAlgebraic

(* --- Error descriptions --- *)

val err_unsupported_change : Pp.t
val err_name_inference : Pp.t
val err_new_parameter : Pp.t
val err_new_constructor : Pp.t
val err_save_ornament : Pp.t
val err_unexpected_change : String.t -> Pp.t
val err_type : env -> evar_map -> Pretype_errors.pretype_error -> Pp.t
val err_opaque_not_constant : Libnames.qualid -> Pp.t
val err_ambiguous_swap :
  env -> string -> ((pconstructor * pconstructor) list) list -> evar_map -> Pp.t

(* --- Possible workaround suggestions --- *)

val try_name : Pp.t
val try_opaque : Pp.t
val try_not_opaque : Pp.t
val try_preprocess : Pp.t
val try_check_typos : Pp.t
val try_fully_qualify : Pp.t
val try_supported : Pp.t
val try_provide : Pp.t

(* --- Reasons to cut an issue --- *)

val cool_feature : Pp.t
val problematic : Pp.t
val mistake : Pp.t

(* --- Putting these together --- *)

(*
 * Our own user_err function to make it easier to present nice information
 * to the user
 *)
val user_err :
  String.t -> (* where you're calling it from *)
  Pp.t -> (* error description *)
  Pp.t list -> (* workaround suggestions *)
  Pp.t list -> (* reasons to cut an issue *)
  'a