[errors] Introduce error registration API

Partially addresses #7560

Coq exception handling is complex, and requires quite a bit of
meta-data on exceptions, including custom printing and documentation
for each error.

We introduce an error registration API that should help with the above
problematic, by requiring new errors to be properly registered.

There are some questions:

- OCaml has support for private extensible types, however that cannot
  be used with exceptions unless we introduce a `CErrors.t` type. May
  be worth doing.

- We could make the error kinds extensible too, but I'm not sure it is
  worth the gain, and it could be used badly.

- Is the E0 variant worth it?

A new error is declared as:

```ocaml
module UE_Sig = struct
  type t = string option * Pp.t
  let print (hdr, pp) = Pp.strpp
  let doc = Pp.str "Generic User Error, to be deprecated"
  let kind = ErrorKind.Regular
end

module UserError = CoqError.Make(UE_Sig)
```

in the `.mli` file:

```ocaml
module UserError = CErrors.S with type t := string option * Pp.t
```

the `with type` constraint is needed if the user wishes to expose the
exception constructor.

Author: ejgallego

lib/cErrors.ml

@@ -30,7 +30,49 @@ let anomaly ?loc ?info ?label pp =
   let info = Option.cata (Loc.add_loc info) info loc in
   Exninfo.iraise (Anomaly (label, pp), info)
 
-exception UserError of string option * Pp.t (* User errors *)
+module ErrorKind = struct
+  type t = Anomaly | Regular
+end
+
+(* TODO: support for errors with context *)
+module type S = sig
+  type t
+  val print : t -> Pp.t
+  val doc : Pp.t
+  val kind : ErrorKind.t
+end
+
+module type E = sig
+  type t
+  type exn += E of t
+end
+
+module type S0 = sig
+  val print : Pp.t
+  val doc : Pp.t
+  val kind : ErrorKind.t
+end
+
+module type E0 = sig
+  type exn += E
+end
+
+module CoqError : sig
+  module Make (X : S) : E with type t = X.t
+  module Make0 (X : S0) : E0
+end = struct
+  module Make (X : S) = struct
+    type t = X.t
+    type exn += E of t
+    (* register printer *)
+  end
+  module Make0 (X : S0) = struct
+    type exn += E
+    (* register printer *)
+  end
+end
+
+exception UserError of string option * Pp.t
 
 let user_err ?loc ?info ?hdr strm =
   let info = Option.default Exninfo.null info in
@@ -132,7 +174,7 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e)
 (** Predefined handlers **)
 
 let _ = register_handler begin function
-  | UserError(s, pps) ->
+  | UserError (s, pps) ->
     Some (where s ++ pps)
   | _ -> None
 end

lib/cErrors.mli

@@ -16,6 +16,39 @@
 val push : exn -> Exninfo.iexn
 [@@ocaml.deprecated "please use [Exninfo.capture]"]
 
+(** {6 Error registration API} *)
+
+module ErrorKind : sig
+  type t = Anomaly | Regular
+end
+
+module type S = sig
+  type t
+  val print : t -> Pp.t
+  val doc : Pp.t
+  val kind : ErrorKind.t
+end
+
+module type E = sig
+  type t
+  type exn += E of t
+end
+
+module type S0 = sig
+  val print : Pp.t
+  val doc : Pp.t
+  val kind : ErrorKind.t
+end
+
+module type E0 = sig
+  type exn += E
+end
+
+module CoqError : sig
+  module Make0 (X : S0) : E0
+  module Make (X : S) : E with type t = X.t
+end
+
 (** {6 Generic errors.}
 
  [Anomaly] is used for system errors and [UserError] for the