Commit 802a0d87 authored by Samuel Hym's avatar Samuel Hym
Browse files

Error out properly when an argument cannot be located

parent 272b7b36
Pipeline #16942 passed with stages
in 7 minutes and 59 seconds
......@@ -167,9 +167,10 @@ Elpi Accumulate lp:{{
type argumentSeparator term.
pred resolveArg i:argument, o:term.
resolveArg (trm T) T.
resolveArg (trm T) T :- !.
resolveArg (str "__") argumentSeparator :- !.
resolveArg (str Name) T :- coq.locate-all Name (Loc :: _), resolveLoc Loc T.
resolveArg (str Name) T :- coq.locate-all Name (Loc :: _), resolveLoc Loc T, !.
resolveArg (str Name) _ :- coq.error "Cannot locate name" Name.
% Split the argument list at "__"
pred splitArgs i:list argument, o:list argument, o:list argument.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment