Skip to content

Commit

Permalink
fix compilation coq_elpi_builtins.ml
Browse files Browse the repository at this point in the history
  • Loading branch information
gares authored Oct 25, 2024
1 parent 622716d commit 3e75635
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/coq_elpi_builtins.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down

0 comments on commit 3e75635

Please sign in to comment.