diff --git a/elpi/elpi-quoted_syntax.elpi b/elpi/elpi-quoted_syntax.elpi
deleted file mode 100644
index e0fb35030..000000000
--- a/elpi/elpi-quoted_syntax.elpi
+++ /dev/null
@@ -1,26 +0,0 @@
-/* elpi: embedded lambda prolog interpreter                                  */
-/* license: GNU Lesser General Public License Version 2.1 or later           */
-/* ------------------------------------------------------------------------- */
-
-% HOAS for elpi programs
-
-kind term type.
-
-type app list term -> term.
-type lam (term -> term) -> term.
-type const string -> term.
-
-type cdata ctype "cdata" -> term. % int, string, float.. see also $is_cdata
-
-type arg (term -> term) -> term.  % only to bind the args of a clause
-
-kind clause type.
-type clause (ctype "Loc.t") -> list string -> term -> clause.
-
-% a program is then a list of clause while
-% the query is just one item of the same kind.
-
-% see elpi-checker.elpi for an example
-
-% vim: set ft=lprolog:
-
diff --git a/elpi/elpi2html.elpi b/elpi/elpi2html.elpi
deleted file mode 100644
index 3b40275bc..000000000
--- a/elpi/elpi2html.elpi
+++ /dev/null
@@ -1,404 +0,0 @@
-/* elpi: embedded lambda prolog interpreter                                  */
-/* license: GNU Lesser General Public License Version 2.1 or later           */
-/* ------------------------------------------------------------------------- */
-
-accumulate elpi_elpi/elpi-quoted_syntax.
-
-shorten std.{spy, rev, exists}.
-
-pred iter i:(A -> prop), o:list A.
-iter _ [].
-iter P [X|XS] :- P X, iter P XS.
-
-pred iter-sep i:list string, i:string, i:(list string -> A -> list string -> prop), i:list A, i:list string.
-iter-sep _ _ _ [] _.
-iter-sep _ S P [X] A :- !, P [] X A.
-iter-sep B S P [X|XS] A :- P B X [], write S, iter-sep [] S P XS A.
-
-pred iter-sep2 i:list string, i:string, i:string, i:(list string -> A -> list string -> prop), i:list A, i:list string.
-iter-sep2 _ _ _  _ [] _.
-iter-sep2 _ S _  P [X] A :- !, P [] X A.
-iter-sep2 B S S1 P [X|XS] A :- P B X [S1], write S, iter-sep2 [] S S1 P XS A.
-
-pred monad i:list (S -> S -> prop), i:S, o:S.
-monad [] X X.
-monad [P|PS] X R :- P X X1, monad PS X1 R.
-
-pred len i:list A, o:int.
-len uvar 0.
-len [] 0.
-len [_|XS] N :- len XS M, N is M + 1.
-
-pred write-to o:ctype "out_stream".
-pred write i:string.
-write S :- write-to OC, output OC S.
-
-pred sanitize i:string, o:string.
-sanitize X Y :-
-  monad [
-    rex_replace "&" "&",
-    rex_replace "<" "&lt;",
-    rex_replace ">" "&gt;",
-    rex_replace "\"" "&quot;",
-    rex_replace "'" "&apos;" ]
-  X Y.
-
-pred mk-name i:string, i:A, o:string.
-mk-name S1 I Y :-
-  Y is "<span class='name' varname='" ^
-       {term_to_string I} ^
-       "'>" ^ S1 ^ "</span>".
-
-pred cur-int o:int.
-pred incr-int i:prop.
-incr-int P :- cur-int J, I is J + 1, (cur-int I :- !) => P.
-
-pred var-to-string i:A, i:B, o:string.
-var-to-string X I Y :-
-  cur-int J, S1 is "x<sub>" ^ {term_to_string J} ^ "</sub>",
-  mk-name S1 I Y.
-pred uvar-to-string i:A, i:B, o:string.
-uvar-to-string X I Y :-
-  cur-int J, S1 is "X<sub>" ^ {term_to_string J} ^ "</sub>",
-  mk-name S1 I Y.
-pred name-to-string i:string, i:B, o:string.
-name-to-string X0 I Y :-
-  if (rex_match "^_" X0) (X = "_") (X = X0),
-  rex_replace "^\\([A-Za-z]+\\)_?\\([0-9]+\\)_?$" "\\1<sub>\\2</sub>" X S1,
-  mk-name S1 I Y.
-
-pred concat i:list string, o:string.
-concat [] "".
-concat [X|XS] S :- concat XS Res, S is X ^ Res.
-
-pred par? i:int, i:int, i:list string, i:list string, o:list string, o:list string.
-par? CL PL Open Close Open1 Close1 :-
-  if (CL =< PL)
-     (Open1 = Open, Close1 = Close)
-     (Open1 = ["("|Open], Close1 = [")"|Close]).
-
-kind option type -> type.
-type some A -> option A.
-type none option A.
-
-pred grab-list i:term, o:list term, o:option term.
-grab-list (const "[]") [] none.
-grab-list (app [ const "::", X, XS]) [ X | R ] T :- grab-list XS R T.
-grab-list X [] (some X).
-
-
-pred infx i:string, o:int, o:string, o:int, o:int.
-% TODO: fix precendences
-infx "<"  60 "&nbsp;&lt;&nbsp;"      60 60.
-infx "=>" 60 "&nbsp;<b>⇒</b>&nbsp;"  59 59.
-infx "="  60 "&nbsp;=&nbsp;"           70 70.
-infx "^"  60 "&nbsp;^&nbsp;"           60 60.
-infx "is" 60 "&nbsp;<b>is</b>&nbsp;" 60 60.
-infx ";"  50 "&nbsp;;&nbsp;"         50 50.
-infx "+"  60 "&nbsp;+&nbsp;"           60 60.
-infx "*"  60 "&nbsp;*&nbsp;"           60 60.
-infx "as"  0 "&nbsp;<b>as</b>&nbsp;" 60 60.
-
-%@log (pp _ _ _ _).
-
-pred pp-compound i:prop.
-pp-compound P :- write "<div class='compound'>", P, write "</div>".
-
-%    pp Level  ParensBefore   Term    ParensAfter
-pred pp i:int, i:list string, i:term, i:list string.
-pp L B (app [ const OP, Left, Right ]) A :- infx OP LOP S PL PR, !,
-  par? L LOP B A B1 A1,
-  pp-compound (pp PL B1 Left  [S]),
-  pp-compound (pp PR [] Right A1).
-
-pp L B (app [ const ":-" , Hd , Hyps ]) A :-
-  par? L 60 B A B1 A1,
-  if (Hyps = app [ const "," , const "!" | Rest])
-     (Hyps2 = app [ const "," | Rest], NeckCut = " neckcut")
-     (Hyps2 = Hyps, NeckCut = ""),
-  write "<div class='hyps'>",
-  pp 59 B1 Hyps2 [],
-  write "</div>",
-  Concl is "<div class='concl" ^ NeckCut ^ "'><div class='compound'>",
-  write Concl,
-  pp 59 [] Hd A1,
-  write "</div></div>".
-
-pp L B (app [ const C, lam _ ] as T) A :- (C = "pi"; C = "sigma"), !,
-  par? L 60 B A B1 A1,
-  pp-quantifier-block B1 C T [] A1.
-
-pred pp-quantifier-block i:list string, i:string, i:term, i:list string, i:list string.
-pp-quantifier-block B C (app [ const C, lam F ]) Args A :- !, incr-int (
-  new_int I,
-  pi x\ if (C = "pi") (var-to-string x I X) (uvar-to-string x I X),
-        is-name x X => pp-quantifier-block B C (F x) [X|Args] A).
-pp-quantifier-block B C T Args A :-
-  write "<div class='compound'>",
-  write-math-quantifier B C,
-  iter-sep [] " " (b\ x\ a\ write x) {rev Args} [],
-  write ". </div><div class='compound'>",
-  pp 60 [] T A,
-  write "</div>".
-
-pred write-math-quantifier i:list string, i:string.
-write-math-quantifier B "pi"    :- write {concat B}, write "<b>∀</b>".
-write-math-quantifier B "sigma" :- write {concat B}, write "<b>∃</b>".
-
-pp L B (app [ const "," | Args ]) A :-
-  par? L 60 B A B1 A1,
-  write "<div class='hyp compound' level='60'>",
-  iter-sep2 B1 "</div><div class='hyp compound'>" "," (pp 59) Args A1,
-  write "</div>".
-
-pp L B (app [ const "::", HD, TL ]) A :-
-  par? L 99 B A B1 A1,
-  grab-list TL Args Last,
-  write "<div class='compound' level='99'><b>[</b><div class='compound'>",
-  iter-sep2 B1 "</div><div class='compound'> " "<b>,</b>" (pp 61) [HD|Args] [],
-  if (Last = some X) (write " <b>|</b> ", pp 0 [] X []) (true),
-  write "</div><b>]</b></div>", write {concat A1}.
-
-pp L B (app Args) A :-
-  par? L 65 B A B1 A1,
-  iter-sep B1 " " (pp 66) Args A1.
-
-pp L B (lam F) A :- incr-int (
-  par? L 70 B A B1 A1,
-  new_int I,
-  pi x\
-    write "<div class='compound' level='70'><b>λ</b>",
-    write {concat B1},
-    var-to-string x I X, write X,
-    write ". </div><div class='compound'>",
-    is-name x X => pp 10 [] (F x) A1,
-    write "</div>").
-
-pp _ B (const "!") A :- !,
-  write {concat B},
-  write "<span class='cut'>!</span>",
-  write {concat A}.
-
-pp _ B (const "discard") A :-
-  write {concat B},
-  write "_",
-  write {concat A}.
-
-pp _ B (const X) A :-
-  write {concat B},
-  write {sanitize X},
-  write {concat A}.
-
-pp _ B X A :- is-name X Y, !,
-  write {concat B}, write Y, write {concat A}.
-
-pp _ B (cdata S) A :- is_cdata S _, !,
-  term_to_string S Y,
-  write {concat B},
-  write Y,
-  write {concat A}.
-
-pp _ B X A :- write "ERROR".
-
-pred hd-symbol i:term.
-hd-symbol (app [ const ":-", H, _ ]) :- hd-symbol H.
-hd-symbol (app [ const S | _ ]) :- write S.
-hd-symbol (const S) :- write S.
-
-type is-name term -> string -> prop.
-pred write-clause i:clause.
-write-clause (clause Loc [] (arg Body)) :-
-  new_int I,
-  (pi x\ X is "X" ^ {term_to_string I}),
-  name-to-string X I A1,
-  pi x\ is-name x A1 => write-clause (clause Loc [] (Body x)).
-write-clause (clause Loc [A|Args] (arg Body)) :-
-  new_int I, name-to-string A I A1,
-  pi x\ is-name x A1 => write-clause (clause Loc Args (Body x)).
-write-clause (clause Loc [] C) :- !,
-  write "<div class='clause' predicate='", hd-symbol C, write "'>",
-  write "<div class='loc'>",
-    term_to_string Loc LocS, write LocS,
-  write "</div>",
-  cur-int 0 =>
-  if (C = app [const ":-"|_])
-     (pp 0 [] C [])
-     (write "<div class='hyps'><div class='hyp'></div></div><div class='concl'>",
-       pp 0 [] C [],
-      write "</div>"),
-  write "</div>\n".
-
-pred write-preamble i:string.
-write-preamble F :-
-  write "<!DOCTYPE html>
-         <html>
-         <head>
-           <meta charset='UTF-8'>
-           <title>",
-  write F,
-  write "  </title>
-           <link rel='stylesheet'
-             href='https://code.jquery.com/ui/1.12.1/themes/base/jquery-ui.css'>
-           <script src='https://code.jquery.com/jquery-1.12.4.js'></script>
-           <script src='https://code.jquery.com/ui/1.12.1/jquery-ui.js'></script>
-           <script>
-           $( function() {
-               $( '.clause' ).each(function() { $( this ).resizable({
-                    start: function( event, ui ) {
-                      //$( ui.element ).css('max-width','100%');
-                    }
-              }); });
-           } );
-// Highlight the box around compound elements
-$( function() {
-  $('.compound').each(function() {
-    $( this ).mouseover(function (e) {
-      e.stopPropagation();
-      $( this ).addClass('hover')
-    }).mouseout(function (e) {
-      $( this ).removeClass('hover')
-    })
-  });
-});
-
-// Highlight all variables named the same
-$( function() {
-  $('.name').each(function() {
-    $( this ).mouseover(function (e) {
-      $( 'span[varname=' + $( this ).attr('varname') + ']' ).addClass('samevar')
-    }).mouseout(function (e) {
-      $( 'span[varname=' + $( this ).attr('varname') + ']' ).removeClass('samevar')
-    })
-  });
-});
-
-           </script>
-           <style>
-           .clause{
-             display: inline-block;
-             padding: 1em;
-             margin: 5px;
-             border: 2px solid black;
-             width: 30em;
-             cursor: default;
-           }
-           .hidden {
-             display: none;
-           }
-           .hyps {
-             display: block;
-           }
-           .hyp {
-             display: inline-block;
-             margin-right: 1em;
-             margin-top: 0.5em;
-           }
-           .compound {
-             display: inline-block;
-             vertical-align: top;
-             padding-left: 1em;
-             text-indent: -1em;
-             border: 1px solid transparent;
-           }
-/*
-           .hover:after {
-             content: attr(level);
-             position: fixed;
-             right: 0;
-             top: 0;
-           }
-*/
-           .hover {
-             border: 1px dotted grey;
-             transition: border 0.5s;
-           }
-           .samevar {
-             color: #22aD22;
-             transition: color 0.5s;
-             border: 1px dotted #22aD22;
-             transition: border 0.5s;
-           }
-           .name {
-             border: 1px solid transparent;
-           }
-           .concl {
-             display: block;
-             border-top: 1px solid black;
-           }
-           .neckcut {
-             border-top: 2px solid red;
-           }
-           .cut {
-             color: red;
-           }
-           .loc {
-             display: block;
-             background-color: #ecebeb;
-           }
-         </style>
-         </head>
-         <body>
-         <h1>",
-  write F,
-  write "</h1>
-         <script type='text/javascript'>
-         function filter() {
-           var f = document.getElementById('filter').value;
-           var cl = document.getElementsByClassName('clause');
-           for (i=0;i < cl.length; i++) {
-             if (cl[i].getAttribute('predicate') === f || f === '' ) {
-               cl[i].classList.remove('hidden')
-             } else {
-               cl[i].classList.add('hidden')
-             }
-           }
-         }
-         </script>
-         <p>Filter predicate: <input onkeyup='filter();' type='text' id='filter' name='filter'></p>
-".
-
-pred write-end.
-write-end :-
-  write "</body></html>".
-
-pred filter-out i:list A, i:(A -> prop), o:list A.
-filter-out [] _ [].
-filter-out [X|XS] P R :-
-  if (P X) (R = [X | RS]) (R = RS),
-  filter-out XS P RS.
-
-pred write-html i:list clause, i:string, i:(string -> prop).
-write-html P F R :-
-  filter-out P (c\
-    sigma Loc LocS \ c = (clause Loc _ _),
-    term_to_string Loc LocS, not(R LocS)) PF,
-  write-preamble F,
-  iter write-clause PF,
-  write-end.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-pred main-quoted i:list clause, i:string, i:list string.
-
-% entry point from a software having the program in compiled form
-main-quoted P OUT FILTERS :-
-  open_out OUT OC,
-  R = (x\exists FILTERS (y\ rex_match y x)),
-  write-to OC => write-html P OUT R,
-  close_out OC.
-
-pred main i:list string.
-type main prop.
-
-% entry point from the command line
-main [IN,OUT|FILTERS] :- !,
-  quote_syntax IN "main" P _,
-  main-quoted P OUT FILTERS.
-
-main _ :- usage.
-main.
-
-usage :-
-  halt "usage: elpi elpi2html.elpi -exec main -- in out [filter]".
-
-% vim: set ft=lprolog:
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 7f2a8e956..a3a49e761 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -391,9 +391,11 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x)
     let raw_args = Option.default false raw_args in
     let elpi = P.ensure_initialized () in
     P.declare_program n (Program { raw_args });
-    let unit = P.unit_from_string ~elpi ~base:(EC.empty_base ~elpi) ~loc sloc s in
-    let init = EmbeddedString { (*sloc = loc; sdata = s;*) sast = unit} in
-    P.init_program n [init];
+    if P.stage = Summary.Stage.Interp then begin
+      let unit = P.unit_from_string ~elpi ~base:(EC.empty_base ~elpi) ~loc sloc s in
+      let init = EmbeddedString { sast = unit} in
+      P.init_program n [init];
+    end;
     set_current_program (snd n)
 
   let create_db ~atts ~loc n ~init:(sloc,s) =
diff --git a/tests/boom.elpi b/tests/boom.elpi
index 655730c03..33743e42a 100644
--- a/tests/boom.elpi
+++ b/tests/boom.elpi
@@ -1 +1,12 @@
-p :- X = {{ hd }}.
\ No newline at end of file
+pred locate?! i:id, i:A -> located, o:A.  % Locate or fail (rather than panic)
+  pred locate? i:id, i:A -> located, o:A.   % Can succeed more than once
+
+  locate?! Name Pat Val :-
+    std.mem! {coq.locate-all Name} (Pat Tmp),
+    ( ground_term Tmp, !, Val = Tmp
+    ; fail ).
+
+  locate? Name Pat Val :-
+    std.mem {coq.locate-all Name} (Pat Tmp),
+    ( ground_term Tmp, Val = Tmp
+    ; fail ).
\ No newline at end of file
diff --git a/tests/test_File2.v b/tests/test_File2.v
index 60bf9b809..ac2509c68 100644
--- a/tests/test_File2.v
+++ b/tests/test_File2.v
@@ -8,4 +8,8 @@ Elpi Accumulate File file1.
 Elpi Accumulate File file2.
 Elpi Accumulate lp:{{ main _ :- coq.say "hello4". }}.
 
-Elpi c.
\ No newline at end of file
+Elpi c.
+
+
+
+
diff --git a/tests/test_File3.v b/tests/test_File3.v
new file mode 100644
index 000000000..8a2b34363
--- /dev/null
+++ b/tests/test_File3.v
@@ -0,0 +1,18 @@
+From elpi Require Import elpi.
+Elpi File myfile lp:{{
+  pred locate?! i:id, i:A -> located, o:A.  % Locate or fail (rather than panic)
+  locate?! Name Pat Val :-
+    std.mem! {coq.locate-all Name} (Pat Tmp),
+    ( ground_term Tmp, !, Val = Tmp
+    ; fail ).
+}}.
+
+Elpi Command C1.
+Elpi Accumulate File myfile.
+Elpi Accumulate lp:{{  }}.
+
+Elpi Command C2.
+Elpi Accumulate File myfile.
+Elpi Accumulate lp:{{  }}. (* Error: todbl: term contains spill: coq.locate-all Name *)
+
+#[phase="interp"] Elpi Program foo lp:{{ pred p i:gref. main _ :- coq.say "hello". }}.
\ No newline at end of file