diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 98a7ad6f3..bf86d63fd 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -21,17 +21,10 @@ jobs:
           - 4.08.x
         profile:
           - dev
-        parser:
-          - menhir
         include:
           - os: ubuntu-latest
             ocaml-compiler: 5.1.x
             profile: fatalwarnings
-            parser: menhir
-          - os: ubuntu-latest
-            ocaml-compiler: 4.11.x
-            profile: dev
-            parser: menhir-camlp5
 
     runs-on: ${{ matrix.os }}
 
@@ -98,36 +91,27 @@ jobs:
         run: |
           opam install ./elpi.opam --deps-only --with-doc --with-test
 
-      - name: Install optional dependencies for menhir-camlp5 parser
-        if: matrix.parser == 'menhir-camlp5'
-        run: |
-          opam depext camlp5 || true # no depext on opam 2.1
-          sudo apt-get install libstring-shellquote-perl
-          sudo apt-get install libipc-system-simple-perl
-          opam install ./elpi-option-legacy-parser.opam
-          opam exec -- make config LEGACY_PARSER=1
-
       - name: Build elpi with dune profile ${{ matrix.profile }}
         run: |
           opam exec -- dune subst
           opam exec -- make build DUNE_OPTS='--profile ${{ matrix.profile }}'
-          opam exec -- cp _build/install/default/bin/elpi elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- cp _build/install/default/bin/elpi-trace-elaborator elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
+          opam exec -- cp _build/install/default/bin/elpi elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- cp _build/install/default/bin/elpi-trace-elaborator elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
 
       - name: Strip binary
         run: |
-          opam exec -- chmod u+w ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- chmod u+w ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- strip ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- strip ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
+          opam exec -- chmod u+w ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- chmod u+w ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- strip ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- strip ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
 
 # Artifacts 1 ################################################################
 
       - name: Save binary
         uses: actions/upload-artifact@v2
         with:
-          name: elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}
-          path: elpi*-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
+          name: elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}
+          path: elpi*-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
 
 # Test ######################################################################
 #
@@ -135,13 +119,13 @@ jobs:
 
       - name: Test elpi on Unix
         if: runner.os != 'Windows'
-        run: opam exec -- make tests RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe'
+        run: opam exec -- make tests RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe'
 
       - name: Test elpi on Windows
         if: runner.os == 'Windows'
         run: |
           opam exec -- ls -l tests/sources/*.elpi
-          opam exec -- make tests PWD=${{ env.workspace }} RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe' TIME=--time=${{ env.cygwin_root }}/bin/time.exe
+          opam exec -- make tests PWD=${{ env.workspace }} RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe' TIME=--time=${{ env.cygwin_root }}/bin/time.exe
 
 # Artifacts 2 ################################################################
 
@@ -149,7 +133,7 @@ jobs:
         uses: actions/upload-artifact@v2
         if: always()
         with:
-          name: .logs-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}
+          name: .logs-${{ matrix.ocaml-compiler }}-${{ runner.os }}
           path: _log
           retention-days: 1
 
@@ -157,7 +141,7 @@ jobs:
         uses: actions/upload-artifact@v2
         if: always()
         with:
-          name: .benchmark-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}
+          name: .benchmark-${{ matrix.ocaml-compiler }}-${{ runner.os }}
           path: data.csv
           retention-days: 1
 
diff --git a/CHANGES.md b/CHANGES.md
index f5896c259..a9f1e6ffd 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,13 +1,15 @@
-# v1.18.1 (November 2023)
+# v1.18.1 (December 2023)
 
 Requires Menhir 20211230 and OCaml 4.08 or above.
-Camlp5 8.0 or above is optional.
+
+Parser:
+  - Remove legacy parsing engine based on Camlp5
 
 API:
   - New `RawQuery.compile_ast`, lets one set up the initial state in which the
     query is run, even if the query is given as an ast.
-  - New `Utils.relocate_closed_term` to move a term from one runtime to another
-    (experimental)
+  - New `solution.relocate_assignment_to_runtime` to pass a query result
+    to another query
   - New `BuiltInPredicate.FullHO` for higher order external predicates
   - New `BuiltInPredicate.HOAdaptors` for `map` and `filter` like HO predicates
   - New `Calc.register` to register operators for `calc` (aka infix `is`)
diff --git a/Makefile b/Makefile
index 28e0ce211..5ff186187 100644
--- a/Makefile
+++ b/Makefile
@@ -40,12 +40,6 @@ DUNE_OPTS=
 build:
 	dune build $(DUNE_OPTS) @all
 
-config:
-	@(if [ -z $$LEGACY_PARSER ]; \
-	then echo '(dirs :standard \ legacy_parser)'; \
-	else echo '(dirs :standard )'; \
-	fi ) > src/dune.config
-
 install:
 	dune install $(DUNE_OPTS)
 
diff --git a/elpi-option-legacy-parser.opam b/elpi-option-legacy-parser.opam
deleted file mode 100644
index a0a295ad8..000000000
--- a/elpi-option-legacy-parser.opam
+++ /dev/null
@@ -1,19 +0,0 @@
-opam-version: "2.0"
-version: "1"
-maintainer: "Enrico Tassi <enrico.tassi@inria.fr>"
-authors: [ "Enrico Tassi" ]
-license: "LGPL-2.1-or-later"
-homepage: "https://github.com/LPCIC/elpi"
-doc: "https://LPCIC.github.io/elpi/"
-dev-repo: "git+https://github.com/LPCIC/elpi.git"
-bug-reports: "https://github.com/LPCIC/elpi/issues"
-
-depends: [
-  # "elpi" {post & >= "1.15.2"} # this is nice to have in the main repo, not here
-  "camlp5" {> "7.99"}
-  "ocaml" {< "4.14.0" }
-]
-flags: conf
-synopsis: "ELPI - option for legacy parser"
-description: """
-Enables the -legacy-parser flag, implemented on top of CamlP5"""
diff --git a/elpi.opam b/elpi.opam
index 9ee72f6cb..abd79cec9 100644
--- a/elpi.opam
+++ b/elpi.opam
@@ -9,7 +9,6 @@ bug-reports: "https://github.com/LPCIC/elpi/issues"
 
 build: [
   ["dune" "subst"] {dev}
-  [make "config" "LEGACY_PARSER=1"] {elpi-option-legacy-parser:installed}
   ["dune" "build" "-p" name "-j" jobs]
   [make "tests" "DUNE_OPTS=-p %{name}%" "SKIP=performance_HO" "SKIP+=performance_FO" "SKIP+=elpi_api_performance"] {with-test & os != "macos" & os-distribution != "alpine" & os-distribution != "freebsd"}
 ]
@@ -29,12 +28,6 @@ depends: [
   "atdts" {>= "2.10.0"}
   "odoc" {with-doc}
 ]
-depopts: [
-  "elpi-option-legacy-parser"
-]
-conflicts: [
-  "elpi-option-legacy-parser" {!= "1"}
-]
 synopsis: "ELPI - Embeddable λProlog Interpreter"
 description: """
 ELPI implements a variant of λProlog enriched with Constraint Handling Rules,
diff --git a/src/API.ml b/src/API.ml
index ece6c816b..5b0f8dfb7 100644
--- a/src/API.ml
+++ b/src/API.ml
@@ -73,9 +73,10 @@ let init ?(flags=Compiler.default_flags) ?(state=default_state_descriptor) ?(quo
         List.iteri (fun i s ->
           Printf.eprintf "%4d: %s\n" (i+1) s)
           (Re.Str.(split_delim (regexp_string "\n") text));
-        Printf.eprintf "Excerpt of %s:\n%s\n" fname
+        begin try Printf.eprintf "Excerpt of %s:\n%s\n" fname
           (String.sub text loc.Util.Loc.line_starts_at
-            Util.Loc.(loc.source_stop - loc.line_starts_at));
+            Util.Loc.(loc.source_stop - loc.line_starts_at))
+        with _ -> (* loc could be bogus *) (); end;
         Util.anomaly ~loc msg) in
   let header =
     try Compiler.header_of_ast ~flags ~parser state !quotations !hoas !calc builtins (List.concat header_src)
@@ -193,6 +194,18 @@ module Execute = struct
   type 'a outcome =
     Success of 'a Data.solution | Failure | NoMoreSteps
 
+  let rec uvar2discard ~depth t =
+    let open ED in
+    let module R = (val !r) in
+    match R.deref_head ~depth t with
+    | App(c,x,xs) -> mkApp c (uvar2discard ~depth x) (List.map (uvar2discard ~depth) xs)
+    | Cons(x,xs) -> mkCons (uvar2discard ~depth x) (uvar2discard ~depth xs)
+    | Lam x -> mkLam (uvar2discard ~depth:(depth+1) x)
+    | Builtin(c,xs) -> mkBuiltin c (List.map (uvar2discard ~depth) xs)
+    | UVar _ | AppUVar _ -> mkDiscard
+    | Arg _ | AppArg _ -> assert false
+    | Const _ | Nil | CData _ | Discard -> t
+  
   let map_outcome full_deref hmove = function
     | ED.Failure -> Failure
     | ED.NoMoreSteps -> NoMoreSteps
@@ -200,7 +213,7 @@ module Execute = struct
       Success { assignments; constraints; state; output; pp_ctx;
         relocate_assignment_to_runtime = (fun ~target ~depth s ->
           Compiler.relocate_closed_term ~from
-            (Util.StrMap.find s assignments |> full_deref ~depth:idepth) ~to_:target
+            (Util.StrMap.find s assignments |> full_deref ~depth:idepth |> uvar2discard ~depth:idepth) ~to_:target
           |> Stdlib.Result.map (hmove ?avoid:None ~from:depth ~to_:depth)
         );
         }
@@ -448,7 +461,7 @@ module BuiltInData = struct
     { Conversion.embed; readback; ty;
       pp = (fun fmt (t,d) ->
         let module R = (val !r) in let open R in
-        Pp.uppterm d [] d ED.empty_env fmt t);
+        Pp.uppterm d [] ~argsdepth:d ED.empty_env fmt t);
       pp_doc = (fun fmt () -> ()) }
    
   let map_acc f s l =
@@ -506,7 +519,7 @@ module Elpi = struct
         Format.fprintf fmt "%s" str
     | Ref ub ->
         let module R = (val !r) in let open R in
-        Pp.uppterm 0 [] 0 [||] fmt (ED.mkUVar ub 0 0)
+        Pp.uppterm 0 [] ~argsdepth:0 [||] fmt (ED.mkUVar ub 0 0)
 
   let show m = Format.asprintf "%a" pp m
 
@@ -1339,9 +1352,6 @@ module Utils = struct
       body = aux depth Util.IntMap.empty term;
     }]
 
-  let relocate_closed_term (state,t) new_state =
-    Compiler.relocate_closed_term ~from:state t ~to_:new_state
-
   let map_acc = BuiltInData.map_acc
 
   module type Show = Util.Show
@@ -1356,7 +1366,7 @@ end
 module RawPp = struct
   let term depth fmt t =
     let module R = (val !r) in let open R in
-    Pp.uppterm depth [] 0 ED.empty_env fmt t
+    Pp.uppterm depth [] ~argsdepth:0 ED.empty_env fmt t
 
   let constraints f c = 
     let module R = (val !r) in let open R in
@@ -1367,7 +1377,7 @@ module RawPp = struct
   module Debug = struct
     let term depth fmt t =
       let module R = (val !r) in let open R in
-       Pp.ppterm depth [] 0 ED.empty_env fmt t
+       Pp.ppterm depth [] ~argsdepth:0 ED.empty_env fmt t
     let show_term = ED.show_term
   end
 end
diff --git a/src/API.mli b/src/API.mli
index b98f0fc91..830cfc71e 100644
--- a/src/API.mli
+++ b/src/API.mli
@@ -161,7 +161,7 @@ module Data : sig
     state : state;
     output : 'a;
     pp_ctx : pretty_printer_context;
-    relocate_assignment_to_runtime : target:state -> depth:int -> string -> (term, string) Stdlib.Result.t
+    relocate_assignment_to_runtime : target:state -> depth:int -> string -> (term, string) Stdlib.Result.t (* uvars are turned into discard *)
   }
 
   (* Hypothetical context *)
@@ -1224,11 +1224,6 @@ module Utils : sig
     ?name:string -> ?graft:([`After | `Before] * string) ->
     depth:int -> Ast.Loc.t -> Data.term -> Ast.program
 
-  (** Hackish API. Move a term from one runtime (after execution) to another
-      one which has all the needed symbols *)
-  val relocate_closed_term :
-    State.t * Data.term -> State.t -> (Data.term,string) Stdlib.Result.t
-
   (** Lifting/restriction/beta (LOW LEVEL, don't use) *)
   val move : from:int -> to_:int -> Data.term -> Data.term
   val beta : depth:int -> Data.term -> Data.term list -> Data.term
diff --git a/src/compiler.ml b/src/compiler.ml
index b58f60917..92190f80d 100644
--- a/src/compiler.ml
+++ b/src/compiler.ml
@@ -2100,7 +2100,7 @@ let unit_or_header_of_ast { print_passes } s ?(toplevel_macros=F.Map.empty) p =
   s, {
     version = "%%VERSION_NUM%%";
     code = p;
-    symbol_table = Symbols.prune (State.get Symbols.table s) p.Flat.symbols
+    symbol_table = Symbols.prune (State.get Symbols.table s) ~alive:p.Flat.symbols
   }
 ;;
 
@@ -2121,22 +2121,19 @@ let header_of_ast ~flags ~parser:p state_descriptor quotation_descriptor hoas_de
     | Some x ->
         D.State.set D.Conversion.extra_goals_postprocessing state x
     | None -> state in          
+  let { D.QuotationHooks.default_quotation;
+        named_quotations;
+        singlequote_compilation;
+        backtick_compilation } = quotation_descriptor in
+
+  let state = D.State.set CustomFunctorCompilation.backtick state (Option.map snd backtick_compilation) in
+  let state = D.State.set CustomFunctorCompilation.singlequote state (Option.map snd singlequote_compilation) in
+  let state = D.State.set Quotation.default_quotation state default_quotation in
+  let state = D.State.set Quotation.named_quotations state named_quotations in
   let state =
-    let { D.QuotationHooks.default_quotation;
-          named_quotations;
-          singlequote_compilation;
-          backtick_compilation } = quotation_descriptor in
-
-    let state = D.State.set CustomFunctorCompilation.backtick state (Option.map snd backtick_compilation) in
-    let state = D.State.set CustomFunctorCompilation.singlequote state (Option.map snd singlequote_compilation) in
-    let state = D.State.set Quotation.default_quotation state default_quotation in
-    let state = D.State.set Quotation.named_quotations state named_quotations in
-    let state =
-      let eval_map = List.fold_left (fun m (c,{ CalcHooks.code }) -> Constants.Map.add c code m) Constants.Map.empty (List.rev calc_descriptor) in
-      D.State.set CalcHooks.eval state eval_map in
-    state
-  in
-
+    let eval_map = List.fold_left (fun m (c,{ CalcHooks.code }) -> Constants.Map.add c code m) Constants.Map.empty (List.rev calc_descriptor) in
+    D.State.set CalcHooks.eval state eval_map in
+  let state = D.State.set parser state (Some p) in
   let state = D.State.set D.while_compiling state true in
   let state = State.set Symbols.table state (Symbols.global_table ()) in
   let state =
@@ -2147,7 +2144,6 @@ let header_of_ast ~flags ~parser:p state_descriptor quotation_descriptor hoas_de
       | Data.BuiltInPredicate.MLDataC _ -> state
       | Data.BuiltInPredicate.LPCode _ -> state
       | Data.BuiltInPredicate.LPDoc _ -> state) state decls) state builtins in
-  let state = D.State.set parser state (Some p) in
   let state, u = unit_or_header_of_ast flags state ast in
   print_unit flags u;
   state, u
diff --git a/src/data.ml b/src/data.ml
index 351fceb74..cb62d0304 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -286,8 +286,8 @@ module State : sig
      - end_compilation (just once before running)
      - end_execution (just once after running)
   *)
+  
   val init : descriptor -> t
-  val descriptor : t -> descriptor
   val end_clause_compilation : t -> t
   val begin_goal_compilation : t -> t
   val end_goal_compilation : uvar_body StrMap.t -> t -> t
@@ -301,9 +301,12 @@ module State : sig
   val update_return : 'a component -> t -> ('a -> 'a * 'b) -> t * 'b
   val pp : Format.formatter -> t -> unit
 
+  val dummy : t
+
 end = struct
 
   type stage =
+    | Dummy
     | Compile_prog
     | Compile_goal
     | Link
@@ -323,6 +326,7 @@ end = struct
   type descriptor = extension StrMap.t ref
 
   type t = { data : Obj.t StrMap.t; stage : stage; extensions : descriptor }
+  let dummy : t = { data = StrMap.empty; stage = Dummy; extensions = ref StrMap.empty }
   let descriptor { extensions = x } = x
  
   let new_descriptor () : descriptor = ref StrMap.empty
@@ -366,13 +370,15 @@ end = struct
     name
 
   let init extensions : t =
-    { data =
-       StrMap.fold (fun name { init } acc ->
-        let o = init () in
-        StrMap.add name o acc)
-        !extensions StrMap.empty;
+    let data = StrMap.fold (fun name { init } acc ->
+      let o = init () in
+      StrMap.add name o acc)
+      !extensions StrMap.empty in
+    {
+      data;
       stage = Compile_prog;
-      extensions }
+      extensions;
+    }
 
   let end_clause_compilation { data = m; stage = s; extensions } : t =
     assert(s = Compile_prog);
diff --git a/src/dune b/src/dune
index 20a1b2aa0..e7cc1ca66 100644
--- a/src/dune
+++ b/src/dune
@@ -82,5 +82,3 @@
 (rule
   (targets trace.ts)
   (action (run atdts %{dep:trace.atd})))
-
-(include dune.config)
diff --git a/src/legacy_parser/dune b/src/legacy_parser/dune
deleted file mode 100644
index 499e68fe5..000000000
--- a/src/legacy_parser/dune
+++ /dev/null
@@ -1,7 +0,0 @@
-(library
-  (name elpi_legacy_parser)
-  (public_name elpi.legacy_parser)
-  (libraries elpi.util elpi.parser camlp5.gramlib)
-  (flags -w -A)
-  (preprocess (per_module ((action (run camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file})) parser)))
-  (modules parser))
diff --git a/src/legacy_parser/parser.ml b/src/legacy_parser/parser.ml
deleted file mode 100644
index 7ce33d80a..000000000
--- a/src/legacy_parser/parser.ml
+++ /dev/null
@@ -1,893 +0,0 @@
-(* elpi: embedded lambda prolog interpreter                                  *)
-(* license: GNU Lesser General Public License Version 2.1 or later           *)
-(* ------------------------------------------------------------------------- *)
-
-open Elpi_util
-
-module U = Util
-module Loc = U.Loc
-open Elpi_parser.Ast
-open Elpi_parser.Parser_config
-open Term
-
-module Str = Re.Str
-
-let of_ploc l = {
-  Loc.source_name = Ploc.file_name l;
-  source_start = Ploc.first_pos l;
-  source_stop = Ploc.last_pos l;
-  line = Ploc.line_nb l;
-  line_starts_at = Ploc.bol_pos l;
-}
-let to_ploc {
-  Loc.source_name = source_name;
-  line = line;
-  line_starts_at = line_starts_at;
-  source_start = source_start;
-  source_stop = source_stop;
-} = Ploc.make_loc source_name line line_starts_at (source_start, source_stop) ""
-
-type fixity = Infixl | Infixr | Infix | Prefix | Prefixr | Postfix | Postfixl
-
-let fixity_of_string = function
-  | "infixl" -> Infixl 
-  | "infixr" -> Infixr 
-  | "infix" -> Infix 
-  | "prefix" -> Prefix 
-  | "prefixr" -> Prefixr 
-  | "postfix" -> Postfix 
-  | "postfixl" -> Postfixl
-  | s -> raise (Stream.Error ("invalid fixity: " ^ s))
-
-let set_precedence, precedence_of =
- let module ConstMap = Map.Make(Func) in 
- let precs = ref ConstMap.empty in
- (fun c p -> precs := ConstMap.add c p !precs),
- (fun c -> ConstMap.find c !precs)
-;;
-
-type parser_state_aux = { file_resolver : ?cwd:string -> unit:string -> unit -> string }
-type parser_state = parser_state_aux option
-let parser_state = ref { file_resolver = (fun ?cwd:_ ~unit:_ () -> assert false) }
-let cur_dirname = ref "./"
-
-let last_loc : Ploc.t ref = ref (Ploc.make_loc "dummy" 1 0 (0, 0) "")
-let set_fname ?(line=1) fname = last_loc := (Ploc.make_loc fname line 0 (0, 0) "")
-
-let rec readsymlinks f =
-  try
-    let link = Unix.readlink f in
-    if not(Filename.is_relative link) then readsymlinks link
-    else readsymlinks Filename.(concat (dirname f) link)
-  with Unix.Unix_error _ | Failure _ -> f
-
-let symlink_dirname f = Filename.dirname (readsymlinks f)
-
-let make_absolute cwd filename =
-  if not (Filename.is_relative filename) then filename
-  else Filename.concat cwd filename
-
-let parse_silent = ref true
-(* the parsed variable is a cache to avoid parsing the same file twice *)
-let parsed = ref []
-
-let resolve ?cwd ~unit () = !parser_state.file_resolver ?cwd ~unit ()
-
-let rec parse_one e (origfilename as filename) =
- let origprefixname =
-   try Filename.chop_extension origfilename
-   with Invalid_argument _ ->
-     raise (Failure ("File "^origfilename^" has no extension")) in
- let filename = resolve ~cwd:!cur_dirname ~unit:filename () in
- let prefixname = Filename.chop_extension filename in
- let inode = Digest.file filename in
- if List.mem_assoc inode !parsed then begin
-  if not !parse_silent then Printf.eprintf "already loaded %s\n%!" origfilename;
-  match !(List.assoc inode !parsed) with
-  | None -> inode, []
-  | Some l -> inode, l
- end else begin
-  let sigs =
-   if Filename.check_suffix filename ".sig" then []
-   else
-    let signame = prefixname ^ ".sig" in
-    if Sys.file_exists signame then
-     let origsigname = origprefixname ^ ".sig" in
-     snd (parse_one e origsigname)
-    else [] in
-  if not !parse_silent then
-    Printf.printf "loading %s (%s)\n%!" origfilename (Digest.to_hex inode);
-  let ast = ref None in
-  parsed := (inode,ast) ::!parsed ;
-  let ch = open_in filename in
-  let saved_cur_dirname = !cur_dirname in
-  cur_dirname := symlink_dirname filename;
-  inode, sigs @
-  try
-   let loc = !last_loc in
-   set_fname filename;
-   let res = Grammar.Entry.parse e (Stream.of_channel ch)in
-   last_loc := loc;
-   ast := Some res;
-   close_in ch;
-   cur_dirname := saved_cur_dirname;
-   res
-  with Ploc.Exc(l,(Token.Error msg | Stream.Error msg)) ->
-    close_in ch;
-    let loc = of_ploc l in
-    raise (ParseError(loc,msg))
-  | Ploc.Exc(_,e) -> close_in ch; raise e
- end
-  
-let parse e filenames =
-  List.concat (List.map (fun x -> snd (parse_one e x)) filenames)
-
-let string_of_chars chars = 
-  let buf = Buffer.create 10 in
-  List.iter (Buffer.add_char buf) chars;
-  Buffer.contents buf
-let _spy ?(name="") ?pp f b s =
-  let l = Stream.npeek 10 s in
-  Printf.eprintf "%s< %s | %S...\n"
-    name (Plexing.Lexbuf.get b) (string_of_chars l);
-  try
-    let b = f b s in
-    begin match pp with
-    | None -> Printf.eprintf "%s> ok" name
-    | Some pp -> Printf.eprintf "%s> %s\n\n" name (pp b)
-    end; b
-  with e ->
-    Printf.eprintf "nope\n";
-    raise e
-;;
-
-let digit = lexer [ '0'-'9' ]
-(* let octal = lexer [ '0'-'7' ] *)
-(* let hex = lexer [ '0'-'9' | 'A'-'F' | 'a'-'f' ] *)
-let schar2 =
- lexer [ '+'  | '*' | '/' | '^' | '<' | '>' | '`' | '\'' | '?' | '@' | '#'
-       | '~' | '=' | '&' | '!' ]
-let schar = lexer [ schar2 | '-' | '$' | '_' ]
-let lcase = lexer [ 'a'-'z' ]
-let ucase = lexer [ 'A'-'Z' ]
-let idchar = lexer [ lcase | ucase | digit | schar ]
-let rec idcharstar = lexer [ idchar idcharstar | ]
-let rec idcharstarns = lexer [ idchar idcharstarns | ?= [ '.' 'a'-'z' | '.' 'A'-'Z' ] '.' idchar idcharstarns | ]
-let idcharplus = lexer [ idchar idcharstar ]
-let rec pnum = lexer [ digit | digit pnum ]
-let num = lexer [ pnum | ?= [ '-' '0'-'9' ] '-' pnum ]
-let symbchar = lexer [ lcase | ucase | digit | schar | ':' ]
-let rec symbcharstar = lexer [ symbchar symbcharstar | ]
-
-let succ_line ?(eol_num=1) loc ep =
-  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + eol_num) ep
-                (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
-let stringchar eol_found = lexer
- [ "\\\\" / -> $add "\\"
- | "\\n" / -> $add "\n"
- | "\\b" / -> $add "\b"
- | "\\t" / -> $add "\t"
- | "\\r" / -> $add "\r"
- | "\\x" / -> $add "\x"
- | "\\\"" / -> $add "\""
- (* CSC: I have no idea how to implement the \octal syntax & friend :-(
- | "\\" / [ -> buflen := String.length $buf ; $add "" ] octal / ->
-    $add (mkOctal "4")*)
- | "\n" / -> incr eol_found ; $add "\n"
- | _ ]
-
-let rec string eol_found = lexer [ '"' / '"' (string eol_found) | '"' / | (stringchar eol_found) (string  eol_found)]
-let any eol_found = lexer
-  [ "\n" -> incr eol_found ; $add "\n"
-  | _ ]
-let mk_terminator keep n b s =
-  let l = Stream.npeek n s in
-  if List.length l = n && List.for_all ((=) '}') l then begin
-   let b = ref b in
-   for _i = 1 to n do
-     Stream.junk s;
-     if keep then b := Plexing.Lexbuf.add '}' !b;
-   done; !b
-  end else raise Stream.Failure
-let rec quoted_inner eol_found d = (*spy ~name:"quoted_inner"*) (lexer
-  [ d
-  | "{" (maybe_quoted_inner eol_found d)
-  | (any eol_found) (quoted_inner eol_found d) ])
-and maybe_quoted_inner eol_found d = (*spy ~name:"maybe"*) (lexer
-  [ d
-  | "{" (quoted eol_found true 2) (quoted_inner eol_found d)
-  | (any eol_found) (quoted_inner eol_found d) ])
-and  quoted eol_found keep n = (*spy ~name:"quoted"*) (lexer
-  [ "{" (quoted eol_found keep (n+1))
-  | (quoted_inner eol_found (mk_terminator keep n)) ])
-
-let constant = "CONSTANT" (* to use physical equality *)
-
-let rec tok b s = let eol_found = ref 0 in (*spy ~name:"tok" ~pp:(fun (a,b) -> a ^ " " ^ b)*) (lexer
-  [ ucase idcharstar -> constant,$buf,!eol_found
-  | lcase idcharstarns -> constant,$buf,!eol_found
-  | schar2 symbcharstar -> constant,$buf,!eol_found
-  | num -> "INTEGER",$buf,!eol_found
-  | num ?= [ '.' '0'-'9' ] '.' pnum -> "FLOAT",$buf,!eol_found
-  | '-' idcharstar -> constant,$buf,!eol_found
-  | '_' -> "FRESHUV", "_",!eol_found
-  | '_' idcharplus -> constant,$buf,!eol_found
-  | ":-"  -> constant,$buf,!eol_found
-  | ":"  -> "COLON",$buf,!eol_found
-  | "::"  -> constant,$buf,!eol_found
-  | ',' -> constant,$buf,!eol_found
-  | ';' -> constant,$buf,!eol_found
-  | '?' -> constant,$buf,!eol_found
-  | '.' -> "FULLSTOP",$buf,!eol_found
-  | '.' pnum -> "FLOAT",$buf,!eol_found
-  | '\\' -> "BIND","\\",!eol_found
-  | '(' [ is_infix ->
-             "ESCAPE",  String.(sub $buf 0 (length $buf - 1)),!eol_found
-        | -> "LPAREN",$buf,!eol_found ]
-  | ')' -> "RPAREN",$buf,!eol_found
-  | '[' -> "LBRACKET",$buf,!eol_found
-  | ']' -> "RBRACKET",$buf,!eol_found
-  | "{{" / (quoted eol_found false 2) -> "QUOTED", $buf,!eol_found
-  | '{' -> "LCURLY",$buf,!eol_found
-  | '}' -> "RCURLY",$buf,!eol_found
-  | '|' -> "PIPE",$buf,!eol_found
-  | '"' / (string eol_found) -> "LITERAL", $buf, !eol_found
-]) b s
-and is_infix_aux b s =
-  let k1, s1, _ = tok b s in
-  let k2, s2, _ = tok b s in 
-  if k1 == constant && k2 = "RPAREN" && not (is_capital s1.[0])
-  then string2lexbuf2 s1 s2
-  else if k1 = "LBRACKET" && k2 = "RBRACKET" then
-    let k3, s3, _ = tok b s in
-    if k3 = "RPAREN" then string2lexbuf3 s1 s2 s3
-    else raise Stream.Failure
-  else raise Stream.Failure
-and protect max_chars lex s =
-  let l = Stream.npeek max_chars s in
-  let safe_s = Stream.of_list l in
-  let to_junk, res = lex Plexing.Lexbuf.empty safe_s in
-  for _i = 0 to to_junk-1 do Stream.junk s; done;
-  res
-and is_infix _ s = protect 6 is_infix_aux s
-and string2lexbuf2 s1 s2 =
-  let b = ref Plexing.Lexbuf.empty in
-  String.iter (fun c -> b := Plexing.Lexbuf.add c !b) s1;
-  String.iter (fun c -> b := Plexing.Lexbuf.add c !b) s2;
-  String.(length s1 + length s2), !b
-and string2lexbuf3 s1 s2 s3 =
-  let b = ref Plexing.Lexbuf.empty in
-  String.iter (fun c -> b := Plexing.Lexbuf.add c !b) s1;
-  String.iter (fun c -> b := Plexing.Lexbuf.add c !b) s2;
-  String.iter (fun c -> b := Plexing.Lexbuf.add c !b) s3;
-  String.(length s1 + length s2 + length s3), !b
-and is_capital c = match c with 'A'..'Z' -> true | _ -> false
-
-let option_eq x y = match x, y with Some x, Some y -> x == y | _ -> x == y
-
-module StringSet = Set.Make(String);;
-let symbols = ref StringSet.empty;;
-
-let literatebuf = Buffer.create 17;;
-
-(* %! <= \leq creates a map from "<=" to "\leq" *)
-let set_liter_map, get_literal, _print_lit_map =
- let lit_map = ref U.StrMap.empty in
- (fun s1 s2 -> lit_map := U.StrMap.add s1 s2 !lit_map),
- (fun s -> U.StrMap.find s !lit_map),
- (fun () -> U.StrMap.iter (fun s1 s2 -> Format.printf "\n%s -> %s\n%!" s1 s2) !lit_map);;
-
-
-let set_loc_pos loc init bp ep =
-  Ploc.sub loc (bp - init) (ep - bp)
-
-let rec lex loc c init = parser bp
-  | [< '( ' ' | '\t' | '\r' ); s >] -> lex loc c init s
-  | [< '( '\n' ) ; s >] ep -> lex (succ_line loc ep) c init s
-  | [< '( '%' ); '( '!'); s >] -> literatecomment loc c init s
-  | [< '( '%' ); s >] -> comment loc c init s
-  | [< ?= [ '/'; '*' ]; '( '/' ); '( '*' ); s >] -> comment2 loc 0 c init s
-  | [< s >] ->
-       if option_eq (Stream.peek s) None
-       then ("EOF",""), (set_loc_pos loc init bp bp)
-       else
-        let x,y, eol_num = tok c s in
-        let res = x, y in
-        let ep = Stream.count s in
-        let loc = succ_line ~eol_num loc ep in
-        (if x == constant then
-         (match y with
-         | "module" -> "MODULE", "module"
-         | "sig" -> "SIG", "SIG"
-         | "import" -> "IMPORT", "accumulate"
-         | "shorten" -> "SHORTEN", "shorten"
-         | "accum_sig" -> "ACCUM_SIG", "accum_sig"
-         | "use_sig" -> "USE_SIG", "use_sig"
-         | "local" -> "LOCAL", "local"
-         | "pred" -> "PRED", "pred"
-         | "mode" -> "MODE", "mode"
-         | "macro" -> "MACRO", "macro"
-         | "rule" -> "RULE", "rule"
-         | "namespace" -> "NAMESPACE", "namespace"
-         | "constraint" -> "CONSTRAINT", "constraint"
-         | "localkind" -> "LOCALKIND", "localkind"
-         | "useonly" -> "USEONLY", "useonly"
-         | "exportdef" -> "EXPORTDEF", "exportdef"
-         | "kind" -> "KIND", "kind"
-         | "typeabbrev" -> "TYPEABBREV", "typeabbrev"
-         | "type" -> "TYPE", "type"
-         | "external" -> "EXTERNAL", "external"
-         | "closed" -> "CLOSED", "closed"
-         | "end" -> "EOF", "end"
-         | "accumulate" -> "ACCUMULATE", "accumulate"
-         | "infixl" -> "FIXITY", "infixl"
-         | "infixr" -> "FIXITY", "infixr"
-         | "infix" -> "FIXITY", "infix"
-         | "prefix" -> "FIXITY", "prefix"
-         | "prefixr" -> "FIXITY", "prefixr"
-         | "postfix" -> "FIXITY", "postfix"
-         | "postfixl" -> "FIXITY", "postfixl"
-        
-         | x when StringSet.mem x !symbols -> "SYMBOL",x
-        
-         | _ -> res) else res), (set_loc_pos loc init bp ep)
-and literatecomment loc c init = parser
-  | [< '( '\n' ); s >] ep ->
-      let loc = succ_line loc ep in
-      let buf = Buffer.contents literatebuf in
-      Buffer.reset literatebuf;
-      let list_str = Str.split (Str.regexp " +") buf in
-      (match list_str with
-       | [s1;s2] -> set_liter_map s1 s2; 
-       | _ -> prerr_endline ("Wrong syntax: literate comment: " ^ buf); exit 1);
-  (*   print_lit_map (); *)
-  (*   prerr_endline buf; (*register imperatively*) *)
-      lex loc c init s
-  | [< '_ as x ; s >] -> Buffer.add_char literatebuf x; literatecomment loc c init s
-and comment loc c init = parser
-  | [< '( '\n' ); s >] ep -> lex (succ_line loc ep) c init s
-  | [< '_ ; s >] -> comment loc c init s
-  | [< >] -> lex loc c init [< >]
-and comment2 loc lvl c init = parser
-  | [< ?= [ '*'; '/' ]; '( '*' ); '( '/'); s >] ->
-      if lvl = 0 then lex loc c init s else comment2 loc (lvl-1) c init s
-  | [< ?= [ '/'; '*' ]; '( '/' ); '( '*' ); s >] -> comment2 loc (lvl+1) c init s
-  | [< '( '\n' ); s >] ep -> comment2 (succ_line loc ep) lvl c init s
-  | [< '_ ; s >] -> comment2 loc lvl c init s
-
-
-open Plexing
-
-(* For some reason, the [Ploc.after] function of Camlp5 does not update line
-   numbers, so we define our own function that does it. *)
-let after loc =
-  let line_nb = Ploc.line_nb_last loc in
-  let bol_pos = Ploc.bol_pos_last loc in
-  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
-                (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
-let lex_fun s =
-  let tab = Locations.create () in
-  (Stream.from (fun id ->
-     let tok, loc = lex !last_loc Lexbuf.empty (Stream.count s) s in
-(*      Printf.eprintf "tok: %s, %s, %s\n" (Loc.show (of_ploc loc)) (fst tok) (snd tok); *)
-     last_loc := after loc;
-     Locations.add tab id loc;
-     Some tok)),
-  tab
-;;
-
-let tok_match =
- function
-    ((s1:string),"") ->
-      fun ((s2:string),v) ->
-       if Stdlib.compare s1 s2 == 0 then v else raise Stream.Failure
-  | ((s1:string),v1) ->
-      fun ((s2:string),v2) ->
-       if Stdlib.compare s1 s2==0 && Stdlib.compare v1 v2==0 then v2
-       else raise Stream.Failure
-
-let lex = {
-  tok_func = lex_fun;
-  tok_using =
-   (fun x,y ->
-      if x = "SYMBOL" && y <> "" then begin
-       symbols := StringSet.add y !symbols
-      end
-   );
-  tok_removing = (fun _ -> ());
-  tok_match = tok_match;
-  tok_text = (function (s,y) -> s ^ " " ^ y);
-  tok_comm = None;
-}
-
-let g = Grammar.gcreate lex
-let lp = Grammar.Entry.create g "lp"
-let goal = Grammar.Entry.create g "goal"
-let atom = Grammar.Entry.create g "atom"
-
-let min_precedence = -1  (* minimal precedence in use *)
-let lam_precedence = -1  (* precedence of lambda abstraction *)
-let umin_precedence = 0   (* minimal user defined precedence *)
-let umax_precedence = 256 (* maximal user defined precedence *)
-let appl_precedence = umax_precedence + 1 (* precedence of application *)
-let inf_precedence = appl_precedence+1 (* greater than any used precedence*)
-
-(*
-let dummy_prod =
- let dummy_action =
-   Gramext.action (fun _ ->
-     failwith "internal error, lexer generated a dummy token") in
- [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ]
-*)
-
-let used_precedences = ref [110];;
-let is_used n =
- let rec aux visited acc =
-  function
-     hd::_  when hd = n ->
-     !used_precedences, (Gramext.Level (string_of_int n), None)
-   | hd::tl when hd < n ->
-     aux (hd::visited) (Gramext.After (string_of_int hd)) tl
-   | l -> List.rev (n::visited) @ l, (acc, Some (string_of_int n))
- in
-  let used, res = aux [] Gramext.First !used_precedences in
-  used_precedences := used ;
-  res
-;;
-
-let desugar_multi_binder loc = function
-  | App(Const hd as binder,args)
-    when Func.equal hd Func.pif || Func.equal hd Func.sigmaf && List.length args > 1 ->
-      let last, rev_rest = let l = List.rev args in List.hd l, List.tl l in
-      let names = List.map (function
-        | Const x -> Func.show x
-        | (App _ | Lam _ | CData _ | Quoted _) ->
-            U.error "multi binder syntax") rev_rest in
-      let body = mkApp (of_ploc loc) [binder;last] in
-      List.fold_left (fun bo name -> mkApp (of_ploc loc) [binder;mkLam name bo]) body names
-  | (App _ | Const _ | Lam _ | CData _ | Quoted _) as t -> t
-;;
-
-let desugar_macro loc = function
-  | App(Const hd,[Const name; body]) when Func.equal hd Func.rimplf ->
-      if ((Func.show name).[0] != '@') then
-        raise (Stream.Error "Macro name must begin with @");
-      name, body
-  | App(Const hd,[App(Const name,args); body]) when Func.equal hd Func.rimplf ->
-      if ((Func.show name).[0] != '@') then
-        raise (Stream.Error "Macro name must begin with @");
-      let names = List.map (function
-        | Const x -> Func.show x
-        | (App _ | Lam _ | CData _ | Quoted _) ->
-             U.error ~loc "macro binder syntax") args in
-      name, List.fold_right mkLam names body
-  | (App _ | Const _ | Lam _ | CData _ | Quoted _) as x ->
-        raise (Stream.Error ("Illformed macro:" ^ show x))
-;;
-
-let constant_colon strm =
-  match Stream.npeek 2 strm with
-  | [ ("CONSTANT",_); ("COLON",_) ] -> ()
-  | _ -> raise Stream.Failure
-let constant_colon =
-  Grammar.Entry.of_parser g "constant_colon" constant_colon
-
-type gramext = { fix : fixity; sym : string; prec : int }
-
-let gram_extend loc { fix; sym = cst; prec = nprec } =
-  if nprec < umin_precedence || nprec > umax_precedence then
-    raise (ParseError(loc,Printf.sprintf "precedence muse be inside [%d,%d]" umin_precedence umax_precedence))
-  else
-    let hash_expr e =
-       e
-       |> Hashtbl.hash
-       |> Printf.sprintf "%08x" in
-    let binrule =
-     [ Gramext.Sself ; Gramext.Stoken ("SYMBOL",cst); Gramext.Sself ],
-     hash_expr     "(fun t2 cst t1 loc -> mkApp (of_ploc loc) [mkCon cst;t1;t2])",
-     Gramext.action (fun t2 cst t1 loc -> mkApp (of_ploc loc) [mkCon cst;t1;t2]) in
-    let prerule =
-     [ Gramext.Stoken ("SYMBOL",cst); Gramext.Sself ],
-     hash_expr     "(fun t cst loc -> mkApp (of_ploc loc) [mkCon cst;t])",
-     Gramext.action (fun t cst loc -> mkApp (of_ploc loc) [mkCon cst;t]) in
-    let postrule =
-     [ Gramext.Sself ; Gramext.Stoken ("SYMBOL",cst) ],
-     hash_expr     "(fun cst t loc -> mkApp (of_ploc loc) [mkCon cst;t])",
-     Gramext.action (fun cst t loc -> mkApp (of_ploc loc) [mkCon cst;t]) in
-    let ppinfo = fix, nprec in
-    let fixity,rule =
-     (* NOTE: we do not distinguish between infix and infixl,
-        prefix and prefix, postfix and postfixl *)
-     match fix with
-       Infix    -> Gramext.NonA,   binrule
-     | Infixl   -> Gramext.LeftA,  binrule
-     | Infixr   -> Gramext.RightA, binrule
-     | Prefix   -> Gramext.NonA,   prerule
-     | Prefixr  -> Gramext.RightA, prerule
-     | Postfix  -> Gramext.NonA,   postrule
-     | Postfixl -> Gramext.LeftA,  postrule in
-    set_precedence (Func.from_string cst) ppinfo ;
-    let where,name = is_used nprec in
-     Grammar.extend
-      [Grammar.Entry.obj atom, Some where, [name, Some fixity, [rule]]];
-;;
-          (* Debugging code
-          prerr_endline "###########################################";
-          Grammar.iter_entry (
-            Grammar.print_entry Format.err_formatter
-          ) (Grammar.Entry.obj atom);
-          prerr_endline ""; *)
-
-let accumulate loc extension modnames =
-  List.map (fun file -> Program.Accumulated(of_ploc loc, [parse_one lp (file ^ extension)])) modnames
-
-EXTEND
-  GLOBAL: lp goal atom;
-  lp: [ [ cl = LIST0 decl; EOF -> List.concat cl ] ];
-  const_sym:
-    [[ c = CONSTANT -> c
-     | s = SYMBOL -> s
-     | e = ESCAPE -> e ]];
-  filename:
-    [[ c = CONSTANT -> c
-     | c = LITERAL -> c ]];
-  i_o : [[ CONSTANT "i" -> true | CONSTANT "o" -> false ]];
-  mode :
-    [[ LPAREN; c = CONSTANT; l = LIST1 i_o; RPAREN ->
-       { Mode.name = Func.from_string c; args = l; loc = of_ploc loc} ]];
-  chrrule :
-    [[ to_match = LIST0 sequent;
-       to_remove = OPT [ BIND; l = LIST1 sequent -> l ];
-       guard = OPT [ PIPE; a = atom LEVEL "abstterm" -> a ];
-       new_goal = OPT [ SYMBOL "<=>"; gs = sequent -> gs ] ->
-         { Chr.to_match = to_match;
-               to_remove = Util.option_default [] to_remove;
-               guard = guard;
-               new_goal = new_goal;
-               attributes=[];
-               loc=(of_ploc loc) }
-    ]];
-  sequent_core :
-    [ [ constant_colon; e = CONSTANT; COLON; t = atom -> Some e, (t : Term.t) 
-      | t = atom -> None, (t : Term.t) ]
-    ];
-  sequent :
-   [[ LPAREN; c = sequent_core; RPAREN ->
-         let e, t1 = (c : string option * Term.t) in
-         let eigen =
-           match e with Some x -> mkCon x | None -> mkFreshUVar () in
-         let context, conclusion =
-           match t1 with
-           | App(Const x,[a;b]) when Func.equal x Func.sequentf -> a, b
-           | (App _ | Const _ | Lam _ | CData _ | Quoted _) ->
-                mkFreshUVar (), t1 in
-         { Chr.eigen = eigen; context; conclusion }
-    | c = atom LEVEL "abstterm" ->
-         { Chr.eigen = mkFreshUVar (); context = mkFreshUVar (); conclusion = c }
-   ]];
-  indexing_arg_spec :
-  [[ d = INTEGER -> int_of_string d
-   | FRESHUV -> 0
-   ]];
-  indexing_expr :
-    [[ LPAREN; l = LIST1 indexing_arg_spec; RPAREN -> l ]];
-  clause_attribute :
-   [[ CONSTANT "name";   name = LITERAL -> Name name
-    | CONSTANT "before"; name = LITERAL -> Before name
-    | CONSTANT "after";  name = LITERAL -> After name
-    | CONSTANT "if";     expr = LITERAL -> If expr
-    ]];
-  type_attribute :
-   [[ CONSTANT "index";  expr = indexing_expr -> Index expr
-    ]];
-  clause_attributes : [[ l = LIST1 clause_attribute SEP COLON-> l ]];
-  type_attributes : [[ l = LIST1 type_attribute SEP COLON-> l ]];
-  pragma : [[ CONSTANT "#line"; l = INTEGER; f = LITERAL ->
-    set_fname ~line:(int_of_string l) f ]];
-  pred_item : [[ m = i_o; COLON; t = ctype -> (m,t) ]];
-  pred : [[ c = const_sym; a = LIST0 pred_item SEP SYMBOL "," ->
-    let name = Func.from_string c in
-    [ { Mode.name = name; args = List.map fst a; loc = (of_ploc loc)} ],
-     (name, List.fold_right (fun (_,t) ty ->
-        mkApp (of_ploc loc) [mkCon "->";t;ty]) a (mkCon "prop"))
-  ]];
-  string_trie_aux :
-    [ [ name = CONSTANT -> [name,name]
-      | prefix = CONSTANT; FULLSTOP;
-          LCURLY; l = LIST1 SELF SEP SYMBOL ","; RCURLY ->
-        List.map (fun (p,x) -> prefix ^ "." ^ p, x) (List.flatten l)
-  ]];
-  string_trie :
-    [ [ prefix = CONSTANT; FULLSTOP;
-          LCURLY; l = LIST1 string_trie_aux SEP SYMBOL ","; RCURLY ->
-        List.map (fun (p,x) -> prefix ^ "." ^ p, x) (List.flatten l)
-  ]];
-  decl :
-    [[ pragma -> []
-     | COLON; cattributes = clause_attributes; RULE; r = chrrule; FULLSTOP ->
-       let cattributes = cattributes in
-       [Program.Chr { r with Chr.attributes = cattributes } ]
-     | RULE; r = chrrule; FULLSTOP ->
-       [Program.Chr { r with Chr.attributes = [] } ]
-     | COLON; attributes = type_attributes; PRED; p = pred; FULLSTOP ->
-         let m, (n,t) = p in
-         [Program.Type [{ Type.loc=of_ploc loc; attributes; name = n ; ty = t }]; Program.Mode m]
-     | PRED; p = pred; FULLSTOP ->
-         let m, (n,t) = p in
-         [Program.Type [{ Type.loc=of_ploc loc; attributes = []; name = n ; ty = t }]; Program.Mode m]
-     | COLON; attributes = type_attributes; TYPE;
-       names = LIST1 const_sym SEP SYMBOL ","; t = type_; FULLSTOP ->
-        [Program.Type 
-          (List.map (fun n ->
-           { Type.loc=of_ploc loc; attributes; name=Func.from_string n; ty=t })
-           names)]
-     | TYPE; names = LIST1 const_sym SEP SYMBOL ","; t = type_; FULLSTOP ->
-        [Program.Type
-          (List.map (fun n ->
-           { Type.loc=of_ploc loc; attributes = []; name=Func.from_string n; ty=t })
-           names)]
-     | KIND; names = LIST1 const_sym SEP SYMBOL ","; t = kind; FULLSTOP ->
-        [Program.Type 
-          (List.map (fun n ->
-           { Type.loc=of_ploc loc; attributes=[]; name=Func.from_string n; ty=t })
-           names)]
-     | COLON; attributes = clause_attributes; f = atom; FULLSTOP ->
-       let c = { Clause.loc = of_ploc loc; attributes; body = f } in
-       [Program.Clause c]
-     | f = atom; FULLSTOP ->
-       let c = { Clause.loc = of_ploc loc; attributes = []; body = f } in
-       [Program.Clause c]
-     | EXTERNAL;
-       TYPE; names = LIST1 const_sym SEP SYMBOL ","; t = type_; FULLSTOP ->
-        [Program.Type 
-          (List.map (fun n ->
-           { Type.loc = of_ploc loc;
-                  attributes=[External];
-                  name=Func.from_string n;
-                  ty=t })
-         names)]
-     | EXTERNAL; PRED; p = pred; FULLSTOP ->
-         let _, (n,t) = p in (* No mode for ML code *)
-         [Program.Type [{ Type.loc = of_ploc loc;
-                 attributes = [External];
-                 name = n;
-                 ty = t }]]
-     | LCURLY -> [Program.Begin (of_ploc loc)]
-     | RCURLY -> [Program.End (of_ploc loc)]
-     | MODE; m = LIST1 mode SEP SYMBOL ","; FULLSTOP -> [Program.Mode m]
-     | MACRO; b = atom; FULLSTOP ->
-         let name, body = desugar_macro (of_ploc loc) b in
-         [Program.Macro { Macro.loc = of_ploc loc; name = name; body = body }]
-     | NAMESPACE; ns = CONSTANT; LCURLY ->
-         [ Program.Namespace (of_ploc loc, Func.from_string ns) ]
-     | CONSTRAINT; names=LIST0 CONSTANT; LCURLY ->
-         [ Program.Constraint (of_ploc loc, List.map Func.from_string names) ]
-     | MODULE; CONSTANT; FULLSTOP -> []
-     | SIG; CONSTANT; FULLSTOP -> []
-     | ACCUMULATE; filenames=LIST1 filename SEP SYMBOL ","; FULLSTOP ->
-         accumulate loc ".elpi" filenames
-     | IMPORT; filenames=LIST1 CONSTANT SEP SYMBOL ","; FULLSTOP ->
-         accumulate loc ".elpi" filenames
-     | ACCUM_SIG; filenames=LIST1 filename SEP SYMBOL ","; FULLSTOP ->
-         accumulate loc ".sig" filenames
-     | USE_SIG; filenames=LIST1 filename SEP SYMBOL ","; FULLSTOP ->
-         accumulate loc ".sig" filenames
-     | SHORTEN; names = string_trie; FULLSTOP ->
-        List.map (fun (prefix, name) ->
-          Program.Shorten(of_ploc loc, [Func.from_string prefix, Func.from_string name]))
-          names
-     | LOCAL; vars = LIST1 const_sym SEP SYMBOL ","; FULLSTOP ->
-        [Program.mkLocal vars]
-     | LOCAL; vars = LIST1 const_sym SEP SYMBOL ","; type_; FULLSTOP ->
-        [Program.mkLocal vars]
-     | LOCALKIND; LIST1 const_sym SEP SYMBOL ","; FULLSTOP -> []
-     | LOCALKIND; LIST1 const_sym SEP SYMBOL ","; kind; FULLSTOP -> []
-     | CLOSED; LIST1 const_sym SEP SYMBOL ","; FULLSTOP -> []
-     | CLOSED; LIST1 const_sym SEP SYMBOL ","; type_; FULLSTOP -> []
-     | USEONLY; LIST1 const_sym SEP SYMBOL ","; FULLSTOP -> []
-     | USEONLY; LIST1 const_sym SEP SYMBOL ","; type_; FULLSTOP -> []
-     | EXPORTDEF; LIST1 const_sym SEP SYMBOL ","; FULLSTOP -> []
-     | EXPORTDEF; LIST1 const_sym SEP SYMBOL ","; type_; FULLSTOP -> []
-     | TYPEABBREV; a = abbrform; t = type_; FULLSTOP -> [
-         let name, args = a in
-         let nparams = List.length args in
-         let value = List.fold_right mkLam args t in
-         TypeAbbreviation { TypeAbbreviation.name = name;
-                            nparams = nparams; value = value;
-                            loc = of_ploc loc }
-       ]
-     | fix = FIXITY; syms = LIST1 const_sym SEP SYMBOL ","; prec = INTEGER; FULLSTOP ->
-         List.iter (fun sym ->
-           gram_extend (of_ploc loc) {
-             fix = fixity_of_string fix;
-             sym;
-             prec = int_of_string prec
-           }) syms;
-         []
-    ]];
-  kind:
-    [[ t = TYPE -> mkCon t
-     | t = TYPE; a = SYMBOL "->"; k = kind -> mkApp (of_ploc loc) [mkCon a; mkCon t; k]
-    ]];
-  type_:
-    [[ c = ctype -> c
-     | s = ctype; a = SYMBOL "->"; t = type_ -> mkApp (of_ploc loc) [mkCon a; s; t]
-    ]];
-  ctype:
-     [ "main" [ c = CONSTANT; l = LIST0 ctype LEVEL "arg" -> 
-                  if c = "o" && l = [] then mkCon "prop"
-                  else mkApp (of_ploc loc) (mkCon c :: l)
-              | CONSTANT "ctype"; s = LITERAL ->
-                  mkApp (of_ploc loc) [Const Func.ctypef; mkC (cstring.U.CData.cin s)] ]
-     | "arg"  [ c = CONSTANT -> if c = "o" then mkCon "prop" else mkCon c
-              | LPAREN; t = type_; RPAREN -> t ]
-     ];
-  abbrform:
-    [[ c = const_sym -> Func.from_string c, []
-     | LPAREN; hd = const_sym; args = LIST1 CONSTANT; RPAREN -> Func.from_string hd, args
-    ]];
-  goal:
-    [[ OPT pragma; p = premise; OPT FULLSTOP -> of_ploc loc, p ]];
-  premise : [[ a = atom -> a ]];
-  atom :
-   [ "1" [ ]
-   | "110"
-      [ args = LIST1 atom LEVEL "120" SEP SYMBOL "," ->
-          if List.length args > 1 then mkApp (of_ploc loc) (Const Func.andf :: args)
-          else List.hd args
-      ]
-   | "term"
-      [ hd = atom; args = LIST1 atom LEVEL "abstterm" ->
-         desugar_multi_binder loc (mkApp (of_ploc loc) (hd :: args)) ]
-   | "abstterm"
-      [ c=CONSTANT; OPT[COLON;type_]; b=OPT[BIND; a = atom LEVEL "1" -> a ] ->
-          (match b with None -> mkCon c | Some b -> mkLam c b)
-      | u=FRESHUV; OPT[COLON;type_]; b=OPT[BIND; a = atom LEVEL "1" -> a ] ->
-          (match b with None -> mkFreshUVar () | Some b ->
-           mkLam (Func.show Func.dummyname)  b)
-      | s = LITERAL -> mkC (cstring.U.CData.cin s)
-      | s = QUOTED -> mkQuoted (of_ploc loc) s
-      | s = INTEGER -> mkC (cint.U.CData.cin (int_of_string s))
-      | s = FLOAT -> mkC (cfloat.U.CData.cin (float_of_string s))
-      | LPAREN; a = atom; RPAREN -> a
-      | LCURLY; a = atom; RCURLY -> mkApp (of_ploc loc) [Const Func.spillf;a]
-        (* 120 is the first level after 110, which is that of ,
-           Warning: keep the hard-coded constant in sync with
-           the list_element_prec below :-(
-        *)
-      | LBRACKET; xs_holes = LIST0 [ a = atom LEVEL "120" -> Some a | -> None ] SEP SYMBOL ",";
-          tl = OPT [ PIPE; x = atom LEVEL "1" -> x ]; RBRACKET ->
-          let tl = match tl with None -> mkNil | Some x -> x in
-          let xs = Util.map_filter (fun x -> x) xs_holes in
-          if List.length xs_holes > List.length xs + 1 then
-            raise (Token.Error ("List with more , than elements"));
-          if List.length xs_holes = List.length xs + 1 &&
-             List.hd (List.rev xs_holes) <> None then
-            raise (Token.Error ("List with ,, (no element between commas)"));
-          if List.length xs = 0 && tl <> mkNil then 
-            raise (Token.Error ("List with no elements cannot have a tail"));
-          if List.length xs = 0 then mkNil
-          else mkSeq (xs@[tl]) ]
-   | "wtf" 
-      [ s = ESCAPE -> mkCon s ]
-      ];
-END
-
-(* 120 is the first level after 110, which is that of , *)
-let list_element_prec = 120
-
-let parser_initialized = ref false
-
-let init_loc = {
-  Loc.source_name = "";
-  source_start = 0;
-  source_stop = 0;
-  line = -1;
-  line_starts_at = 0;
-}
-
-let set_state = function
-  | None -> ()
-  | Some x ->
-      parsed := [];
-      parser_state := x
-
-
-let run_parser state f x =
-  set_state state;
-  try f x with
-  | Ploc.Exc(l,(Token.Error msg | Stream.Error msg)) ->
-      let loc = of_ploc l in
-      raise(ParseError(loc,msg))
-  | Ploc.Exc(l,NotInProlog(loc,s)) -> raise (ParseError(loc, "NotInProlog: " ^ s))
-  | Ploc.Exc(l,e) ->
-      let loc = of_ploc l in
-      raise(ParseError(loc,"Unexpected exception: " ^ Printexc.to_string e))
-;;
-
-let parse_program s ~print_accumulated_files filenames : Program.t =
-  parse_silent := not print_accumulated_files;
-  run_parser s (parse lp) filenames
-
-let parse_program_from_stream s ~print_accumulated_files loc strm : Program.t =
-  parse_silent := not print_accumulated_files;
-  last_loc := to_ploc loc;
-  run_parser s (Grammar.Entry.parse lp) strm
-
-let set_last_loc = function
-  | None -> ()
-  | Some loc -> last_loc := to_ploc { loc with Loc.source_stop = loc.Loc.source_start }
-
-let parse_goal ?loc s : Goal.t =
-  set_last_loc loc;
-  let stream = Stream.of_string s in
-  let ast = run_parser None (Grammar.Entry.parse goal) stream in
-  let next, _ = lex_fun stream in
-  try begin match Stream.peek next with
-  | None -> ast
-  | Some ("EOF",_) -> ast
-  | Some (_,x) -> raise (ParseError(of_ploc !last_loc,"trailing text after goal: " ^ x))
-  end with Stream.Error _ -> ast
-
-let parse_goal_from_stream ?loc strm =
-  set_last_loc loc;
-  run_parser None (Grammar.Entry.parse goal) strm
-
-let lp_gramext = [
-  { fix = Infixl;	sym = ":-";	prec = 1; };
-  { fix = Infixr;	sym = ";";	prec = 100; };
-  { fix = Infix;	sym = "?-";	prec = 115; };
-  { fix = Infixr;	sym = "->";	prec = 116; };
-  { fix = Infixr;	sym = "&";	prec = 120; };
-  { fix = Infixr;	sym = "=>";	prec = 129; };
-  { fix = Infixl;	sym = "as";	prec = 0; };
-  { fix = Infix;	sym = "<";	prec = 130; };
-  { fix = Infix;	sym = "=<";	prec = 130; };
-  { fix = Infix;	sym = "=";	prec = 130; };
-  { fix = Infix;	sym = "==";	prec = 130; };
-  { fix = Infix;	sym = ">=";	prec = 130; };
-  { fix = Infix;	sym = ">";	prec = 130; };
-  { fix = Infix;	sym = "i<";	prec = 130; };
-  { fix = Infix;	sym = "i=<";	prec = 130; };
-  { fix = Infix;	sym = "i>=";	prec = 130; };
-  { fix = Infix;	sym = "i>";	prec = 130; };
-  { fix = Infix;	sym = "is";	prec = 130; };
-  { fix = Infix;	sym = "r<";	prec = 130; };
-  { fix = Infix;	sym = "r=<";	prec = 130; };
-  { fix = Infix;	sym = "r>=";	prec = 130; };
-  { fix = Infix;	sym = "r>";	prec = 130; };
-  { fix = Infix;	sym = "s<";	prec = 130; };
-  { fix = Infix;	sym = "s=<";	prec = 130; };
-  { fix = Infix;	sym = "s>=";	prec = 130; };
-  { fix = Infix;	sym = "s>";	prec = 130; };
-  { fix = Infix;	sym = "@";	prec = 135; };
-  { fix = Infixr;	sym = "::";	prec = 140; };
-  { fix = Infix;	sym = "`->";	prec = 141; };
-  { fix = Infix;	sym = "`:";	prec = 141; };
-  { fix = Infix;	sym = "`:=";	prec = 141; };
-  { fix = Infixl;	sym = "^";	prec = 150; };
-  { fix = Infixl;	sym = "-";	prec = 150; };
-  { fix = Infixl;	sym = "+";	prec = 150; };
-  { fix = Infixl;	sym = "i-";	prec = 150; };
-  { fix = Infixl;	sym = "i+";	prec = 150; };
-  { fix = Infixl;	sym = "r-";	prec = 150; };
-  { fix = Infixl;	sym = "r+";	prec = 150; };
-  { fix = Infixl;	sym = "/";	prec = 160; };
-  { fix = Infixl;	sym = "*";	prec = 160; };
-  { fix = Infixl;	sym = "div";	prec = 160; };
-  { fix = Infixl;	sym = "i*";	prec = 160; };
-  { fix = Infixl;	sym = "mod";	prec = 160; };
-  { fix = Infixl;	sym = "r*";	prec = 160; };
-  { fix = Prefix;	sym = "~";	prec = 256; };
-  { fix = Prefix;	sym = "i~";	prec = 256; };
-  { fix = Prefix;	sym = "r~";	prec = 256; };
-]
-
-let init  ~file_resolver =
-  if !parser_initialized = false then
-    List.iter (gram_extend init_loc) lp_gramext;
-  parser_initialized := true;
-  Some { file_resolver }
-;;
diff --git a/src/legacy_parser/parser.mli b/src/legacy_parser/parser.mli
deleted file mode 100644
index adf3f40d6..000000000
--- a/src/legacy_parser/parser.mli
+++ /dev/null
@@ -1,42 +0,0 @@
-(* elpi: embedded lambda prolog interpreter                                  *)
-(* license: GNU Lesser General Public License Version 2.1 or later           *)
-(* ------------------------------------------------------------------------- *)
-
-open Elpi_util
-open Elpi_parser
-
-open Util
-open Ast
-
-type fixity = Infixl | Infixr | Infix | Prefix | Prefixr | Postfix | Postfixl
-
-(* raises Not_found is the constant has no declared fixity *)
-val min_precedence : int   (* minimal precedence in use *)
-val lam_precedence : int   (* precedence of lambda abstraction *)
-val appl_precedence : int  (* precedence of applications *)
-val inf_precedence : int   (* greater than any used precedence *)
-val list_element_prec : int
-val precedence_of : Func.t -> fixity * int
-
-type gramext = { fix : fixity; sym : string; prec : int }
-
-type parser_state
-
-(* Loads the basic grammar and sets the paths.
-   Camlp5 limitation: the grammar is loaded once and forall. *)
-val init :
-  file_resolver:(?cwd:string -> unit:string -> unit -> string) ->
-    parser_state
-
-(* BUG: extending the grammar is imperative, cannot be undone *)
-val parse_program : parser_state -> print_accumulated_files:bool -> string list -> Program.t
-val parse_program_from_stream : parser_state -> print_accumulated_files:bool -> Loc.t -> char Stream.t -> Program.t
-val parse_goal : ?loc:Loc.t -> string -> Goal.t
-val parse_goal_from_stream : ?loc:Loc.t -> char Stream.t -> Goal.t
-
-val resolve : ?cwd:string -> unit:string -> unit -> string
-
-val get_literal : string -> string
-
-(* Standard lambda prolog syntax *)
-val lp_gramext : gramext list
diff --git a/src/runtime.ml b/src/runtime.ml
index 2ccfc64d3..bde6bec62 100644
--- a/src/runtime.ml
+++ b/src/runtime.ml
@@ -378,6 +378,7 @@ module ConstraintStoreAndTrail : sig
   val pp_stuck_goal : ?pp_ctx:pp_ctx -> Fmt.formatter -> stuck_goal -> unit
 
   val state : State.t Fork.local_ref
+  val initial_state : State.t Fork.local_ref
 
   (* ---------------------------------------------------- *)
 
@@ -418,7 +419,10 @@ end = struct (* {{{ *)
  }
 
   let state =
-    Fork.new_local (State.init Data.elpi_state_descriptor |> State.begin_goal_compilation |> State.end_goal_compilation StrMap.empty |> State.end_compilation)
+    Fork.new_local State.dummy
+  let initial_state =
+    Fork.new_local State.dummy
+
   let read_custom_constraint ct =
     State.get ct !state
   let update_custom_constraint ct f =
@@ -1726,7 +1730,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
          true
        with RestrictionFailure ->
         (* avoid fail occur-check on: x\A x = A *)
-        match eta_contract_flex depth adepth bdepth e a with
+        match eta_contract_flex depth adepth ~argsdepth:bdepth e a with
         | None -> false
         | Some a -> unif argsdepth matching depth adepth a bdepth b e end
    | UVar (r,origdepth,0), _ when not matching ->
@@ -1746,7 +1750,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
          true
        with RestrictionFailure ->
         (* avoid fail occur-check on: x\A x = A *)
-        match eta_contract_flex depth bdepth bdepth e b with
+        match eta_contract_flex depth bdepth ~argsdepth:bdepth e b with
         | None -> false
         | Some b -> unif argsdepth matching depth adepth a bdepth b e end
 
@@ -1792,7 +1796,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
        e.(i) <- UVar(r,adepth,0);
        let kind = Unification {adepth = adepth+depth; env = e; bdepth = bdepth+depth; a; b; matching} in
        let blockers =
-         match is_flex (adepth+depth) other with
+         match is_flex ~depth:(adepth+depth) other with
          | None -> [r]
          | Some r' -> if r==r' then [r] else [r;r'] in
        CS.declare_new { kind; blockers };
@@ -1808,7 +1812,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
        Fmt.fprintf Fmt.std_formatter "HO unification delayed: %a = %a\n%!"
          (uppterm depth [] ~argsdepth empty_env) a (uppterm depth [] ~argsdepth empty_env) b ;
        let kind = Unification {adepth = adepth+depth; env = e; bdepth = bdepth+depth; a; b; matching} in
-       let blockers = match is_flex (bdepth+depth) other with | None -> [r] | Some r' -> [r;r'] in
+       let blockers = match is_flex ~depth:(bdepth+depth) other with | None -> [r] | Some r' -> [r;r'] in
        CS.declare_new { kind; blockers };
        true
        end else error (error_msg_hard_unif a b)
@@ -1821,7 +1825,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
          (uppterm depth [] ~argsdepth empty_env) a (uppterm depth [] ~argsdepth e) b ;
        let kind = Unification {adepth = adepth+depth; env = e; bdepth = bdepth+depth; a; b; matching} in
        let blockers =
-         match is_flex (adepth+depth) other with
+         match is_flex ~depth:(adepth+depth) other with
          | None -> [r]
          | Some r' -> if r==r' then [r] else [r;r'] in
        CS.declare_new { kind; blockers };
@@ -1864,7 +1868,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
    | _ -> false
    end]
 and eta_contract_heap_or_expand_stack argsdepth matching depth adepth a x bdepth b c args e =
-  match eta_contract_flex depth adepth adepth e a with
+  match eta_contract_flex depth adepth ~argsdepth:adepth e a with
   | Some flex -> unif argsdepth matching depth adepth flex bdepth b e
   | None when c == Global_symbols.uvarc-> false
   | None ->
@@ -1874,7 +1878,7 @@ and eta_contract_heap_or_expand_stack argsdepth matching depth adepth a x bdepth
       let eta = C.mkAppL c (args @ [extra]) in
       unif argsdepth matching (depth+1) adepth x bdepth eta e
 and eta_contract_stack_or_expand_heap argsdepth matching depth adepth a c args bdepth b x e =
-  match eta_contract_flex depth bdepth adepth e b with
+  match eta_contract_flex depth bdepth ~argsdepth:adepth e b with
   | Some flex -> unif argsdepth matching depth adepth a bdepth flex e
   | None when c == Global_symbols.uvarc-> false
   | None ->
@@ -3409,7 +3413,7 @@ let try_fire_rule (gid[@trace]) rule (constraints as orig_constraints) =
         (shift_bound_vars ~depth:0 ~to_:max_depth guard);
     assignments = StrMap.empty;
     initial_depth = max_depth;
-    initial_runtime_state = State.(init (State.descriptor !CS.state) |> State.begin_goal_compilation |> end_goal_compilation StrMap.empty |> end_compilation);
+    initial_runtime_state = !CS.initial_state;
     query_arguments = Query.N;
     symbol_table = !C.table;
     builtins = !FFI.builtins;
@@ -3702,12 +3706,12 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
     | AppUVar ({contents = t}, from, args) when t != C.dummy -> [%spy "user:rule" ~rid ~gid pp_string "deref"]; [%spy "user:rule:deref" ~rid ~gid pp_string "success"];
        [%tcall run depth p (deref_appuv ~from ~to_:depth args t) (gid[@trace]) gs next alts cutto_alts]
     | Const k ->
-       let clauses = get_clauses depth k g p in
+       let clauses = get_clauses ~depth k g p in
        [%spy "user:rule" ~rid ~gid pp_string "backchain"];
        [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
        [%tcall backchain depth p (k, C.dummy, [], gs) (gid[@trace]) next alts cutto_alts clauses]
     | App (k,x,xs) ->
-       let clauses = get_clauses depth k g p in
+       let clauses = get_clauses ~depth k g p in
        [%spy "user:rule" ~rid ~gid pp_string "backchain"];
        [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
        [%tcall backchain depth p (k, x, xs, gs) (gid[@trace]) next alts cutto_alts clauses]
@@ -3753,7 +3757,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
              | arg_mode :: ms -> unif ~argsdepth:depth ~matching:(arg_mode == Input) (gid[@trace]) depth env c_depth arg x && for_all3b3 ~argsdepth:depth (unif (gid[@trace])) depth env c_depth args_of_g xs ms false
         with
         | false ->
-            T.undo old_trail (); [%tcall backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cs]
+            T.undo ~old_trail (); [%tcall backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cs]
         | true ->
            let oldalts = alts in
            let alts = if cs = [] then alts else
@@ -3811,7 +3815,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
       initial_goal = g;
       assignments = StrMap.empty;
       initial_depth = depth;
-      initial_runtime_state = State.(init (State.descriptor !CS.state) |> State.begin_goal_compilation |> end_goal_compilation StrMap.empty |> end_compilation);
+      initial_runtime_state = !CS.initial_state;
       query_arguments = Query.N;
       symbol_table = !C.table;
       builtins = !FFI.builtins;
@@ -3972,6 +3976,7 @@ end;*)
   set delay_hard_unif_problems delay_outside_fragment;
   set steps_made 0;
   set CS.state initial_runtime_state;
+  set CS.initial_state initial_runtime_state;
   set C.table symbol_table;
   set FFI.builtins builtins;
   set rid !max_runtime_id;
diff --git a/tests/sources/is.elpi b/tests/sources/is.elpi
new file mode 100644
index 000000000..5e6ab393f
--- /dev/null
+++ b/tests/sources/is.elpi
@@ -0,0 +1,4 @@
+main :-
+  "ab" is "a" ^ "b",
+  3 is 2 + 1,
+  std.findall (X is 1 + 2) L.
\ No newline at end of file
diff --git a/tests/sources/trace_chr.elab.json b/tests/sources/trace_chr.elab.json
index 0b8b977eb..c84d93c6a 100644
--- a/tests/sources/trace_chr.elab.json
+++ b/tests/sources/trace_chr.elab.json
@@ -1033,7 +1033,7 @@
               {
                 "step_id": 0,
                 "runtime_id": 1,
-                "step": [ "Init", { "goal_text": "odd z", "goal_id": 21 } ],
+                "step": [ "Init", { "goal_text": "odd z", "goal_id": 20 } ],
                 "color": "Grey"
               },
               {
@@ -1042,7 +1042,7 @@
                 "step": [
                   "Inference",
                   {
-                    "current_goal_id": 21,
+                    "current_goal_id": 20,
                     "current_goal_text": "odd z",
                     "current_goal_predicate": "odd",
                     "failed_attempts": [],
@@ -1071,7 +1071,7 @@
                   "step_id": 0,
                   "runtime_id": 2,
                   "step": [
-                    "Init", { "goal_text": "odd (s z)", "goal_id": 23 }
+                    "Init", { "goal_text": "odd (s z)", "goal_id": 21 }
                   ],
                   "color": "Grey"
                 },
@@ -1081,7 +1081,7 @@
                   "step": [
                     "Inference",
                     {
-                      "current_goal_id": 23,
+                      "current_goal_id": 21,
                       "current_goal_text": "odd (s z)",
                       "current_goal_predicate": "odd",
                       "failed_attempts": [],
@@ -1106,7 +1106,7 @@
                             "events": [ [ "Assign", "A0 := z" ] ]
                           },
                           "siblings": [
-                            { "goal_text": "even z", "goal_id": 24 }
+                            { "goal_text": "even z", "goal_id": 22 }
                           ],
                           "siblings_aggregated_outcome": "Success"
                         }
@@ -1143,7 +1143,7 @@
                   "step": [
                     "Inference",
                     {
-                      "current_goal_id": 24,
+                      "current_goal_id": 22,
                       "current_goal_text": "even z",
                       "current_goal_predicate": "even",
                       "failed_attempts": [],
@@ -1219,7 +1219,7 @@
               ]
             },
             "chr_removed_goals": [ 19, 14 ],
-            "chr_new_goals": [ { "goal_text": "_ => fail", "goal_id": 25 } ]
+            "chr_new_goals": [ { "goal_text": "_ => fail", "goal_id": 23 } ]
           }
         ],
         "chr_store_before": [
@@ -1237,7 +1237,7 @@
     "step": [
       "Inference",
       {
-        "current_goal_id": 25,
+        "current_goal_id": 23,
         "current_goal_text": "_ => fail",
         "current_goal_predicate": "=>",
         "failed_attempts": [],
@@ -1247,7 +1247,7 @@
               "rule": [ "BuiltinRule", [ "Logic", "implication" ] ],
               "events": []
             },
-            "siblings": [ { "goal_text": "fail", "goal_id": 26 } ],
+            "siblings": [ { "goal_text": "fail", "goal_id": 24 } ],
             "siblings_aggregated_outcome": "Fail"
           }
         ],
@@ -1269,7 +1269,7 @@
     "step": [
       "Inference",
       {
-        "current_goal_id": 26,
+        "current_goal_id": 24,
         "current_goal_text": "fail",
         "current_goal_predicate": "fail",
         "failed_attempts": [],
diff --git a/tests/sources/trace_chr.json b/tests/sources/trace_chr.json
index 51da5305f..c19d5da4c 100644
--- a/tests/sources/trace_chr.json
+++ b/tests/sources/trace_chr.json
@@ -97,44 +97,44 @@
 {"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 2, column 3, character 25:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]}
 {"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--496 []"]}
-{"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : []}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["fail"]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : []}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["fail"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:rule-failed","payload" : []}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 3, column 3, character 71:"," \\ (even A0) (odd A0) | (odd (s z)) <=> (fail)"]}
 {"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--497 []"]}
-{"step" : 0,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 13, column 0, character 209:"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 13, column 0, character 209:","(odd (s A0)) :- (even A0)."]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 13, column 0, character 209:"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 13, column 0, character 209:","(odd (s A0)) :- (even A0)."]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := z"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:subgoal","payload" : ["24"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["even z"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain","payload" : ["success"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["even","even z"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 11, column 0, character 200:"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 11, column 0, character 200:","(even z) :- ."]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain","payload" : ["success"]}
-{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["25"]}
-{"step" : 14,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["_ => fail"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:subgoal","payload" : ["22"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["even z"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:rule:backchain","payload" : ["success"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["even","even z"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 11, column 0, character 200:"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 11, column 0, character 200:","(even z) :- ."]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 22,"runtime_id" : 2,"name" : "user:rule:backchain","payload" : ["success"]}
+{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["23"]}
+{"step" : 14,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["_ => fail"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:rule-fired","payload" : ["File \"tests/sources/trace_chr.elpi\", line 3, column 3, character 71:"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:rule-remove-constraints","payload" : ["19","14"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:store:before","payload" : ["19"," even X1  /* suspended on X1 */"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:store:before","payload" : ["14"," odd X1  /* suspended on X1 */"]}
-{"step" : 14,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:CHR:resumed","payload" : ["_ => fail"]}
-{"step" : 15,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","_ => fail"]}
-{"step" : 15,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]}
-{"step" : 15,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["26"]}
-{"step" : 15,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail"]}
-{"step" : 15,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule:implication","payload" : ["success"]}
-{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["fail","fail"]}
-{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : []}
-{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["fail"]}
+{"step" : 14,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 0,"name" : "user:CHR:resumed","payload" : ["_ => fail"]}
+{"step" : 15,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","_ => fail"]}
+{"step" : 15,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]}
+{"step" : 15,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["24"]}
+{"step" : 15,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail"]}
+{"step" : 15,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 0,"name" : "user:rule:implication","payload" : ["success"]}
+{"step" : 16,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["fail","fail"]}
+{"step" : 16,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 16,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : []}
+{"step" : 16,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["fail"]}
 {"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["not","not (even X1)"]}
 {"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
 {"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 54, column 0, character 631:"]}
diff --git a/tests/sources/trace_findall.elab.json b/tests/sources/trace_findall.elab.json
index ffd0d5c88..c1770ba38 100644
--- a/tests/sources/trace_findall.elab.json
+++ b/tests/sources/trace_findall.elab.json
@@ -163,7 +163,7 @@
           {
             "step_id": 0,
             "runtime_id": 1,
-            "step": [ "Init", { "goal_text": "p X0", "goal_id": 9 } ],
+            "step": [ "Init", { "goal_text": "p X0", "goal_id": 8 } ],
             "color": "Grey"
           },
           {
@@ -172,7 +172,7 @@
             "step": [
               "Inference",
               {
-                "current_goal_id": 9,
+                "current_goal_id": 8,
                 "current_goal_text": "p X0",
                 "current_goal_predicate": "p",
                 "failed_attempts": [],
@@ -232,7 +232,7 @@
             "step": [
               "Inference",
               {
-                "current_goal_id": 9,
+                "current_goal_id": 8,
                 "current_goal_text": "p X0",
                 "current_goal_predicate": "p",
                 "failed_attempts": [],
@@ -292,7 +292,7 @@
             "step": [
               "Inference",
               {
-                "current_goal_id": 9,
+                "current_goal_id": 8,
                 "current_goal_text": "p X0",
                 "current_goal_predicate": "p",
                 "failed_attempts": [],
@@ -316,7 +316,7 @@
                       ],
                       "events": [ [ "Assign", "X0 := 3" ] ]
                     },
-                    "siblings": [ { "goal_text": "p 2", "goal_id": 10 } ],
+                    "siblings": [ { "goal_text": "p 2", "goal_id": 9 } ],
                     "siblings_aggregated_outcome": "Success"
                   }
                 ],
@@ -352,7 +352,7 @@
             "step": [
               "Inference",
               {
-                "current_goal_id": 10,
+                "current_goal_id": 9,
                 "current_goal_text": "p 2",
                 "current_goal_predicate": "p",
                 "failed_attempts": [],
diff --git a/tests/sources/trace_findall.json b/tests/sources/trace_findall.json
index fddbf78f8..ca6c135f3 100644
--- a/tests/sources/trace_findall.json
+++ b/tests/sources/trace_findall.json
@@ -19,32 +19,32 @@
 {"step" : 2,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]}
 {"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["findall_solutions","findall_solutions (p _) X0"]}
 {"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["findall"]}
-{"step" : 0,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["p X0"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 1, column 0, character 0:","File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 1, column 0, character 0:","(p 1) :- ."]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["p X0"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 1, column 0, character 0:","File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 1, column 0, character 0:","(p 1) :- ."]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X0 := 1"]}
-{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","(p 2) :- ."]}
+{"step" : 1,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","(p 2) :- ."]}
 {"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X0 := 2"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:","(p 3) :- (p 2)."]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:","(p 3) :- (p 2)."]}
 {"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X0 := 3"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:subgoal","payload" : ["10"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["p 2"]}
-{"step" : 3,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
-{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p 2"]}
-{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:"]}
-{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","(p 2) :- ."]}
-{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 1,"name" : "user:subgoal","payload" : ["9"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["p 2"]}
+{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
+{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p 2"]}
+{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
+{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:"]}
+{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","(p 2) :- ."]}
+{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]}
 {"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X0 := [p 1, p 2, p 3]"]}
 {"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:findall","payload" : ["success"]}
 {"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["print","print [p 1, p 2, p 3]"]}
diff --git a/tests/suite/correctness_FO.ml b/tests/suite/correctness_FO.ml
index e3c08ad4d..4f33ae95f 100644
--- a/tests/suite/correctness_FO.ml
+++ b/tests/suite/correctness_FO.ml
@@ -126,3 +126,7 @@ let () = declare "dt_var2"
   ~expectation:(SuccessOutput (Str.regexp "dev:disc-tree:candidates = 3"))
   ()
 
+let () = declare "is"
+  ~source_elpi:"is.elpi"
+  ~description:"calc"
+  ()