diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi
index c3dc18f8f..1c3595302 100644
--- a/elpi-builtin.elpi
+++ b/elpi-builtin.elpi
@@ -55,7 +55,7 @@ not _.
 
 % [declare_constraint C Key1 Key2...] declares C blocked
 % on Key1 Key2 ... (variables, or lists thereof).
-external type declare_constraint variadic any prop.
+external type declare_constraint any -> any -> variadic any prop.
 
 external pred print_constraints. % prints all constraints
 
@@ -1173,6 +1173,26 @@ external pred getenv i:string, o:option string.
 % [system Command RetVal] executes Command and sets RetVal to the exit code
 external pred system i:string, o:int.
 
+%  -- Unix --
+
+% gathers the standard file descriptors or a process
+kind unix.process type.
+type unix.process out_stream -> in_stream -> in_stream -> unix.process.
+
+% [unix.process.open Executable Arguments Environment P Diagnostic] OCaml's
+% Unix.open_process_args_full.
+% Note that the first argument is the executable name (as in argv[0]).
+% If Executable is omitted it defaults to the first element of
+% Arguments.
+% Environment can be left unspecified, defaults to the current process
+% environment.
+% This API only works reliably since OCaml 4.12.
+external pred unix.process.open i:string, i:list string, i:list string,
+				o:unix.process, o:diagnostic.
+
+% [unix.process.close P Diagnostic] OCaml's Unix.close_process_full
+external pred unix.process.close i:unix.process, o:diagnostic.
+
 %  -- Debugging --
 
 % [term_to_string T S] prints T to S
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 8e9c74e0a..9107bcf7b 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -2020,7 +2020,7 @@ Supported attributes:
   (fun (me, uctx, univ_binders, record_info, ind_impls) _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-indt" (fun state ->
      let sigma = get_sigma state in
      if not (is_mutual_inductive_entry_ground me sigma) then
-       err Pp.(str"coq.env.add-indt: the inductive type declaration must be ground. Did you forge to call coq.typecheck-indt-decl?");
+       err Pp.(str"coq.env.add-indt: the inductive type declaration must be ground. Did you forget to call coq.typecheck-indt-decl?");
      let primitive_expected = match record_info with Some(p, _) -> p | _ -> false in
      let (uentry, uentry', ubinders) = 
        let open Entries in