From 9fb6631d13a128197a6743b1a95d2e3a633df51f Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Tue, 26 Sep 2023 12:11:35 +0200 Subject: [PATCH 1/2] Fix typo --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 254bee6ab2054436eb660b4b09f356ee596e43ef Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Thu, 28 Sep 2023 18:23:24 +0200 Subject: [PATCH 2/2] Update elpi-builtin.elpi --- elpi-builtin.elpi | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) 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