From 3e756356161bb201ba51d681e9052bc505130a4b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Oct 2024 16:13:12 +0200 Subject: [PATCH] fix compilation coq_elpi_builtins.ml --- 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 30cbebf50..1027e3df4 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -579,7 +579,7 @@ let preprocess_clause ~depth clause = E.mkLam (subst ~depth:(depth+1) m x) | E.Builtin(c,xs) -> E.mkBuiltin c (List.map (subst ~depth m) xs) - | E.UnifVar _ -> CErrors.error Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify them out using 'pi'.") + | E.UnifVar _ -> CErrors.user_err Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify them out using 'pi'.") | E.Const _ | E.Nil | E.CData _ -> t in let clause =