diff --git a/src/core/check.ml b/src/core/check.ml
index 784821f4a..44ae2235b 100644
--- a/src/core/check.ml
+++ b/src/core/check.ml
@@ -169,7 +169,7 @@ module Comp = struct
          Id.print name
 
     | NotRecursiveDst name ->
-       fprintf ppf "A recursive call to nonrecursive fucntion %a is forbidden."
+       fprintf ppf "A recursive call to nonrecursive function %a is forbidden."
          Id.print name
 
     | IllegalParamTyp (cD, cPsi, tA) ->
diff --git a/src/core/check.mli b/src/core/check.mli
index 6554090ec..88a0fd827 100644
--- a/src/core/check.mli
+++ b/src/core/check.mli
@@ -2,6 +2,7 @@
    @author Brigitte Pientka
    modified: Joshua Dunfield
 *)
+open Support
 
 module LF : sig
 
@@ -25,15 +26,15 @@ module LF : sig
       of mctx
          * dctx (* expected *)
          * dctx_hat (* found *)
-         * (Loc.t * mfront)
+         * (Location.t * mfront)
     | IllTypedMetaObj of mctx * clobj * dctx * cltyp
     | TermWhenVar of mctx * dctx * normal
     | SubWhenRen of mctx * dctx * sub
     | MissingType of string
 
-  exception Error of Loc.t * error
+  exception Error of Location.t * error
 
-  val throw : Loc.t -> error -> 'a
+  val throw : Location.t -> error -> 'a
 
   val check : mctx -> dctx -> nclo -> tclo -> unit
 
@@ -43,7 +44,7 @@ module LF : sig
   val checkDCtx : mctx -> dctx -> unit
 
   val checkSchemaWf : schema -> unit
-  val checkSchema : Loc.t -> mctx -> dctx -> Id.name -> schema -> unit
+  val checkSchema : Location.t -> mctx -> dctx -> Id.name -> schema -> unit
   val subsumes : mctx -> ctx_var -> ctx_var -> bool
 
   (** Checks that a type exists within a given schema.
@@ -54,12 +55,12 @@ module LF : sig
       The input name will be a part of the error message, and should
       be the declared name of the schema.
    *)
-  val checkTypeAgainstSchema: Syntax.Loc.t -> mctx -> dctx -> typ -> Id.name -> sch_elem list
+  val checkTypeAgainstSchema: Location.t -> mctx -> dctx -> typ -> Id.name -> sch_elem list
                               -> typ_rec * sub
   val instanceOfSchElem : mctx -> dctx -> tclo -> sch_elem -> (typ_rec * sub)
   val instanceOfSchElemProj : mctx -> dctx -> tclo -> (head * int) -> sch_elem -> (typ_rec * sub)
 
-  val checkMSub : Loc.t -> mctx -> msub -> mctx -> unit
+  val checkMSub : Location.t -> mctx -> msub -> mctx -> unit
 
 end
 
@@ -120,10 +121,10 @@ module Comp : sig
          * int (* premise index *)
          * suffices_typ (* given type annotation *)
 
-  exception Error of Loc.t * error
+  exception Error of Location.t * error
 
   (** Raises an error from this module. *)
-  val throw : Loc.t -> error -> 'a
+  val throw : Location.t -> error -> 'a
 
   (** Appends two sets of hypotheses.
       Appropriately MShifts the left contexts and applies an
@@ -153,7 +154,7 @@ module Comp : sig
       plicity and type information from the context on the left, but
       the entry name from the context on the right.
    *)
-  val validate_contexts : Loc.t -> LF.mctx * LF.mctx -> gctx * gctx -> LF.mctx * gctx
+  val validate_contexts : Location.t -> LF.mctx * LF.mctx -> gctx * gctx -> LF.mctx * gctx
 
   (** Checks a theorem in the given contexts against the given type.
       The given list of total declarations is used for totality checking.
@@ -249,7 +250,7 @@ module Comp : sig
       else, raises a synthesis mismatch error for the expression i
       saying that the type of i is expected to be a box-type.
    *)
-  val require_syn_typbox : LF.mctx -> gctx -> Loc.t -> exp_syn -> tclo -> meta_typ * LF.msub
+  val require_syn_typbox : LF.mctx -> gctx -> Location.t -> exp_syn -> tclo -> meta_typ * LF.msub
 
 
   (** Processes all leading PiBoxes to replace them with unification
@@ -296,7 +297,7 @@ module Comp : sig
 
       The provided location is used when raising errors.
    *)
-  val unify_suffices : Loc.t -> LF.mctx
+  val unify_suffices : Location.t -> LF.mctx
                        -> typ (* scrutinee type; to be decomposed *)
                        -> suffices_typ list (* type annotations *)
                        -> typ (* goal type; to match against
@@ -309,5 +310,5 @@ module Comp : sig
       the type (together with a delayed meta-substitution) of the
       produced expression.
    *)
-  val genMApp : Loc.t -> (LF.ctyp_decl -> bool) -> LF.mctx -> exp_syn * tclo -> int * (exp_syn * tclo)
+  val genMApp : Location.t -> (LF.ctyp_decl -> bool) -> LF.mctx -> exp_syn * tclo -> int * (exp_syn * tclo)
 end
diff --git a/src/core/command.ml b/src/core/command.ml
index 1d4f38ba1..f565a5c6f 100644
--- a/src/core/command.ml
+++ b/src/core/command.ml
@@ -450,7 +450,11 @@ let printfun =
                ; thm_loc = Syntax.Loc.ghost
                }
              in
-             P.fmt_ppr_sgn_decl ppf (Synint.Sgn.Theorem [d])
+             P.fmt_ppr_sgn_decl ppf
+              (Synint.Sgn.Theorem
+                { location=Syntax.Loc.ghost
+                ; theorems=Nonempty.singleton d
+                })
           | _  -> fprintf ppf "- %s is not a function.;\n@?" arg
         with
         | Not_found ->
@@ -475,7 +479,7 @@ let query =
       begin fun ppf arglist ->
       try
         begin
-          let [Synext.Sgn.Query (_, name, extT, expected, tries)] =
+          let [Synext.Sgn.Query { name; typ=extT; expected_solutions=expected; maximum_tries=tries; _ }] =
             let expected = List.hd arglist in
             let tries = List.hd (List.tl arglist) in
             let str = String.concat " " (List.tl (List.tl arglist)) in
diff --git a/src/core/coverage.ml b/src/core/coverage.ml
index 337eebc8e..277f6c50a 100644
--- a/src/core/coverage.ml
+++ b/src/core/coverage.ml
@@ -1274,7 +1274,7 @@ let genObj (cD, cPsi, tP) (tH, tA, k) =
        end;
      Some (cD', (cPsi', tR', (tP', S.LF.id)), ms')
 
-let genAllObj cg = Option.filter_map (genObj cg)
+let genAllObj cg = List.filter_map (genObj cg)
 
 let genConst (cD, cPsi, (a, tS)) =
   Types.freeze a;
@@ -2520,7 +2520,7 @@ let genPatt names mk_pat_var (cD_p, tau_v) (c, tau_c) =
      raise e
 
 let genAllPatt names mk_pat_var ((cD_v, tau_v) : LF.mctx * Comp.typ) =
-  Option.filter_map
+  List.filter_map
     begin fun (c, tau_c) ->
     genPatt names mk_pat_var (cD_v, tau_v) (c, tau_c)
     end
diff --git a/src/core/holes.mli b/src/core/holes.mli
index c5e51d5a1..189e8c3fb 100644
--- a/src/core/holes.mli
+++ b/src/core/holes.mli
@@ -1,3 +1,4 @@
+open Support
 open Syntax.Int
 
 (* Define two opaque types to be used as indices for `hole_info`. *)
@@ -20,7 +21,7 @@ type _ hole_info =
 
 (** A hole with a known kind of information. *)
 type 'a hole =
-  { loc : Syntax.Loc.t
+  { loc : Location.t
   ; name : HoleId.name
     (** "Context Delta", for metavariables. *)
   ; cD : LF.mctx
@@ -41,11 +42,11 @@ val string_of_lookup_strategy : lookup_strategy -> string
 type error =
   | InvalidHoleIdentifier of string
   | NoSuchHole of lookup_strategy
-  | NameShadowing of string * Loc.t
+  | NameShadowing of string * Location.t
   | UnsolvedHole of HoleId.name * HoleId.t
 
 (** An error that arises when lookup by a given strategy fails. *)
-exception Error of Loc.t * error
+exception Error of Location.t * error
 
 (** Parses a lookup strategy.
  * An integer gives the `by_id` strategy, whereas a non-integer gives
@@ -56,7 +57,7 @@ val parse_lookup_strategy : string -> lookup_strategy option
 (** Parses a lookup strategy, throwing an exception on failure.
     The given location is used in the thrown exception.
  *)
-val unsafe_parse_lookup_strategy : Loc.t -> string -> lookup_strategy
+val unsafe_parse_lookup_strategy : Location.t -> string -> lookup_strategy
 
 (** Looks up a hole by its number.
   * Use strategies with `get`. *)
@@ -111,13 +112,13 @@ val unsafe_get : lookup_strategy -> HoleId.t * some_hole
 val lookup : string -> (HoleId.t * some_hole) option
 
 (** Decides whether a location is contained within a location. *)
-val loc_within : Syntax.Loc.t -> Syntax.Loc.t -> bool
+val loc_within : Location.t -> Location.t -> bool
 
 (** Counts the number of holes. *)
 val count : unit -> int
 
 (** Removes all holes contained in the given location. *)
-val destroy_holes_within : Syntax.Loc.t -> unit
+val destroy_holes_within : Location.t -> unit
 
 (** Allocates a new hole ID. *)
 val allocate : unit -> HoleId.t
@@ -135,7 +136,7 @@ val clear : unit -> unit
 val list : unit -> (HoleId.t * some_hole) list
 
 (** Adds a Harpoon subgoal to the internal list. *)
-val add_harpoon_subgoal : Loc.t * Comp.open_subgoal -> unit
+val add_harpoon_subgoal : Location.t * Comp.open_subgoal -> unit
 
 (** Gets the list of Harpoon subgoals. *)
-val get_harpoon_subgoals : unit -> (Loc.t * Comp.open_subgoal) list
+val get_harpoon_subgoals : unit -> (Location.t * Comp.open_subgoal) list
diff --git a/src/core/id.ml b/src/core/id.ml
index e7d53865b..6d2ee959a 100644
--- a/src/core/id.ml
+++ b/src/core/id.ml
@@ -95,12 +95,12 @@ let gen_fresh_name (ns : name list) (n : name) : name =
     else y
   in
   let cnts =
-    let open Option in
-    filter_map
+    List.filter_map
       begin fun n' ->
-      String.equal n'.hint_name n.hint_name
-      |> of_bool
-      $> Fun.const n'.hint_cnt
+        let open Option in
+        String.equal n'.hint_name n.hint_name
+        |> of_bool
+        $> Fun.const n'.hint_cnt
       end
       ns
   in
diff --git a/src/core/parser.ml b/src/core/parser.ml
index e048c7488..f8967baf1 100644
--- a/src/core/parser.ml
+++ b/src/core/parser.ml
@@ -863,11 +863,11 @@ let check_datatype_decl loc a cs : unit parser =
   in
   traverse_
     (function
-     | Sgn.CompConst (_, c, tau) ->
-        retname tau
+     | Sgn.CompConst { identifier; typ; _ } ->
+        retname typ
         $ fun a' ->
           if not (Id.equals a a')
-          then fail (WrongConstructorType (c, a, a'))
+          then fail (WrongConstructorType (identifier, a, a'))
           else pure ()
      | _ -> fail (Violation "check_datatype_decl invalid input"))
     cs
@@ -880,11 +880,11 @@ let check_codatatype_decl loc a cs : unit parser =
   in
   traverse_
     (function
-     | Sgn.CompDest (_, c, _, tau0, _) ->
+     | Sgn.CompDest { identifier; observation_typ=tau0; _} ->
         retname tau0
         $ fun a' ->
           if not (Id.equals a a')
-          then fail (WrongConstructorType (c, a, a'))
+          then fail (WrongConstructorType (identifier, a, a'))
           else pure ()
      | _ -> fail (Violation "check_codatatype_decl invalid input"))
     cs
@@ -1095,8 +1095,8 @@ let only p = p <& eoi
 open Syntax.Ext
 
 let sgn_global_prag : Sgn.decl parser =
-  let g s = span (pragma (s)) in
-  let f prag (loc, _) = Sgn.GlobalPragma (loc, prag) in
+  let g s = span (pragma s) in
+  let f pragma (location, _) = Sgn.GlobalPragma { location; pragma } in
   let h s a = g s $> f a in
   labelled "global pragma"
     begin
@@ -1114,8 +1114,8 @@ let sgn_name_pragma : Sgn.decl parser =
     (maybe identifier <& token T.DOT)
   |> labelled "name pragma"
   |> span
-  $> fun (loc, (w, mv, x)) ->
-     Sgn.Pragma (loc, Sgn.NamePrag (w, mv, x))
+  $> fun (location, (w, mv, x)) ->
+     Sgn.Pragma { location; pragma=Sgn.NamePrag (w, mv, x) }
 
 (** Parses the `type' kind. *)
 let type_kind =
@@ -1314,8 +1314,8 @@ let lf_const_decl (* sgn_lf_typ *) =
        (name <& token T.COLON)
        lf_typ
      |> span
-     $ fun (loc, (id, tA)) ->
-       pure (Sgn.Const (loc, id, tA)))
+     $ fun (location, (identifier, typ)) ->
+       pure (Sgn.Const { location; identifier; typ }))
 
 let sgn_lf_typ_decl : Sgn.decl parser =
   let lf_typ_decl_body (* cmp_dat *) =
@@ -1329,18 +1329,17 @@ let sgn_lf_typ_decl : Sgn.decl parser =
       (maybe (token T.PIPE)
        &> sep_by0 lf_const_decl (token (T.PIPE)))
     |> span
-    $> fun (loc, ((a, k), const_decls)) ->
-       Sgn.Typ (loc, a, k), const_decls
+    $> fun (location, ((identifier, kind), const_decls)) ->
+       Sgn.Typ { location; identifier; kind }, const_decls
   in
 
   labelled "LF type declaration block"
     (token T.KW_LF
-     &> (sep_by1 lf_typ_decl_body (token T.KW_AND)
-         $> Nonempty.to_list)
+     &> (sep_by1 lf_typ_decl_body (token T.KW_AND))
      <& token T.SEMICOLON
      |> span
-     $> fun (loc, f) ->
-        Sgn.MRecTyp (loc, f))
+     $> fun (location, declarations) ->
+        Sgn.MRecTyp { location; declarations })
 
   (*
 let ctyp_decl, implicit_ctyp_decl =
@@ -2588,8 +2587,8 @@ let sgn_cmp_typ_decl =
             (name <& token (T.COLON))
             cmp_typ
           |> span
-          $> fun (loc, (x, tau)) ->
-             Sgn.CompConst (loc, x, tau)
+          $> fun (location, (identifier, typ)) ->
+             Sgn.CompConst { location; identifier; typ }
         in
         seq5
           flavour
@@ -2598,10 +2597,10 @@ let sgn_cmp_typ_decl =
           (sep_by0 sgn_cmp_typ_decl_body (token T.PIPE))
           get_state
         |> span
-        $ fun (loc, (flavour, name, kind, decls, s)) ->
-          check_datatype_decl loc name decls
+        $ fun (location, (datatype_flavour, identifier, kind, decls, s)) ->
+          check_datatype_decl location identifier decls
           $> fun () ->
-             Sgn.CompTyp (loc, name, kind, flavour), decls
+             Sgn.CompTyp { location; identifier; kind; datatype_flavour }, decls
       in
       let cmp_cotyp_decl =
         let cmp_cotyp_body =
@@ -2629,9 +2628,14 @@ let sgn_cmp_typ_decl =
              <& token T.DOUBLE_COLON)
             cmp_typ
           |> span
-          $> fun (loc, ((* cD, *) (a, tau0), tau1)) ->
-             Sgn.CompDest (loc, a, (* cD, *) LF.Empty, tau0, tau1)
-
+          $> fun (location, ((* cD, *) (identifier, tau0), tau1)) ->
+             Sgn.CompDest
+              { location
+              ; identifier
+              ; mctx=LF.Empty
+              ; observation_typ=tau0
+              ; return_typ=tau1
+              }
         in
         seq4
           (token T.KW_COINDUCTIVE &> name <& token T.COLON)
@@ -2639,17 +2643,16 @@ let sgn_cmp_typ_decl =
           (sep_by0 cmp_cotyp_body (token T.PIPE))
           get_state
         |> span
-        $ fun (loc, (a, k, decls, s)) ->
-          check_codatatype_decl loc a decls
+        $ fun (location, (identifier, kind, decls, s)) ->
+          check_codatatype_decl location identifier decls
           $> fun () ->
-             Sgn.CompCotyp (loc, a, k), decls
+             Sgn.CompCotyp { location; identifier; kind }, decls
       in
 
       sep_by1 (alt cmp_typ_decl cmp_cotyp_decl) (token T.KW_AND)
-      $> Nonempty.to_list
       <& token T.SEMICOLON
       |> span
-      $> fun (loc, ds) -> Sgn.MRecTyp (loc, ds)
+      $> fun (location, declarations) -> Sgn.MRecTyp { location; declarations }
     end
 
 let sgn_query_pragma =
@@ -2667,8 +2670,8 @@ let sgn_query_pragma =
   <& token T.DOT
   |> span
   |> labelled "logic programming engine query pragma"
-  $> fun (loc, ((e, t), x, a)) ->
-     Sgn.Query (loc, x, a, e, t)
+  $> fun (location, ((expected_solutions, maximum_tries), name, typ)) ->
+     Sgn.Query { location; name; typ; expected_solutions; maximum_tries }
 
 let sgn_oldstyle_lf_decl =
   labelled
@@ -2678,16 +2681,16 @@ let sgn_oldstyle_lf_decl =
         (name <& token T.COLON)
         (lf_kind_or_typ <& token T.DOT)
       |> span
-      $> fun (loc, (a_or_c, k_or_a)) ->
+      $> fun (location, (identifier, k_or_a)) ->
          match k_or_a with
-         | `Kind k -> Sgn.Typ (loc, a_or_c, k)
-         | `Typ a -> Sgn.Const (loc, a_or_c, a)
+         | `Kind kind -> Sgn.Typ { location; identifier; kind }
+         | `Typ typ -> Sgn.Const { location; identifier; typ }
     end
 
 let sgn_not_pragma : Sgn.decl parser =
   pragma "not"
   |> span
-  $> fun (loc, _) -> Sgn.Pragma (loc, Sgn.NotPrag)
+  $> fun (location, _) -> Sgn.Pragma { location; pragma=Sgn.NotPrag }
 
 let associativity =
   [ "left", Sgn.Left
@@ -2703,16 +2706,22 @@ let sgn_fixity_pragma : Sgn.decl parser =
     &> seq3 name integer (maybe associativity)
     <& token T.DOT
     |> span
-    $> fun (loc, (x, precedence, assoc)) ->
-       Sgn.Pragma (loc, Sgn.FixPrag (x, Sgn.Infix, precedence, assoc))
+    $> fun (location, (x, precedence, assoc)) ->
+       Sgn.Pragma
+       { location
+       ; pragma=Sgn.FixPrag (x, Sgn.Infix, precedence, assoc)
+       }
   in
   let prefix_pragma : Sgn.decl parser =
     pragma "prefix"
     &> seq2 name integer
     <& token T.DOT
     |> span
-    $> fun (loc, (x, precedence)) ->
-       Sgn.Pragma (loc, Sgn.FixPrag (x, Sgn.Prefix, precedence, Some Sgn.Left))
+    $> fun (location, (x, precedence)) ->
+       Sgn.Pragma
+       { location
+       ; pragma=Sgn.FixPrag (x, Sgn.Prefix, precedence, Some Sgn.Left)
+       }
   in
   alt infix_pragma prefix_pragma
 
@@ -2721,7 +2730,8 @@ let sgn_associativity_pragma : Sgn.decl parser =
   &> associativity
   <& token T.DOT
   |> span
-  $> fun (loc, assoc) -> Sgn.Pragma (loc, Sgn.DefaultAssocPrag assoc)
+  $> fun (location, assoc) ->
+    Sgn.Pragma { location; pragma=Sgn.DefaultAssocPrag assoc}
 
 let sgn_open_pragma : Sgn.decl parser =
   pragma "open"
@@ -2729,8 +2739,8 @@ let sgn_open_pragma : Sgn.decl parser =
   |> span
   |> labelled "open pragma"
   <& token T.DOT
-  $> fun (loc, id) ->
-     Sgn.Pragma (loc, Sgn.OpenPrag (Nonempty.to_list id))
+  $> fun (location, id) ->
+     Sgn.Pragma { location; pragma=Sgn.OpenPrag (Nonempty.to_list id) }
 
 let sgn_abbrev_pragma : Sgn.decl parser =
   pragma "abbrev"
@@ -2738,9 +2748,9 @@ let sgn_abbrev_pragma : Sgn.decl parser =
   <& token T.DOT
   |> span
   |> labelled "module abbreviation pragma"
-  $> fun (loc, (fq, x)) ->
+  $> fun (location, (fq, x)) ->
      let fq = Nonempty.to_list fq in
-     Sgn.Pragma (loc, Sgn.AbbrevPrag (fq, x))
+     Sgn.Pragma { location; pragma=Sgn.AbbrevPrag (fq, x) }
 
 let sgn_comment : Sgn.decl parser =
   satisfy' `html_comment
@@ -2749,7 +2759,7 @@ let sgn_comment : Sgn.decl parser =
      | _ -> None)
   |> span
   |> labelled "HTML comment"
-  $> fun (loc, s) -> Sgn.Comment (loc, s)
+  $> fun (location, content) -> Sgn.Comment { location; content }
 
 let sgn_typedef_decl : Sgn.decl parser =
   seq3
@@ -2758,8 +2768,8 @@ let sgn_typedef_decl : Sgn.decl parser =
     (token T.EQUALS &> cmp_typ <& token T.SEMICOLON)
   |> span
   |> labelled "type synonym declaration"
-  $> fun (loc, (x, k, tau)) ->
-     Sgn.CompTypAbbrev (loc, x, k, tau)
+  $> fun (location, (identifier, kind, typ)) ->
+     Sgn.CompTypAbbrev { location; identifier; kind; typ }
 
 let lf_schema_some : LF.typ_decl LF.ctx parser =
   alt
@@ -2804,8 +2814,8 @@ let sgn_schema_decl : Sgn.decl parser =
   <& token T.SEMICOLON
   |> span
   |> labelled "schema declaration"
-  $> fun (loc, (x, bs)) ->
-     Sgn.Schema (loc, x, LF.Schema bs)
+  $> fun (location, (identifier, bs)) ->
+     Sgn.Schema { location; identifier; schema=LF.Schema bs }
 
 let sgn_let_decl : Sgn.decl parser =
   seq2
@@ -2816,8 +2826,8 @@ let sgn_let_decl : Sgn.decl parser =
     (token T.EQUALS &> cmp_exp_syn <& token T.SEMICOLON)
   |> span
   |> labelled "value declaration"
-  $> fun (loc, ((x, tau), i)) ->
-     Sgn.Val (loc, x, tau, i)
+  $> fun (location, ((identifier, typ), expression)) ->
+     Sgn.Val { location; identifier; typ; expression }
 
 let boxity =
   choice
@@ -3033,11 +3043,10 @@ let sgn_thm_decl : Sgn.decl parser =
   sep_by1
     (choice [program_decl; proof_decl])
     (token T.KW_AND)
-  $> Nonempty.to_list
   <& token T.SEMICOLON
   |> span
   |> labelled "(mutual) recursive function declaration(s)"
-  $> fun (loc, f) -> Sgn.Theorem (loc, f)
+  $> fun (location, theorems) -> Sgn.Theorem { location; theorems }
 
 let rec sgn_decl : Sgn.decl parser =
   { run =
@@ -3067,7 +3076,6 @@ let rec sgn_decl : Sgn.decl parser =
           (* term declarations *)
           ; sgn_let_decl
           ; sgn_thm_decl
-          ; sgn_module_decl
           ]
         |> labelled "top-level declaration"
       in
@@ -3084,8 +3092,8 @@ and sgn_module_decl : Sgn.decl parser =
         <& T.(tokens [KW_END; SEMICOLON])
         |> span
         |> labelled "module declaration"
-        $> fun (loc, (x, decls)) ->
-           Sgn.Module (loc, x, decls)
+        $> fun (location, (identifier, declarations)) ->
+           Sgn.Module { location; identifier; declarations }
       in
       p.run s
   }
@@ -3201,7 +3209,8 @@ let interactive_harpoon_command =
     in
     keyword "rename"
     &> seq3 level name name
-    $> fun (level, x_src, x_dst) -> H.Rename (x_src, x_dst, level)
+    $> fun (level, rename_from, rename_to) ->
+      H.Rename { rename_from; rename_to; level }
   in
   let basic_command =
     choice
diff --git a/src/core/prettyext.ml b/src/core/prettyext.ml
index 0621b1241..919a990ce 100644
--- a/src/core/prettyext.ml
+++ b/src/core/prettyext.ml
@@ -862,87 +862,96 @@ module Make (_ : Store.Cid.RENDERER) : Printer.Ext.T = struct
 
   let fmt_ppr_mrec prefix lvl ppf =
     function
-    | Sgn.Typ (_, n, kA) ->
+    | Sgn.Typ { identifier; kind; _ } ->
        fprintf ppf "%s %s : %a = "
          (to_html prefix Keyword)
-         (to_html (Id.render_name n) (ID Typ))
-         (fmt_ppr_lf_kind 0) kA
-    | Sgn.Const (_, n, tA) ->
+         (to_html (Id.render_name identifier) (ID Typ))
+         (fmt_ppr_lf_kind 0) kind
+    | Sgn.Const { identifier; typ; _ } ->
        fprintf ppf "@\n| %s : %a"
-         (to_html (Id.render_name n) (ID Constructor))
-         (fmt_ppr_lf_typ 0)  tA
-    | Sgn.CompTyp (_, n, kA, _)
-      | Sgn.CompCotyp (_, n, kA) ->
+         (to_html (Id.render_name identifier) (ID Constructor))
+         (fmt_ppr_lf_typ 0)  typ
+    | Sgn.CompTyp { identifier; kind; _ }
+      | Sgn.CompCotyp { identifier; kind; _ } ->
        fprintf ppf "%s %s : %a = "
          (to_html prefix Keyword)
-         (to_html (Id.render_name n) (ID Typ))
-         (fmt_ppr_cmp_kind 1) kA
-    | Sgn.CompConst (_, n, tA) ->
+         (to_html (Id.render_name identifier) (ID Typ))
+         (fmt_ppr_cmp_kind 1) kind
+    | Sgn.CompConst { identifier; typ; _ } ->
        fprintf ppf "@\n| %s : %a"
-         (to_html (Id.render_name n) (ID Constructor))
-         (fmt_ppr_cmp_typ 1)  tA
-    | Sgn.CompDest (_, n, cD, tA, tA') ->
+         (to_html (Id.render_name identifier) (ID Constructor))
+         (fmt_ppr_cmp_typ 1)  typ
+    | Sgn.CompDest
+      { identifier
+      ; mctx=cD
+      ; observation_typ=tA
+      ; return_typ=tA'
+      ; _
+      } ->
        fprintf ppf "@\n| (%s : %a) :: %a"
-         (to_html (Id.render_name n) (ID Constructor))
-         (fmt_ppr_cmp_typ 1)  tA
-         (fmt_ppr_cmp_typ 1)  tA'
+         (to_html (Id.render_name identifier) (ID Constructor))
+         (fmt_ppr_cmp_typ 1) tA
+         (fmt_ppr_cmp_typ 1) tA'
     | _ -> ()
 
   (* TODO: Refactor this *)
   let fl_to_prefix =
     function
-    | Sgn.CompTyp (_, _, _, _) -> "inductive"
-    | Sgn.CompCotyp (_, _, _) -> "coinductive"
-    | Sgn.Typ (_, _, _) -> "LF"
+    | Sgn.CompTyp _ -> "inductive"
+    | Sgn.CompCotyp _ -> "coinductive"
+    | Sgn.Typ _ -> "LF"
 
   let fmt_ppr_mrec' lvl ppf (k, body) =
     fmt_ppr_mrec (fl_to_prefix k) lvl ppf k;
     List.iter (fun d -> fmt_ppr_mrec "" lvl ppf d) body
 
-  let rec fmt_ppr_mrecs lvl ppf =
-    function
-    | [h] -> fmt_ppr_mrec' lvl ppf h; fprintf ppf ";@\n"
-    | h :: t -> fmt_ppr_mrec' lvl ppf h;
-              fprintf ppf "@\n%s " (to_html "and" Keyword);
-              fmt_ppr_mrecs lvl ppf t
+  let fmt_ppr_mrecs lvl ppf =
+    Nonempty.destructure (fun h t ->
+      fmt_ppr_mrec' lvl ppf h;
+      t |> List.iter (fun e ->
+        fprintf ppf "@\n%s " (to_html "and" Keyword);
+        fmt_ppr_mrec' lvl ppf e
+      );
+      fprintf ppf ";@\n"
+    )
 
   let rec fmt_ppr_sgn_decl ppf =
     function
-    | Sgn.Const (_, x, a) ->
+    | Sgn.Const { identifier; typ; _ } ->
        fprintf ppf "@[<h>%s : %a.@]@\n"
-         (to_html (Id.render_name x) (ID Constructor))
-         (fmt_ppr_lf_typ l0)  a
+         (to_html (Id.render_name identifier) (ID Constructor))
+         (fmt_ppr_lf_typ l0) typ
 
-    | Sgn.Typ (_, x, k) ->
+    | Sgn.Typ { identifier; kind; _ } ->
        fprintf ppf "@[<h>%s : %a.@]@\n"
-         (to_html (Id.render_name x) (ID Typ))
-         (fmt_ppr_lf_kind l0) k
+         (to_html (Id.render_name identifier) (ID Typ))
+         (fmt_ppr_lf_kind l0) kind
 
-    | Sgn.CompConst (_, x, a) ->
+    | Sgn.CompConst { identifier; typ; _ } ->
        fprintf ppf "@[<h>| %s : %a@]@\n"
-         (to_html (Id.render_name x) (ID Constructor))
-         (fmt_ppr_cmp_typ l0)  a
+         (to_html (Id.render_name identifier) (ID Constructor))
+         (fmt_ppr_cmp_typ l0) typ
 
-    | Sgn.CompTypAbbrev (_, x, k, a) ->
+    | Sgn.CompTypAbbrev { identifier; kind; typ; _ } ->
        fprintf ppf "@[<v>%s %s : %a =@ %a;@]@\n"
          (to_html "datatype" Keyword)
-         (Id.render_name  x)
-         (fmt_ppr_cmp_kind 0) k
-         (fmt_ppr_cmp_typ 0)  a
+         (Id.render_name  identifier)
+         (fmt_ppr_cmp_kind 0) kind
+         (fmt_ppr_cmp_typ 0) typ
 
-    | Sgn.CompTyp (_, x, k, _) ->
+    | Sgn.CompTyp { identifier; kind; _ } ->
        fprintf ppf "@[<v>%s %s : %a = @]@\n"
          (to_html "datatype" Keyword)
-         (to_html (Id.render_name x) (ID Typ))
-         (fmt_ppr_cmp_kind 0) k
+         (to_html (Id.render_name identifier) (ID Typ))
+         (fmt_ppr_cmp_kind 0) kind
 
-    | Sgn.Schema (_, x, schema) ->
+    | Sgn.Schema { identifier; schema; _ } ->
        fprintf ppf "@[<h>%s %s = %a;@]@\n"
          (to_html "schema" Keyword)
-         (to_html (Id.render_name  x) (ID Schema))
+         (to_html (Id.render_name  identifier) (ID Schema))
          (fmt_ppr_lf_schema 0) schema
 
-    | Sgn.Pragma (_, Sgn.NamePrag (name, s, s_opt)) ->
+    | Sgn.Pragma { pragma=Sgn.NamePrag (name, s, s_opt); _ } ->
        fprintf ppf "@[<h>%s %s %s %s@]@\n"
          (to_html "%name" Keyword)
          (Id.render_name name)
@@ -952,29 +961,34 @@ module Make (_ : Store.Cid.RENDERER) : Printer.Ext.T = struct
          | Some x -> x
          end
 
-    | Sgn.Val (_, x, None, i) ->
+    | Sgn.Val { identifier; typ=None; expression; _ } ->
        fprintf ppf "@[%s %s = %a;@]@\n"
          (to_html "let" Keyword)
-         (Id.render_name  x)
-         (fmt_ppr_cmp_exp_syn l0) i
+         (Id.render_name  identifier)
+         (fmt_ppr_cmp_exp_syn l0) expression
 
-    | Sgn.Val (_, x, Some tA, i) ->
+    | Sgn.Val { identifier; typ=Some typ; expression; _ } ->
        fprintf ppf "@[%s %s : %a =@ %a;@]@\n"
          (to_html "let" Keyword)
-         (Id.render_name  x)
-         (fmt_ppr_cmp_typ 0) tA
-         (fmt_ppr_cmp_exp_syn l0) i
+         (Id.render_name  identifier)
+         (fmt_ppr_cmp_typ 0) typ
+         (fmt_ppr_cmp_exp_syn l0) expression
 
     | Sgn.Query _ ->
        fprintf ppf "%s"
          (to_html "query" Keyword)
 
-    | Sgn.Module (_, name, decls) ->
-       let aux ppf t = List.iter (fmt_ppr_sgn_decl ppf) t in
+    | Sgn.Module { identifier; declarations; _ } ->
+       let aux ppf = List.iter (fmt_ppr_sgn_decl ppf) in
        fprintf ppf "@[%s %s = %s@ @[<v2>%a@]@ %s;@]@\n"
-         (to_html "module" Keyword) (name) (to_html "struct" Keyword) (aux) decls (to_html "end" Keyword)
-    | Sgn.MRecTyp (l, decls) ->
-       fmt_ppr_mrecs 0 ppf decls
+         (to_html "module" Keyword)
+         identifier
+         (to_html "struct" Keyword)
+         aux declarations
+         (to_html "end" Keyword)
+
+    | Sgn.MRecTyp { declarations; _ } ->
+       fmt_ppr_mrecs 0 ppf declarations
     | _ -> ()
 
   let fmt_ppr_sgn ppf sgn = List.iter (fmt_ppr_sgn_decl ppf) sgn
diff --git a/src/core/prettyint.ml b/src/core/prettyint.ml
index 556c909f6..4a17ab3f9 100644
--- a/src/core/prettyint.ml
+++ b/src/core/prettyint.ml
@@ -1672,64 +1672,75 @@ module Make (R : Store.Cid.RENDERER) : Printer.Int.T = struct
 
   let rec fmt_ppr_sgn_decl ppf =
     function
-    | Sgn.CompTypAbbrev (_, _, _, _) -> ()
-    | Sgn.Const (_, c, a) ->
+    | Sgn.CompTypAbbrev _ -> ()
+    | Sgn.Const { identifier; typ; _ } ->
        fprintf ppf "%s : %a.@\n"
-         (R.render_cid_term c)
-         (fmt_ppr_lf_typ LF.Empty LF.Null l0) a
+         (R.render_cid_term identifier)
+         (fmt_ppr_lf_typ LF.Empty LF.Null l0) typ
 
-    | Sgn.Typ (_, a, k) ->
+    | Sgn.Typ { identifier; kind; _ } ->
        fprintf ppf "%s : %a.@\n"
-         (R.render_cid_typ a)
-         (fmt_ppr_lf_kind LF.Null l0) k
+         (R.render_cid_typ identifier)
+         (fmt_ppr_lf_kind LF.Null l0) kind
 
-    | Sgn.CompTyp (_, a, cK, _) ->
+    | Sgn.CompTyp { identifier; kind; _ } ->
        fprintf ppf "@\ndatatype %s : @[%a@] = @\n"
-         (Id.render_name a)
-         (fmt_ppr_cmp_kind LF.Empty l0) cK
+         (Id.render_name identifier)
+         (fmt_ppr_cmp_kind LF.Empty l0) kind
 
-    | Sgn.CompCotyp (_, a, cK) ->
+    | Sgn.CompCotyp { identifier; kind; _ } ->
        fprintf ppf "@\ncodatatype %s : @[%a@] = @\n"
-         (Id.render_name a)
-         (fmt_ppr_cmp_kind LF.Empty l0) cK
-
-    | Sgn.CompDest (_, c, cD, tau0, tau1) ->
+         (Id.render_name identifier)
+         (fmt_ppr_cmp_kind LF.Empty l0) kind
+
+    | Sgn.CompDest
+      { identifier
+      ; mctx=cD
+      ; observation_typ=tau0
+      ; return_typ=tau1
+      ; _
+      } ->
        fprintf ppf "@ | (%s : @[%a@] :: @[%a@]@\n"
-         (Id.render_name c)
+         (Id.render_name identifier)
          (fmt_ppr_cmp_typ cD l0) tau0
          (fmt_ppr_cmp_typ cD l0) tau1
-    | Sgn.CompConst (_, c, tau) ->
+
+    | Sgn.CompConst { identifier; typ; _ } ->
        fprintf ppf "@ | %s : @[%a@]@\n"
-         (Id.render_name c)
-         (fmt_ppr_cmp_typ LF.Empty l0) tau
+         (Id.render_name identifier)
+         (fmt_ppr_cmp_typ LF.Empty l0) typ
 
-    | Sgn.MRecTyp(_, l) -> List.iter (fmt_ppr_sgn_decl ppf) (List.flatten l)
+    | Sgn.MRecTyp { declarations; _ } ->
+      declarations
+      |> Nonempty.to_list
+      |> List.flatten
+      |> List.iter (fmt_ppr_sgn_decl ppf)
 
-    | Sgn.Val (_, x, tau, i, None) ->
+    | Sgn.Val { identifier; typ; expression; expression_value=None; _ } ->
        fprintf ppf "@\nlet %s : %a = %a@\n"
-         (Id.render_name x)
-         (fmt_ppr_cmp_typ LF.Empty l0) tau
-         (fmt_ppr_cmp_exp_chk LF.Empty LF.Empty l0) i
+         (Id.render_name identifier)
+         (fmt_ppr_cmp_typ LF.Empty l0) typ
+         (fmt_ppr_cmp_exp_chk LF.Empty LF.Empty l0) expression
 
-    | Sgn.Val (_, x, tau, i, Some v) ->
+    | Sgn.Val { identifier; typ; expression; expression_value=Some value; _ } ->
        fprintf ppf "@\nlet %s : %a = %a@\n   ===> %a@\n"
-         (Id.render_name x)
-         (fmt_ppr_cmp_typ LF.Empty l0) tau
-         (fmt_ppr_cmp_exp_chk LF.Empty LF.Empty l0) i
-         (fmt_ppr_cmp_value l0) v
+         (Id.render_name identifier)
+         (fmt_ppr_cmp_typ LF.Empty l0) typ
+         (fmt_ppr_cmp_exp_chk LF.Empty LF.Empty l0) expression
+         (fmt_ppr_cmp_value l0) value
 
-    | Sgn.Schema (w, schema) ->
+    | Sgn.Schema { identifier; schema; _ } ->
        fprintf ppf "@\nschema %s = @[%a@];@\n"
-         (R.render_cid_schema w)
+         (R.render_cid_schema identifier)
          (fmt_ppr_lf_schema ~useName:false l0) schema
 
-    | Sgn.Theorem thms ->
+    | Sgn.Theorem { theorems; _ } ->
        fprintf ppf "@[<v>%a@]"
-         (pp_print_list ~pp_sep: (fun ppf _ -> fprintf ppf "@,and ")
+         (Nonempty.print ~pp_sep: (fun ppf _ -> fprintf ppf "@,and ")
             (fun ppf x ->
               fprintf ppf "@[%a@]"
                 fmt_ppr_sgn_thm_decl x))
-         thms
+         theorems
 
     (*
     | Sgn.Rec (((f, _, _) as h)::t) ->
@@ -1740,24 +1751,24 @@ module Make (R : Store.Cid.RENDERER) : Printer.Int.T = struct
        List.iter (fmt_ppr_rec l0 ppf ("and"^total)) t
      *)
 
-    | Sgn.Pragma (LF.OpenPrag n) ->
+    | Sgn.Pragma { pragma=LF.OpenPrag n } ->
        let n' = Store.Modules.name_of_id n in
        ignore (Store.Modules.open_module n');
        fprintf ppf "@\n--open %s@\n" (String.concat "." n')
 
     | Sgn.Pragma _ -> ()
 
-    | Sgn.Module(_, name, decls) ->
+    | Sgn.Module { identifier; declarations; _ } ->
        let aux fmt t = List.iter (fun x -> (fmt_ppr_sgn_decl fmt x)) t in
 
        (* Necessary to enforce correct printing *)
        let (_, origName, _, _) as state = Store.Modules.getState () in
-       let newName = origName@[name] in
+       let newName = origName@[identifier] in
        Store.Modules.current := (Store.Modules.id_of_name newName);
        Store.Modules.currentName := newName;
        fprintf ppf "@\nmodule %s = struct@\n@[<v2>%a@]@\nend;@\n"
-         name
-         aux decls;
+         identifier
+         aux declarations;
        Store.Modules.setState state
 
     | _ -> ()
diff --git a/src/core/recsgn.ml b/src/core/recsgn.ml
index 464f40224..181b1e2b7 100644
--- a/src/core/recsgn.ml
+++ b/src/core/recsgn.ml
@@ -138,22 +138,22 @@ let rec get_target_cid_compcotyp tau =
 
 let freeze_from_name tau =
   match tau with
-  | Ext.Sgn.Typ (_, n, _) ->
-     let a = Typ.index_of_name n in
+  | Ext.Sgn.Typ { identifier; _ } ->
+     let a = Typ.index_of_name identifier in
      Typ.freeze a;
      ()
-  | Ext.Sgn.CompTyp (_, n, _, _) ->
-     let a = CompTyp.index_of_name n in
+  | Ext.Sgn.CompTyp { identifier; _ } ->
+     let a = CompTyp.index_of_name identifier in
      CompTyp.freeze a;
      ()
-  | Ext.Sgn.CompCotyp (_, n, _) ->
-     let a = CompCotyp.index_of_name n in
+  | Ext.Sgn.CompCotyp { identifier; _ } ->
+     let a = CompCotyp.index_of_name identifier in
      CompCotyp.freeze a;
      ()
 
 let sgnDeclToHtml =
   function
-  | Ext.Sgn.Comment (_, x) -> Html.appendAsComment x
+  | Ext.Sgn.Comment { content; _ } -> Html.appendAsComment content
   | d ->
     let margin = Format.pp_get_margin Format.str_formatter () in
     Html.printing := true;
@@ -166,10 +166,10 @@ let sgnDeclToHtml =
 
 let rec apply_global_pragmas =
   function
-  | Synext.Sgn.GlobalPragma (_, Synext.Sgn.NoStrengthen) :: t ->
+  | Synext.Sgn.GlobalPragma { pragma=Synext.Sgn.NoStrengthen; _ } :: t ->
      Lfrecon.strengthen := false;
      apply_global_pragmas t
-  | Synext.Sgn.GlobalPragma (_, Synext.Sgn.Coverage(opt)) :: t ->
+  | Synext.Sgn.GlobalPragma { pragma=Synext.Sgn.Coverage opt; _ } :: t ->
      Coverage.enableCoverage := true;
      begin match opt with
      | `Warn -> Coverage.warningOnly := true
@@ -194,7 +194,7 @@ let recSgnDecls decls =
     function
     | [] -> []
 
-    | Ext.Sgn.Pragma (loc, Ext.Sgn.NotPrag) :: not'd_decl :: rest ->
+    | Ext.Sgn.Pragma { location=loc; pragma=Ext.Sgn.NotPrag } :: not'd_decl :: rest ->
        let not'd_decl_succeeds =
            begin
              try
@@ -211,14 +211,14 @@ let recSgnDecls decls =
        else recSgnDecls' rest
 
     (* %not declaration with nothing following *)
-    | [Ext.Sgn.Pragma (_, Ext.Sgn.NotPrag)] -> []
+    | [Ext.Sgn.Pragma { pragma=Ext.Sgn.NotPrag; _ }] -> []
 
-    | Ext.Sgn.GlobalPragma (loc, Ext.Sgn.Coverage `Warn) :: rest ->
-       raise (Error (loc, IllegalOptsPrag "--warncoverage"))
-    | Ext.Sgn.GlobalPragma (loc, Ext.Sgn.Coverage `Error) :: rest ->
-       raise (Error (loc, IllegalOptsPrag "--coverage"))
-    | Ext.Sgn.GlobalPragma (loc, Ext.Sgn.NoStrengthen) :: rest ->
-       raise (Error (loc, IllegalOptsPrag "--nostrengthen"))
+    | Ext.Sgn.GlobalPragma { pragma=Ext.Sgn.Coverage `Warn; location } :: rest ->
+       raise (Error (location, IllegalOptsPrag "--warncoverage"))
+    | Ext.Sgn.GlobalPragma { pragma=Ext.Sgn.Coverage `Error; location } :: rest ->
+       raise (Error (location, IllegalOptsPrag "--coverage"))
+    | Ext.Sgn.GlobalPragma { pragma=Ext.Sgn.NoStrengthen; location } :: rest ->
+       raise (Error (location, IllegalOptsPrag "--nostrengthen"))
 
     | decl :: rest ->
        let decl' = recSgnDecl decl in
@@ -231,16 +231,17 @@ let recSgnDecls decls =
     if !Html.generate && not pauseHtml
     then sgnDeclToHtml d;
     match d with
-    | Ext.Sgn.Comment (l, s) -> Int.Sgn.Comment (l, s)
-    | Ext.Sgn.Pragma (loc, Ext.Sgn.AbbrevPrag (orig, abbrev)) ->
+    | Ext.Sgn.Comment { location; content } ->
+        Int.Sgn.Comment { location; content }
+    | Ext.Sgn.Pragma { location=loc; pragma=Ext.Sgn.AbbrevPrag (orig, abbrev) } ->
        begin
          try
            Store.Modules.addAbbrev orig abbrev
          with
          | Not_found -> raise (Error (loc, InvalidAbbrev (orig, abbrev)))
        end;
-       Int.Sgn.Pragma (Int.LF.AbbrevPrag (orig, abbrev))
-    | Ext.Sgn.Pragma (loc, Ext.Sgn.DefaultAssocPrag a) ->
+       Int.Sgn.Pragma { pragma=Int.LF.AbbrevPrag (orig, abbrev) }
+    | Ext.Sgn.Pragma { location=loc; pragma=Ext.Sgn.DefaultAssocPrag a } ->
        OpPragmas.default := a;
        let a' =
          match a with
@@ -248,8 +249,8 @@ let recSgnDecls decls =
          | Ext.Sgn.Right -> Int.LF.Right
          | Ext.Sgn.None -> Int.LF.NoAssoc
        in
-       Int.Sgn.Pragma (Int.LF.DefaultAssocPrag a')
-    | Ext.Sgn.Pragma (loc, Ext.Sgn.FixPrag (name, fix, precedence, assoc)) ->
+       Int.Sgn.Pragma { pragma=Int.LF.DefaultAssocPrag a' }
+    | Ext.Sgn.Pragma { location=loc; pragma=Ext.Sgn.FixPrag (name, fix, precedence, assoc) } ->
        dprint (fun () -> "Pragma found for " ^ (Id.render_name name));
        begin match fix with
        | Ext.Sgn.Prefix ->
@@ -296,16 +297,16 @@ let recSgnDecls decls =
          | Ext.Sgn.Prefix -> Int.LF.Prefix
          | Ext.Sgn.Infix -> Int.LF.Infix
        in
-       Int.Sgn.Pragma (Int.LF.FixPrag (name, fix', precedence, assoc'))
+       Int.Sgn.Pragma { pragma=Int.LF.FixPrag (name, fix', precedence, assoc') }
 
-    | Ext.Sgn.CompTypAbbrev (loc, a, cK, cT) ->
+    | Ext.Sgn.CompTypAbbrev { location; identifier; kind=cK; typ=cT } ->
        (* index cT in a context which contains arguments to cK *)
        let (apx_tau, apxK) = Index.comptypdef (cT, cK) in
-       let ((cD, tau), i, cK) = Reconstruct.comptypdef loc a (apx_tau, apxK) in
+       let ((cD, tau), i, cK) = Reconstruct.comptypdef location identifier (apx_tau, apxK) in
        dprintf
          begin fun p ->
          p.fmt "typedef %a : %a = %a"
-           Id.print a
+           Id.print identifier
            (P.fmt_ppr_cmp_kind Int.LF.Empty P.l0) cK
            (P.fmt_ppr_cmp_typ cD P.l0) tau
          end;
@@ -313,16 +314,16 @@ let recSgnDecls decls =
          ("Type abbrev. : Kind Check", fun () -> Check.Comp.checkKind Int.LF.Empty cK);
        Monitor.timer
          ("Type abbrev. : Type Check", fun () -> Check.Comp.checkTyp cD tau);
-       ignore (CompTypDef.add (fun _ -> CompTypDef.mk_entry a i (cD, tau) cK));
-       let sgn = Int.Sgn.CompTypAbbrev (loc, a, cK, tau) in
+       ignore (CompTypDef.add (fun _ -> CompTypDef.mk_entry identifier i (cD, tau) cK));
+       let sgn = Int.Sgn.CompTypAbbrev { location; identifier; kind=cK; typ=tau } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.CompTyp (loc , a, extK, pflag) ->
-       dprint (fun () -> "Indexing computation-level data-type constant " ^ string_of_name a);
+    | Ext.Sgn.CompTyp { location; identifier; kind=extK; datatype_flavour=pflag } ->
+       dprint (fun () -> "Indexing computation-level data-type constant " ^ string_of_name identifier);
        let apxK = Index.compkind extK in
        FVar.clear ();
-       dprint (fun () -> "Elaborating data-type declaration " ^ string_of_name a);
+       dprint (fun () -> "Elaborating data-type declaration " ^ string_of_name identifier);
        let cK =
          Monitor.timer
            ( "CType Elaboration"
@@ -344,7 +345,7 @@ let recSgnDecls decls =
        dprintf
          begin fun p ->
          p.fmt "%a : %a"
-           Id.print a
+           Id.print identifier
            (P.fmt_ppr_cmp_kind Int.LF.Empty P.l0) cK'
          end;
        Monitor.timer
@@ -353,7 +354,7 @@ let recSgnDecls decls =
          );
        dprint
          (fun () ->
-           "\nDOUBLE CHECK for data type constant " ^ string_of_name a ^ " successful!");
+           "\nDOUBLE CHECK for data type constant " ^ string_of_name identifier ^ " successful!");
        (* let p =
         *   match pflag with
         *   | None -> Int.Sgn. Noflag
@@ -364,24 +365,24 @@ let recSgnDecls decls =
 
        let p =
          match pflag with
-         | Ext.Sgn.StratifiedDatatype -> Int.Sgn.StratifyAll loc
+         | Ext.Sgn.StratifiedDatatype -> Int.Sgn.StratifyAll location
          | Ext.Sgn.InductiveDatatype -> Int.Sgn.Positivity
        in
        Total.stratNum := -1;
-       ignore (CompTyp.add (fun _ -> CompTyp.mk_entry a cK' i p));
-       let sgn = Int.Sgn.CompTyp (loc, a, cK', p) in
+       ignore (CompTyp.add (fun _ -> CompTyp.mk_entry identifier cK' i p));
+       let sgn = Int.Sgn.CompTyp { location; identifier; kind=cK'; positivity_flag=p } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.CompCotyp (loc , a, extK) ->
+    | Ext.Sgn.CompCotyp { location; identifier; kind=extK } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] CompCotyp at: %a"
-             Syntax.Loc.print loc);
-       dprint (fun () -> "\nIndexing computation-level codata-type constant " ^ string_of_name a);
+             Syntax.Loc.print location);
+       dprint (fun () -> "\nIndexing computation-level codata-type constant " ^ string_of_name identifier);
        let apxK = Index.compkind extK in
        FVar.clear ();
-       dprint (fun () -> "\nElaborating codata-type declaration " ^ string_of_name a);
+       dprint (fun () -> "\nElaborating codata-type declaration " ^ string_of_name identifier);
        let cK =
          Monitor.timer
            ( "CType Elaboration"
@@ -404,7 +405,7 @@ let recSgnDecls decls =
        dprintf
          begin fun p ->
          p.fmt "%a : %a"
-           Id.print a
+           Id.print identifier
            (P.fmt_ppr_cmp_kind Int.LF.Empty P.l0) cK'
          end;
        Monitor.timer
@@ -413,23 +414,23 @@ let recSgnDecls decls =
          );
        dprint
          (fun () ->
-           "\nDOUBLE CHECK for codata type constant " ^ string_of_name a ^
+           "\nDOUBLE CHECK for codata type constant " ^ string_of_name identifier ^
              " successful!");
-       ignore (CompCotyp.add (fun _ -> CompCotyp.mk_entry a cK' i));
-       let sgn = Int.Sgn.CompCotyp (loc, a, cK') in
+       ignore (CompCotyp.add (fun _ -> CompCotyp.mk_entry identifier cK' i));
+       let sgn = Int.Sgn.CompCotyp { location; identifier; kind=cK' } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
 
-    | Ext.Sgn.CompConst (loc , c, tau) ->
+    | Ext.Sgn.CompConst { location; identifier; typ=tau } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] CompConst at: %a"
-             Syntax.Loc.print_short loc);
-       dprint (fun () -> "\nIndexing computation-level data-type constructor " ^ string_of_name c);
+             Syntax.Loc.print_short location);
+       dprint (fun () -> "\nIndexing computation-level data-type constructor " ^ string_of_name identifier);
        let apx_tau = Index.comptyp tau in
        let cD = Int.LF.Empty in
-       dprint (fun () -> "\nElaborating data-type constructor " ^ string_of_name c);
+       dprint (fun () -> "\nElaborating data-type constructor " ^ string_of_name identifier);
        let tau' =
          Monitor.timer
            ( "Data-type Constant: Type Elaboration"
@@ -448,7 +449,7 @@ let recSgnDecls decls =
        dprintf
          begin fun p ->
          p.fmt "[recsgn] @[<v>@[<hov>@[%a@] :@ @[%a@]@]@,with %d implicit parameters@]"
-           Id.print c
+           Id.print identifier
            (P.fmt_ppr_cmp_typ cD P.l0) tau'
            i
          end;
@@ -465,11 +466,11 @@ let recSgnDecls decls =
        | Int.Sgn.Positivity ->
           if Total.positive cid_ctypfamily tau'
           then ()
-          else raise (Error (loc, (NoPositive (string_of_name c))))
+          else raise (Error (location, (NoPositive (string_of_name identifier))))
        | Int.Sgn.Stratify (loc_s, n) ->
           if Total.stratify cid_ctypfamily tau' n
           then ()
-          else raise (Error (loc, (NoStratify (string_of_name c))))
+          else raise (Error (location, (NoStratify (string_of_name identifier))))
        | Int.Sgn.StratifyAll loc_s ->
           let t = Total.stratifyAll cid_ctypfamily tau' in
           let t' = (t land (!Total.stratNum)) in
@@ -491,23 +492,29 @@ let recSgnDecls decls =
         *     else raise (Error (loc, (NoPositive (string_of_name c))))
         *   else ()
         * end; *)
-       ignore (CompConst.add cid_ctypfamily (fun _ -> CompConst.mk_entry c tau' i));
-       let sgn = Int.Sgn.CompConst (loc, c, tau') in
+       ignore (CompConst.add cid_ctypfamily (fun _ -> CompConst.mk_entry identifier tau' i));
+       let sgn = Int.Sgn.CompConst { location; identifier; typ=tau' } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
 
 
-    | Ext.Sgn.CompDest (loc , c, cD, tau0, tau1) ->
+    | Ext.Sgn.CompDest
+      { location
+      ; identifier
+      ; mctx=cD
+      ; observation_typ=tau0
+      ; return_typ=tau1
+      } ->
        dprintf
          (fun p ->
-           p.fmt "[RecSgn Checking] CompDest at: %a" Syntax.Loc.print_short loc);
-       dprint (fun () -> "\nIndexing computation-level codata-type destructor " ^ string_of_name c);
+           p.fmt "[RecSgn Checking] CompDest at: %a" Syntax.Loc.print_short location);
+       dprint (fun () -> "\nIndexing computation-level codata-type destructor " ^ string_of_name identifier);
        let cD = Index.mctx cD in
        let cD = Reconstruct.mctx cD in
        let apx_tau0 = Index.comptyp tau0 in
        let apx_tau1 = Index.comptyp tau1 in
-       dprint (fun () -> "\nElaborating codata-type destructor " ^ string_of_name c);
+       dprint (fun () -> "\nElaborating codata-type destructor " ^ string_of_name identifier);
        let tau0' =
          Monitor.timer
            ( "Codata-type Constant: Type Elaboration"
@@ -538,7 +545,7 @@ let recSgnDecls decls =
        dprintf
          begin fun p ->
          p.fmt "%a : %a :: %a"
-           Id.print c
+           Id.print identifier
            (P.fmt_ppr_cmp_typ cD1 P.l0) tau0'
            (P.fmt_ppr_cmp_typ cD1 P.l0) tau1'
          end;
@@ -551,17 +558,24 @@ let recSgnDecls decls =
          , fun () -> Check.Comp.checkTyp cD1 tau1'
          );
        let cid_ctypfamily = get_target_cid_compcotyp tau0' in
-       ignore (CompDest.add cid_ctypfamily (fun _ -> CompDest.mk_entry c cD1 tau0' tau1' i));
-       let sgn = Int.Sgn.CompDest (loc, c, cD1, tau0', tau1') in
+       ignore (CompDest.add cid_ctypfamily (fun _ -> CompDest.mk_entry identifier cD1 tau0' tau1' i));
+       let sgn =
+        Int.Sgn.CompDest
+        { location
+        ; identifier
+        ; mctx=cD1
+        ; observation_typ=tau0'
+        ; return_typ=tau1'
+        } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
 
-    | Ext.Sgn.Typ (loc, a, extK) ->
+    | Ext.Sgn.Typ { location; identifier=a; kind=extK } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Typ at: %a"
-             Syntax.Loc.print_short loc);
+             Syntax.Loc.print_short location);
        dprint (fun () -> "\nIndexing type constant " ^ string_of_name a);
        let (_, apxK) = Index.kind Index.disambiguate_to_fvars extK in
        FVar.clear ();
@@ -601,17 +615,17 @@ let recSgnDecls decls =
          ^ string_of_name a
          ^ " successful!"
          end;
-       Typeinfo.Sgn.add loc (Typeinfo.Sgn.mk_entry (Typeinfo.Sgn.Kind tK')) "";
+       Typeinfo.Sgn.add location (Typeinfo.Sgn.mk_entry (Typeinfo.Sgn.Kind tK')) "";
        let cid = Typ.add (fun _ -> Typ.mk_entry a tK' i) in
-       let sgn = Int.Sgn.Typ (loc, cid, tK') in
+       let sgn = Int.Sgn.Typ { location; identifier=cid; kind=tK' } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.Const (loc, c, extT) ->
+    | Ext.Sgn.Const { location; identifier=c; typ=extT } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Const at: %a"
-             Syntax.Loc.print_short loc);
+             Syntax.Loc.print_short location);
        let (_, apxT) = Index.typ Index.disambiguate_to_fvars extT in
        let rec get_type_family =
          function
@@ -656,17 +670,17 @@ let recSgnDecls decls =
          ( "Constant Check"
          , fun () -> Check.LF.checkTyp Int.LF.Empty Int.LF.Null (tA', S.LF.id)
          );
-       Typeinfo.Sgn.add loc (Typeinfo.Sgn.mk_entry (Typeinfo.Sgn.Typ tA')) "";
-       let cid = Term.add' loc constructedType (fun _ -> Term.mk_entry c tA' i) in
-       let sgn = Int.Sgn.Const (loc, cid, tA') in
+       Typeinfo.Sgn.add location (Typeinfo.Sgn.mk_entry (Typeinfo.Sgn.Typ tA')) "";
+       let cid = Term.add' location constructedType (fun _ -> Term.mk_entry c tA' i) in
+       let sgn = Int.Sgn.Const { location; identifier=cid; typ=tA' } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.Schema (loc, g, schema) ->
+    | Ext.Sgn.Schema { location; identifier=g; schema } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Schema at: %a"
-             Syntax.Loc.print_short loc);
+             Syntax.Loc.print_short location);
        let apx_schema = Index.schema schema in
        dprint (fun () -> "\nReconstructing schema " ^ string_of_name g ^ "\n");
        FVar.clear ();
@@ -691,18 +705,16 @@ let recSgnDecls decls =
        Check.LF.checkSchemaWf sW';
        dprint (fun () -> "\nTYPE CHECK for schema " ^ string_of_name g ^ " successful");
        let sch = Schema.add (fun _ -> Schema.mk_entry g sW') in
-       let sgn = Int.Sgn.Schema(sch, sW') in
+       let sgn = Int.Sgn.Schema { location; identifier=sch; schema=sW' } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-
-
-    | Ext.Sgn.Val (loc, x, None, i) ->
+    | Ext.Sgn.Val { location; identifier; typ=None; expression } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Val at: %a"
-             Syntax.Loc.print_short loc);
-       let apx_i = Index.exp' (Var.create ()) i in
+             Syntax.Loc.print_short location);
+       let apx_i = Index.exp' (Var.create ()) expression in
        let (cD, cG) = (Int.LF.Empty, Int.LF.Empty) in
        let (i', (tau, theta)) =
          Monitor.timer
@@ -712,40 +724,40 @@ let recSgnDecls decls =
        in
        Unify.forceGlobalCnstr ();
        let tau' = Whnf.cnormCTyp (tau, theta) in
-       let i' = Whnf.cnormExp' (i', Whnf.m_id) in
+       let expression' = Whnf.cnormExp' (i', Whnf.m_id) in
 
        dprintf
          begin fun p ->
          p.fmt "[AFTER Reconstruction Val] @[<v 2>let %a : %a =@ %a@]"
-           Id.print x
+           Id.print identifier
            (P.fmt_ppr_cmp_typ cD P.l0) tau'
-           (P.fmt_ppr_cmp_exp_syn cD cG P.l0) i'
+           (P.fmt_ppr_cmp_exp_syn cD cG P.l0) expression'
          end;
-       let cQ, i'' =
+       let cQ, expression'' =
          Monitor.timer
            ( "Function Abstraction"
            , fun _ ->
-             Abstract.exp (Int.Comp.Syn (loc, i'))
+             Abstract.exp (Int.Comp.Syn (location, expression'))
            )
        in
-       storeLeftoverVars cQ loc;
+       storeLeftoverVars cQ location;
        Monitor.timer
          ( "Function Check"
-         , fun _ -> Check.Comp.check None cD cG [] i'' (tau', C.m_id)
+         , fun _ -> Check.Comp.check None cD cG [] expression'' (tau', C.m_id)
          );
 
        let v =
          if Holes.none () && is_empty cQ
          then
            begin
-             let v = Some (Opsem.eval i'') in
+             let v = Some (Opsem.eval expression'') in
              let open Comp in
              add begin fun _ ->
                let mgid =
                  Comp.add_mutual_group
-                   Int.Comp.[{ name = x; tau = tau'; order = `not_recursive }]
+                   Int.Comp.[{ name = identifier; tau = tau'; order = `not_recursive }]
                in
-               mk_entry (Some (Decl.next ())) x tau' 0 mgid v
+               mk_entry (Some (Decl.next ())) identifier tau' 0 mgid v
                end
              |> ignore;
              v
@@ -753,15 +765,15 @@ let recSgnDecls decls =
          else
            None
        in
-       let sgn = Int.Sgn.Val (loc, x, tau', i'', v) in
+       let sgn = Int.Sgn.Val { location; identifier; typ=tau'; expression=expression''; expression_value=v } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.Val (loc, x, Some tau, i) ->
+    | Ext.Sgn.Val { location; identifier; typ=Some tau; expression } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Val at %a"
-             Syntax.Loc.print_short loc
+             Syntax.Loc.print_short location
          );
        let apx_tau = Index.comptyp tau in
        let (cD, cG) = (Int.LF.Empty, Int.LF.Empty) in
@@ -782,50 +794,49 @@ let recSgnDecls decls =
          ( "Function Type Check"
          , fun () -> Check.Comp.checkTyp cD tau'
          );
-       let apx_i = Index.exp' (Var.create ()) i in
+       let apx_i = Index.exp' (Var.create ()) expression in
        let i' =
          Monitor.timer
            ( "Function Elaboration"
            , fun _ ->
-             Reconstruct.exp cG (Apx.Comp.Syn(loc, apx_i)) (tau', C.m_id)
+             Reconstruct.exp cG (Apx.Comp.Syn(location, apx_i)) (tau', C.m_id)
            )
        in
-       let i' = Whnf.cnormExp (i', Whnf.m_id) in
+       let expression' = Whnf.cnormExp (i', Whnf.m_id) in
        Unify.forceGlobalCnstr ();
        let tau' = Whnf.cnormCTyp (tau', C.m_id) in
        dprintf
          begin fun p ->
            p.fmt "[AFTER Reconstruction Val - 2] let %s : %a =@,%a"
-             (Id.render_name x)
+             (Id.render_name identifier)
              (P.fmt_ppr_cmp_typ cD P.l0) tau'
-             (P.fmt_ppr_cmp_exp_chk cD cG P.l0) i'
+             (P.fmt_ppr_cmp_exp_chk cD cG P.l0) expression'
          end;
 
-       let cQ, i'' =
+       let cQ, expression'' =
          Monitor.timer
            ( "Function Abstraction"
-           , fun () -> Abstract.exp i'
+           , fun () -> Abstract.exp expression'
            )
        in
-       storeLeftoverVars cQ loc;
+       storeLeftoverVars cQ location;
        Monitor.timer
          ( "Function Check"
          , fun _ ->
-           Check.Comp.check None cD cG [] i'' (tau', C.m_id)
+           Check.Comp.check None cD cG [] expression'' (tau', C.m_id)
          );
-
        let v =
          if Holes.none () && is_empty cQ
          then
            begin
-             let v = Some (Opsem.eval i'') in
+             let v = Some (Opsem.eval expression'') in
              let open Comp in
              let mgid =
                add_mutual_group
-                 Int.Comp.[ {name = x; tau = tau'; order = `not_recursive } ]
+                 Int.Comp.[ {name = identifier; tau = tau'; order = `not_recursive } ]
              in
              add begin fun _ ->
-               mk_entry (Some (Decl.next ())) x tau' 0 mgid v
+               mk_entry (Some (Decl.next ())) identifier tau' 0 mgid v
                end;
              |> ignore;
              v
@@ -833,22 +844,25 @@ let recSgnDecls decls =
          else
            None
        in
-       let sgn = Int.Sgn.Val (loc, x, tau', i'', v) in
+       let sgn = Int.Sgn.Val { location; identifier; typ=tau'; expression=expression''; expression_value=v } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.MRecTyp (loc, recDats) ->
+    | Ext.Sgn.MRecTyp { location; declarations=recDats } ->
        dprintf
          (fun p ->
-           p.fmt "[recsgn] MRecTyp at %a" Loc.print_short loc);
-       let recTyps = List.map (fun (k, _) -> k) recDats in
-       let recTyps' = List.map (recSgnDecl ~pauseHtml:true) recTyps in
-       let recConts = List.map (fun (_, cs) -> cs) recDats in
-       let recConts' = List.map (List.map (recSgnDecl ~pauseHtml:true)) recConts in
-       List.iter freeze_from_name recTyps;
-       Int.Sgn.MRecTyp (loc, List.map2 (fun x y -> x :: y) recTyps' recConts')
-
-    | Ext.Sgn.Theorem (loc, recFuns) ->
+           p.fmt "[recsgn] MRecTyp at %a" Loc.print_short location);
+       let recTyps = Nonempty.map (fun (k, _) -> k) recDats in
+       let recTyps' = Nonempty.map (recSgnDecl ~pauseHtml:true) recTyps in
+       let recConts = Nonempty.map (fun (_, cs) -> cs) recDats in
+       let recConts' = Nonempty.map (List.map (recSgnDecl ~pauseHtml:true)) recConts in
+       Nonempty.iter freeze_from_name recTyps;
+       Int.Sgn.MRecTyp
+        { location
+        ; declarations=Nonempty.map2 (fun x y -> x :: y) recTyps' recConts'
+        }
+
+    | Ext.Sgn.Theorem { location; theorems=recFuns } ->
        let pos loc x args =
          match
            List.index_of
@@ -890,30 +904,27 @@ let recSgnDecls decls =
        (* and check that all or none of the declarations are present. *)
        let total_decs =
          let prelim_total_decs =
-           List.map (fun t -> Ext.Sgn.(t.thm_name, t.thm_order)) recFuns
-         in
-         let go p =
-           Option.filter_map
-             (fun (name, x) -> if p x then Some (name, x) else None)
-             prelim_total_decs
+           Nonempty.map (fun t -> Ext.Sgn.(t.thm_name, t.thm_order)) recFuns
          in
          match
-           go Option.is_some,
-           go Fun.(not ++ Option.is_some)
+            Nonempty.partition
+              (fun (_, order) -> Option.is_some order) prelim_total_decs
          with
          | [], [] ->
             Error.violation "[recSgn] empty mutual block is impossible"
          | haves, [] ->
-            Some (List.map Fun.(Option.get ++ snd) haves)
+            haves
+            |> List.map Fun.(Option.get ++ snd)
+            |> Nonempty.of_list
          (* safe because they're haves *)
          | [], have_nots -> None
          | haves, have_nots ->
-            throw loc
+            throw location
               (MutualTotalDecl (List.map fst haves, List.map fst have_nots))
        in
 
        let preprocess =
-         List.map
+         Nonempty.map
            begin fun Ext.Sgn.{ thm_typ; thm_name; thm_loc; thm_body; _ } ->
            let apx_tau = Index.comptyp thm_typ in
            let tau' =
@@ -955,7 +966,7 @@ let recSgnDecls decls =
            end
        in
 
-       let (thm_list, registers) = List.split (preprocess recFuns) in
+       let (thm_list, registers) = Nonempty.split (preprocess recFuns) in
 
        (* We have the elaborated types of the theorems,
           so we construct the final list of totality declarations for
@@ -963,14 +974,14 @@ let recSgnDecls decls =
        let total_decs =
          match total_decs with
          | Some total_decs ->
-            List.map2
+            Nonempty.map2
               (fun (thm_name, _, _, tau) decl ->
                 mk_total_decl thm_name tau decl
                 |> Int.Comp.make_total_dec thm_name tau)
               thm_list
               total_decs
          | None ->
-            List.map
+            Nonempty.map
               (fun (thm_name, _, _, tau) ->
                 Int.Comp.make_total_dec thm_name tau `partial)
               thm_list
@@ -981,7 +992,7 @@ let recSgnDecls decls =
         *)
        let thm_cid_list =
           registers
-          |> List.ap_one (Comp.add_mutual_group total_decs)
+          |> Nonempty.ap_one (Comp.add_mutual_group (Nonempty.to_list total_decs))
        in
 
        let reconThm loc (f, cid, thm, tau) =
@@ -1039,7 +1050,7 @@ let recSgnDecls decls =
          let thm_r' = Whnf.cnormThm (thm_r, Whnf.m_id) in
 
          let tau_ann =
-           match Total.lookup_dec f total_decs with
+           match Total.lookup_dec f (Nonempty.to_list total_decs) with
            | None -> tau
            | Some d ->
               let tau = Total.annotate loc d.Int.Comp.order tau in
@@ -1059,31 +1070,28 @@ let recSgnDecls decls =
                       @,@[<hv 2>total_decs =@ @[<v>%a@]@]\
                       @,tau_ann = @[%a@]@]"
                  Id.print f
-                 (Format.pp_print_list ~pp_sep: Format.pp_print_cut
+                 (Nonempty.print ~pp_sep: Format.pp_print_cut
                     P.(fmt_ppr_cmp_total_dec))
                  total_decs
                  P.(fmt_ppr_cmp_typ Int.LF.Empty l0) tau_ann
                end;
-             Total.enabled := Total.requires_checking f total_decs;
-             Check.Comp.thm (Some cid) Int.LF.Empty Int.LF.Empty total_decs thm_r' (tau_ann, C.m_id);
+             Total.enabled := Total.requires_checking f (Nonempty.to_list total_decs);
+             Check.Comp.thm (Some cid) Int.LF.Empty Int.LF.Empty (Nonempty.to_list total_decs) thm_r' (tau_ann, C.m_id);
              Total.enabled := false;
            );
          (thm_r' , tau)
        in
 
-       if List.null recFuns
-       then Error.violation "[recsgn] no recursive function defined";
-
        let ds =
          let reconOne (thm_cid, (thm_name, thm_body, thm_loc, thm_typ)) =
-           let (e_r', tau') = reconThm loc (thm_name, thm_cid, thm_body, thm_typ) in
+           let (e_r', tau') = reconThm location (thm_name, thm_cid, thm_body, thm_typ) in
            dprintf
              begin fun p ->
              p.fmt "[reconRecFun] @[<v>DOUBLE CHECK of function %a at %a successful@,Adding definition to the store.@]"
                Id.print thm_name
                Loc.print_short thm_loc
              end;
-           let v =Int.(Comp.ThmValue (thm_cid, e_r', LF.MShift 0, Comp.Empty)) in
+           let v = Int.(Comp.ThmValue (thm_cid, e_r', LF.MShift 0, Comp.Empty)) in
            Comp.set_prog thm_cid (Fun.const (Some v));
            let open Int.Sgn in
            { thm_name = thm_cid
@@ -1092,17 +1100,23 @@ let recSgnDecls decls =
            ; thm_typ = tau'
            }
          in
-         List.map reconOne (List.combine thm_cid_list thm_list)
+         Nonempty.map reconOne (Nonempty.combine thm_cid_list thm_list)
        in
-       let decl = Int.Sgn.(Theorem ds) in
+       let decl = Int.Sgn.(Theorem { location; theorems=ds }) in
        Store.Modules.addSgnToCurrent decl;
        decl
 
-    | Ext.Sgn.Query (loc, name, extT, expected, tries) ->
+    | Ext.Sgn.Query
+      { location
+      ; name
+      ; typ=extT
+      ; expected_solutions=expected
+      ; maximum_tries=tries
+      } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Query at %a"
-             Syntax.Loc.print_short loc);
+             Syntax.Loc.print_short location);
        let (_, apxT) = Index.typ Index.disambiguate_to_fvars extT in
        dprint (fun () -> "Reconstructing query.");
        FVar.clear ();
@@ -1141,9 +1155,15 @@ let recSgnDecls decls =
            Check.LF.checkTyp Int.LF.Empty Int.LF.Null (tA', S.LF.id)
          );
        Logic.storeQuery name (tA', i) expected tries;
-       Int.Sgn.Query (loc, name, (tA', i), expected, tries)
-
-    | Ext.Sgn.Pragma (loc, Ext.Sgn.NamePrag (typ_name, m_name, v_name)) ->
+       Int.Sgn.Query
+       { location
+       ; name
+       ; typ=(tA', i)
+       ; expected_solutions=expected
+       ; maximum_tries=tries
+       }
+
+    | Ext.Sgn.Pragma { location=loc; pragma=Ext.Sgn.NamePrag (typ_name, m_name, v_name) } ->
        dprintf
          (fun p ->
            p.fmt "[RecSgn Checking] Pragma at %a"
@@ -1156,25 +1176,25 @@ let recSgnDecls decls =
           let m = Some (Gensym.MVarData.name_gensym m_name) in
           let v = Option.(v_name $> Gensym.VarData.name_gensym) in
           Typ.set_name_convention cid m v;
-          Int.Sgn.Pragma (Int.LF.NamePrag cid)
+          Int.Sgn.Pragma { pragma=Int.LF.NamePrag cid }
        | None ->
            throw loc (UnboundNamePragma typ_name)
        end
 
-    | Ext.Sgn.Module (loc, name, decls) ->
+    | Ext.Sgn.Module { location; identifier; declarations=decls } ->
        let state = Store.Modules.getState () in
-       ignore (Store.Modules.instantiateModule name);
+       ignore (Store.Modules.instantiateModule identifier);
        let decls' = List.map recSgnDecl decls in
 
        Store.Modules.setState state;
-       let sgn = Int.Sgn.Module (loc, name, decls') in
+       let sgn = Int.Sgn.Module { location; identifier; declarations=decls' } in
        Store.Modules.addSgnToCurrent sgn;
        sgn
 
-    | Ext.Sgn.Pragma (loc, Ext.Sgn.OpenPrag n) ->
+    | Ext.Sgn.Pragma { location=loc; pragma=Ext.Sgn.OpenPrag n } ->
        try
          let x = Modules.open_module n in
-         let sgn = Int.Sgn.Pragma (Int.LF.OpenPrag x) in
+         let sgn = Int.Sgn.Pragma { pragma=Int.LF.OpenPrag x } in
          Store.Modules.addSgnToCurrent sgn;
          sgn
        with
diff --git a/src/core/store.ml b/src/core/store.ml
index d95fbb6b0..e10791ac4 100644
--- a/src/core/store.ml
+++ b/src/core/store.ml
@@ -144,8 +144,8 @@ module Modules = struct
     let l =
       x ::
         ( !(DynArray.get modules x)
-          |> List.filter (function (Int.Sgn.Pragma(Int.LF.OpenPrag _)) -> true | _ -> false)
-          |> List.map (fun (Int.Sgn.Pragma(Int.LF.OpenPrag x)) -> x)
+          |> List.filter (function (Int.Sgn.Pragma { pragma=Int.LF.OpenPrag _ }) -> true | _ -> false)
+          |> List.map (fun (Int.Sgn.Pragma { pragma=Int.LF.OpenPrag x }) -> x)
         )
     in
     opened := l @ !opened;
diff --git a/src/core/store.mli b/src/core/store.mli
index c0ae94467..e8baf343a 100644
--- a/src/core/store.mli
+++ b/src/core/store.mli
@@ -1,3 +1,4 @@
+open Support
 open Id
 open Syntax.Int
 
@@ -117,7 +118,7 @@ module Cid : sig
 
     val mk_entry : name -> LF.typ -> int -> entry
     val get : cid_term -> entry
-    val add' : Loc.t -> cid_typ -> (cid_term -> entry) -> cid_term
+    val add' : Location.t -> cid_typ -> (cid_term -> entry) -> cid_term
     val get_implicit_arguments : cid_term -> int
     val index_of_name : name -> cid_term
     val args_of_name : name -> int
diff --git a/src/core/synext.ml b/src/core/synext.ml
index 2b94b6273..e725226bd 100644
--- a/src/core/synext.ml
+++ b/src/core/synext.ml
@@ -286,10 +286,11 @@ module Harpoon = struct
 
   type command =
     (* Administrative commands *)
-    | Rename
-      of name (* from *)
-         * name (* to *)
-         * level
+    | Rename of
+      { rename_from: name
+      ; rename_to: name
+      ; level: level
+      }
     | ToggleAutomation of automation_kind * automation_change
 
     | Type of Comp.exp_syn
@@ -350,22 +351,107 @@ module Sgn = struct
     ; thm_body : Comp.thm
     }
 
+  (** Parsed signature element *)
   type decl =
-    | Const of Location.t * name * LF.typ
-    | Typ of Location.t * name * LF.kind
-    | CompTyp of Location.t * name * Comp.kind * datatype_flavour
-    | CompCotyp of Location.t * name * Comp.kind
-    | CompConst of Location.t * name * Comp.typ
-    | CompDest of Location.t * name * LF.mctx * Comp.typ * Comp.typ
-    | CompTypAbbrev of Location.t * name * Comp.kind * Comp.typ
-    | Schema of Location.t * name * LF.schema
-    | Pragma of Location.t * pragma
-    | GlobalPragma of Location.t * global_pragma
-    | MRecTyp of Location.t * (decl * decl list) list
-    | Theorem of Location.t * thm_decl list
-    | Val of Location.t * name * Comp.typ option * Comp.exp_syn
-    | Query of Location.t * name option * LF.typ * int option * int option
-    | Module of Location.t * string * decl list
-    | Comment of Location.t * string
+    | Typ of
+      { location: Location.t
+      ; identifier: name
+      ; kind: LF.kind
+      } (** LF type family declaration *)
+
+    | Const of
+      { location: Location.t
+      ; identifier: name
+      ; typ: LF.typ
+      } (** LF type constant decalaration *)
+
+    | CompTyp of
+      { location: Location.t
+      ; identifier: name
+      ; kind: Comp.kind
+      ; datatype_flavour: datatype_flavour
+      } (** Computation-level data type constant declaration *)
+
+    | CompCotyp of
+      { location: Location.t
+      ; identifier: name
+      ; kind: Comp.kind
+      } (** Computation-level codata type constant declaration *)
+
+    | CompConst of
+      { location: Location.t
+      ; identifier: name
+      ; typ: Comp.typ
+      } (** Computation-level type constructor declaration *)
+
+    | CompDest of
+      { location: Location.t
+      ; identifier: name
+      ; mctx: LF.mctx
+      ; observation_typ: Comp.typ
+      ; return_typ: Comp.typ
+      } (** Computation-level type destructor declaration *)
+
+    | CompTypAbbrev of
+      { location: Location.t
+      ; identifier: name
+      ; kind: Comp.kind
+      ; typ: Comp.typ
+      } (** Synonym declaration for computation-level type *)
+
+    | Schema of
+      { location: Location.t
+      ; identifier: name
+      ; schema: LF.schema
+      } (** Declaration of a specification for a set of contexts *)
+
+    | Pragma of
+      { location: Location.t
+      ; pragma: pragma
+      } (** Compiler directive *)
+
+    | GlobalPragma of
+      { location: Location.t
+      ; pragma: global_pragma
+      } (** Global directive *)
+
+    | MRecTyp of
+      { location: Location.t
+      ; declarations: (decl * decl list) Nonempty.t
+      } (** Mutually-recursive LF type family declaration *)
+
+    | Theorem of
+      { location: Location.t
+      ; theorems: thm_decl Nonempty.t
+      } (** Mutually recursive theorem declaration(s) *)
+
+    | Val of
+      { location: Location.t
+      ; identifier: name
+      ; typ: Comp.typ option
+      ; expression: Comp.exp_syn
+      } (** Computation-level value declaration *)
+
+    | Query of
+      { location: Location.t
+      ; name: name option
+      ; typ: LF.typ
+      ; expected_solutions: int option
+      ; maximum_tries: int option
+      } (** Logic programming query on LF type *)
+
+    | Module of
+      { location: Location.t
+      ; identifier: string
+      ; declarations: decl list
+      } (** Namespace declaration for other declarations *)
+
+    | Comment of
+      { location: Location.t
+      ; content: string
+      } (** Documentation comment *)
+
+  (** Parsed Beluga project *)
   type sgn = decl list
+
 end
diff --git a/src/core/synint.ml b/src/core/synint.ml
index 4735de258..3b4bced6f 100644
--- a/src/core/synint.ml
+++ b/src/core/synint.ml
@@ -4,8 +4,6 @@ open Support
 
 open Id
 
-module Loc = Location
-
 (* Internal LF Syntax *)
 module LF = struct
   include Syncom.LF
@@ -32,7 +30,7 @@ module LF = struct
     | DeclOpt of name * plicity
 
   and typ =                                     (* LF level                       *)
-    | Atom of Loc.t * cid_typ * spine           (* A ::= a M1 ... Mn              *)
+    | Atom of Location.t * cid_typ * spine           (* A ::= a M1 ... Mn              *)
     | PiTyp of (typ_decl * depend) * typ        (*   | Pi x:A.B                   *)
     | Sigma of typ_rec
     | TClo of (typ * sub)                       (*   | TClo(A,s)                  *)
@@ -42,11 +40,11 @@ module LF = struct
      a hole (_) so that when printing, it can be reproduced correctly.
    *)
   and normal =                                  (* normal terms                   *)
-    | Lam of Loc.t * name * normal              (* M ::= \x.M                     *)
-    | Root of Loc.t * head * spine * plicity    (*   | h . S                      *)
-    | LFHole of Loc.t * HoleId.t * HoleId.name
+    | Lam of Location.t * name * normal              (* M ::= \x.M                     *)
+    | Root of Location.t * head * spine * plicity    (*   | h . S                      *)
+    | LFHole of Location.t * HoleId.t * HoleId.name
     | Clo of (normal * sub)                     (*   | Clo(N,s)                   *)
-    | Tuple of Loc.t * tuple
+    | Tuple of Location.t * tuple
 
   (* TODO: Heads ought to carry their location.
      Erasure currently needs to invent / pretend that a different
@@ -220,7 +218,7 @@ module LF = struct
       carry a location.
    *)
   let head (tH : head) : normal =
-    Root (Loc.ghost, tH, Nil, `explicit)
+    Root (Location.ghost, tH, Nil, `explicit)
 
   let mvar cvar sub : head =
     MVar (cvar, sub)
@@ -382,12 +380,12 @@ module Comp = struct
   include Syncom.Comp
 
   type kind =
-    | Ctype of Loc.t
-    | PiKind of Loc.t * LF.ctyp_decl * kind
+    | Ctype of Location.t
+    | PiKind of Location.t * LF.ctyp_decl * kind
 
   type meta_typ = LF.ctyp
 
-  type meta_obj = Loc.t * LF.mfront
+  type meta_obj = Location.t * LF.mfront
 
   type meta_spine =
     | MetaNil
@@ -395,19 +393,19 @@ module Comp = struct
                  * meta_spine * plicity
 
   type typ =
-    | TypBase of Loc.t * cid_comp_typ * meta_spine
-    | TypCobase of Loc.t * cid_comp_cotyp * meta_spine
-    | TypDef of Loc.t * cid_comp_typ * meta_spine
-    | TypBox of Loc.t * meta_typ
-    | TypArr of Loc.t * typ * typ
-    | TypCross of Loc.t * typ * typ
-    | TypPiBox of Loc.t * LF.ctyp_decl * typ
+    | TypBase of Location.t * cid_comp_typ * meta_spine
+    | TypCobase of Location.t * cid_comp_cotyp * meta_spine
+    | TypDef of Location.t * cid_comp_typ * meta_spine
+    | TypBox of Location.t * meta_typ
+    | TypArr of Location.t * typ * typ
+    | TypCross of Location.t * typ * typ
+    | TypPiBox of Location.t * LF.ctyp_decl * typ
     | TypClo of typ *  LF.msub
     | TypInd of typ
 
   type suffices_typ = typ generic_suffices_typ
 
-  let rec loc_of_typ : typ -> Loc.t =
+  let rec loc_of_typ : typ -> Location.t =
     function
     | TypBase (l, _, _) | TypCobase (l, _, _) | TypDef (l, _, _)
       | TypBox (l, _) | TypArr (l, _, _) | TypCross (l, _, _)
@@ -415,7 +413,7 @@ module Comp = struct
        l
     | TypClo (tau, _) | TypInd tau -> loc_of_typ tau
 
-  let loc_of_suffices_typ : suffices_typ -> Loc.t =
+  let loc_of_suffices_typ : suffices_typ -> Location.t =
     function
     | `exact tau -> loc_of_typ tau
     | `infer loc -> loc
@@ -449,45 +447,45 @@ module Comp = struct
   type ihctx = ih_decl LF.ctx
 
   and exp_chk =
-    | Syn        of Loc.t * exp_syn
-    | Fn         of Loc.t * name * exp_chk
-    | Fun        of Loc.t * fun_branches
-    | MLam       of Loc.t * name * exp_chk * plicity
-    | Pair       of Loc.t * exp_chk * exp_chk
-    | LetPair    of Loc.t * exp_syn * (name * name * exp_chk)
-    | Let        of Loc.t * exp_syn * (name * exp_chk)
-    | Box        of Loc.t * meta_obj * meta_typ (* type annotation used for pretty-printing *)
-    | Case       of Loc.t * case_pragma * exp_syn * branch list
-    | Impossible of Loc.t * exp_syn
-    | Hole       of Loc.t * HoleId.t * HoleId.name
+    | Syn        of Location.t * exp_syn
+    | Fn         of Location.t * name * exp_chk
+    | Fun        of Location.t * fun_branches
+    | MLam       of Location.t * name * exp_chk * plicity
+    | Pair       of Location.t * exp_chk * exp_chk
+    | LetPair    of Location.t * exp_syn * (name * name * exp_chk)
+    | Let        of Location.t * exp_syn * (name * exp_chk)
+    | Box        of Location.t * meta_obj * meta_typ (* type annotation used for pretty-printing *)
+    | Case       of Location.t * case_pragma * exp_syn * branch list
+    | Impossible of Location.t * exp_syn
+    | Hole       of Location.t * HoleId.t * HoleId.name
 
   and exp_syn =
-    | Var       of Loc.t * offset
-    | DataConst of Loc.t * cid_comp_const
-    | Obs       of Loc.t * exp_chk * LF.msub * cid_comp_dest
-    | Const     of Loc.t * cid_prog
-    | Apply     of Loc.t * exp_syn * exp_chk
-    | MApp      of Loc.t * exp_syn * meta_obj * meta_typ (* annotation for printing *)
+    | Var       of Location.t * offset
+    | DataConst of Location.t * cid_comp_const
+    | Obs       of Location.t * exp_chk * LF.msub * cid_comp_dest
+    | Const     of Location.t * cid_prog
+    | Apply     of Location.t * exp_syn * exp_chk
+    | MApp      of Location.t * exp_syn * meta_obj * meta_typ (* annotation for printing *)
                    * plicity
     | AnnBox    of meta_obj * meta_typ
-    | PairVal   of Loc.t * exp_syn * exp_syn
+    | PairVal   of Location.t * exp_syn * exp_syn
 
   and pattern =
-    | PatMetaObj of Loc.t * meta_obj
-    | PatConst of Loc.t * cid_comp_const * pattern_spine
-    | PatFVar of Loc.t * name (* used only _internally_ by coverage *)
-    | PatVar of Loc.t * offset
-    | PatPair of Loc.t * pattern * pattern
-    | PatAnn of Loc.t * pattern * typ * plicity
+    | PatMetaObj of Location.t * meta_obj
+    | PatConst of Location.t * cid_comp_const * pattern_spine
+    | PatFVar of Location.t * name (* used only _internally_ by coverage *)
+    | PatVar of Location.t * offset
+    | PatPair of Location.t * pattern * pattern
+    | PatAnn of Location.t * pattern * typ * plicity
 
   and pattern_spine =
     | PatNil
-    | PatApp of Loc.t * pattern * pattern_spine
-    | PatObs of Loc.t * cid_comp_dest * LF.msub * pattern_spine
+    | PatApp of Location.t * pattern * pattern_spine
+    | PatObs of Location.t * cid_comp_dest * LF.msub * pattern_spine
 
   and branch =
     | Branch
-      of Loc.t
+      of Location.t
          * LF.mctx (* branch prefix *)
          * (LF.mctx * gctx) (* branch contexts *)
          * pattern
@@ -495,8 +493,8 @@ module Comp = struct
          * exp_chk
 
   and fun_branches =
-   | NilFBranch of Loc.t
-   | ConsFBranch of Loc.t * (LF.mctx * gctx * pattern_spine * exp_chk) * fun_branches
+   | NilFBranch of Location.t
+   | ConsFBranch of Location.t * (LF.mctx * gctx * pattern_spine * exp_chk) * fun_branches
 
   type tclo = typ * LF.msub
 
@@ -524,7 +522,7 @@ module Comp = struct
   let rec apply_many i =
     function
     | [] -> i
-    | e :: es -> apply_many (Apply (Loc.ghost, i, e)) es
+    | e :: es -> apply_many (Apply (Location.ghost, i, e)) es
 
   let loc_of_exp_syn =
     function
@@ -655,7 +653,7 @@ module Comp = struct
   (* A proof is a sequence of statements ending either as a complete proof or an incomplete proof.*)
   type proof =
     | Incomplete (* hole *)
-      of Loc.t * proof_state
+      of Location.t * proof_state
     | Command of command * proof
     | Directive of directive (* which can end proofs or split into subgoals *)
 
@@ -705,7 +703,7 @@ module Comp = struct
          * typ (* The type of the scrutinee *)
          * context_branch list
 
-  and suffices_arg = Loc.t * typ * proof
+  and suffices_arg = Location.t * typ * proof
 
   and context_branch = context_case split_branch
   and meta_branch = meta_branch_label split_branch
@@ -738,7 +736,7 @@ module Comp = struct
   *)
   and hypothetical =
     Hypothetical
-    of Loc.t
+    of Location.t
        * hypotheses (* the full contexts *)
        * proof (* the proof; should make sense in `hypotheses`. *)
 
@@ -758,12 +756,12 @@ module Comp = struct
     }
 
   (** Smart constructor for an unfinished proof ending. *)
-  let incomplete_proof (l : Loc.t) (s : proof_state) : proof =
+  let incomplete_proof (l : Location.t) (s : proof_state) : proof =
     Incomplete (l, s)
 
   (** Smart constructor for the intros directive. *)
   let intros (h : hypotheses) (proof : proof) : proof =
-    Directive (Intros (Hypothetical (Loc.ghost, h, proof)))
+    Directive (Intros (Hypothetical (Location.ghost, h, proof)))
 
   let suffices (i : exp_syn) (ps : suffices_arg list) : proof =
     Directive (Suffices (i, ps))
@@ -779,7 +777,7 @@ module Comp = struct
 
   let context_branch (c : context_case) (cG_p, pat) (t : LF.msub) (h : hypotheses) (p : proof)
       : context_branch =
-    SplitBranch (c, (cG_p, pat), t, (Hypothetical (Loc.ghost, h, p)))
+    SplitBranch (c, (cG_p, pat), t, (Hypothetical (Location.ghost, h, p)))
 
   let meta_split (m : exp_syn) (a : typ) (bs : meta_branch list)
       : proof =
@@ -795,7 +793,7 @@ module Comp = struct
         (h : hypotheses)
         (p : proof)
       : meta_branch =
-    SplitBranch (c, (cG_p, pat), t, (Hypothetical (Loc.ghost, h, p)))
+    SplitBranch (c, (cG_p, pat), t, (Hypothetical (Location.ghost, h, p)))
 
   let comp_split (t : exp_syn) (tau : typ) (bs : comp_branch list)
       : proof =
@@ -808,7 +806,7 @@ module Comp = struct
         (h : hypotheses)
         (d : proof)
       : comp_branch =
-    SplitBranch (c, (cG_p, pat), t, (Hypothetical (Loc.ghost, h, d)))
+    SplitBranch (c, (cG_p, pat), t, (Hypothetical (Location.ghost, h, d)))
 
   (** Gives a more convenient way of writing complex proofs by using list syntax. *)
   let prepend_commands (cmds : command list) (proof : proof)
@@ -876,40 +874,118 @@ module Sgn = struct
   (* type positivity_flag =  *)
   (*   | Noflag *)
   (*   | Positivity *)
-  (*   | Stratify of Loc.t * Comp.order * name * (name option) list  *)
+  (*   | Stratify of Location.t * Comp.order * name * (name option) list  *)
 
 
   type positivity_flag =
     | Nocheck
     | Positivity
-    | Stratify of  Loc.t * int
-    | StratifyAll of Loc.t
+    | Stratify of  Location.t * int
+    | StratifyAll of Location.t
 
   type thm_decl =
     { thm_name : cid_prog
     ; thm_typ : Comp.typ
     ; thm_body : Comp.thm
-    ; thm_loc : Loc.t
+    ; thm_loc : Location.t
     }
 
+  (** Reconstructed signature element *)
   type decl =
-    | Typ           of Loc.t * cid_typ  * LF.kind
-    | Const         of Loc.t * cid_term * LF.typ
-    | CompTyp       of Loc.t * name * Comp.kind  *  positivity_flag
-    | CompCotyp     of Loc.t * name * Comp.kind
-    | CompConst     of Loc.t * name * Comp.typ
-    | CompDest      of Loc.t * name * LF.mctx * Comp.typ * Comp.typ
-    | CompTypAbbrev of Loc.t * name * Comp.kind * Comp.typ
-    | Schema        of cid_schema * LF.schema
-    | Theorem       of thm_decl list
-    | Proof         of Comp.typ * Comp.proof
-    | Pragma        of LF.prag
-    | Val           of Loc.t * name * Comp.typ * Comp.exp_chk * Comp.value option
-    | MRecTyp       of Loc.t * decl list list
-    | Module        of Loc.t * string * decl list
-    | Query         of Loc.t * name option * (LF.typ  * Id.offset) * int option * int option
-    | Comment       of Loc.t * string
-
+    | Typ of
+      { location: Location.t
+      ; identifier: cid_typ
+      ; kind: LF.kind
+      } (** LF type family declaration *)
+
+    | Const of
+      { location: Location.t
+      ; identifier: cid_term
+      ; typ: LF.typ
+      } (** LF type constant decalaration *)
+
+    | CompTyp of
+      { location: Location.t
+      ; identifier: name
+      ; kind: Comp.kind
+      ; positivity_flag: positivity_flag
+      } (** Computation-level data type constant declaration *)
+
+    | CompCotyp of
+      { location: Location.t
+      ; identifier: name
+      ; kind: Comp.kind
+      } (** Computation-level codata type constant declaration *)
+
+    | CompConst of
+      { location: Location.t
+      ; identifier: name
+      ; typ: Comp.typ
+      } (** Computation-level type constructor declaration *)
+
+    | CompDest of
+      { location: Location.t
+      ; identifier: name
+      ; mctx: LF.mctx
+      ; observation_typ: Comp.typ
+      ; return_typ: Comp.typ
+      } (** Computation-level type destructor declaration *)
+
+    | CompTypAbbrev of
+      { location: Location.t
+      ; identifier: name
+      ; kind: Comp.kind
+      ; typ: Comp.typ
+      } (** Synonym declaration for computation-level type *)
+
+    | Schema of
+      { location: Location.t
+      ; identifier: cid_schema
+      ; schema: LF.schema
+      } (** Declaration of a specification for a set of contexts *)
+
+    | Theorem of
+      { location: Location.t
+      ; theorems: thm_decl Nonempty.t
+      } (** Mutually recursive theorem declaration(s) *)
+
+    | Pragma of
+      { pragma: LF.prag
+      } (** Compiler directive *)
+
+    | Val of
+      { location: Location.t
+      ; identifier: name
+      ; typ: Comp.typ
+      ; expression: Comp.exp_chk
+      ; expression_value: Comp.value option
+      } (** Computation-level value declaration *)
+
+    | MRecTyp of
+      { location: Location.t
+      ; declarations: decl list Nonempty.t
+      } (** Mutually-recursive LF type family declaration *)
+
+    | Module of
+      { location: Location.t
+      ; identifier: string
+      ; declarations: decl list
+      } (** Namespace declaration for other declarations *)
+
+    | Query of
+      { location: Location.t
+      ; name: name option
+      ; typ: (LF.typ * Id.offset)
+      ; expected_solutions: int option
+      ; maximum_tries: int option
+      } (** Logic programming query on LF type *)
+
+    | Comment of
+      { location: Location.t
+      ; content: string
+      } (** Documentation comment *)
+
+  (** Reconstructed Beluga project *)
   type sgn = decl list
 
 end
diff --git a/src/core/typeinfo.ml b/src/core/typeinfo.ml
index 59bc927da..59eefb21b 100644
--- a/src/core/typeinfo.ml
+++ b/src/core/typeinfo.ml
@@ -1,13 +1,10 @@
 open Support.Equality
 open Support
-module Loc = Syntax.Int.Loc
 module P = Pretty.Int.DefaultPrinter
 
 let generate_annotations = ref false;
 
 module Annot = struct
-  open Syntax.Int
-
   type entry =
     { typ : string
     }
@@ -26,8 +23,8 @@ module Annot = struct
     { typ
     }
 
-  let add (l : Loc.t) (e : entry) =
-    (* dprint (fun () -> "[TypeInfo.Annot] Entry of " ^ e.typ ^ " added at: \n" ^ Syntax.Loc.to_string l ^ "\n");  *)
+  let add (l : Location.t) (e : entry) =
+    (* dprint (fun () -> "[TypeInfo.Annot] Entry of " ^ e.typ ^ " added at: \n" ^ Location.to_string l ^ "\n");  *)
     Hashtbl.replace store l e
   let get = Hashtbl.find store
   let clear () = Hashtbl.clear store
@@ -35,24 +32,24 @@ module Annot = struct
 
   let output_int pp i = output_string pp (string_of_int i)
 
-  let print_position (pp : out_channel) (pos : Loc.pos) (name : string) : unit =
+  let print_position (pp : out_channel) (pos : Location.pos) (name : string) : unit =
     output_string pp "\"";
     output_string pp (String.escaped name);
     output_string pp "\" ";
-    output_int pp (Loc.position_line pos);
+    output_int pp (Location.position_line pos);
     output_char pp ' ';
-    output_int pp (Loc.position_bol pos);
+    output_int pp (Location.position_bol pos);
     output_char pp ' ';
-    output_int pp (Loc.position_column pos)
+    output_int pp (Location.position_column pos)
 
-  let print_location (pp : out_channel) (loc : Loc.t) (name : string) : unit =
-    let start_pos = Loc.start_position loc in
-    let end_pos = Loc.stop_position loc in
+  let print_location (pp : out_channel) (loc : Location.t) (name : string) : unit =
+    let start_pos = Location.start_position loc in
+    let end_pos = Location.stop_position loc in
     print_position pp start_pos name;
     output_char pp ' ';
     print_position pp end_pos name
 
-  let print_one (pp : out_channel) (name : string) (typtup : Loc.t * entry) : unit =
+  let print_one (pp : out_channel) (name : string) (typtup : Location.t * entry) : unit =
     let (loc, entry) = typtup in
     let tp = entry.typ in
     print_location pp loc name;
@@ -62,7 +59,7 @@ module Annot = struct
 
   let print_annot pp (name : string) : unit =
     let sorted =
-      let cmp l1 l2 = Loc.start_offset l1 - Loc.start_offset l2 in
+      let cmp l1 l2 = Location.start_offset l1 - Location.start_offset l2 in
       let l = Hashtbl.fold (fun k v acc -> (k, v) :: acc) store [] in
       List.sort (fun (key1, _) (key2, _) -> cmp key1 key2) l
     in
@@ -87,11 +84,11 @@ module LF = struct
     ; tc = t
     }
 
-  let add (l : Loc.t) (e : entry) (_ : string) =
-    if not (Loc.is_ghost l)
+  let add (l : Location.t) (e : entry) (_ : string) =
+    if not (Location.is_ghost l)
     then
       begin
-        (* dprint (fun () -> "[TypeInfo.LF] Entry of " ^ P.typToString e.ctx e.psi e.tc ^ " added at: \n" ^ Syntax.Loc.to_string l ^ "\n"); *)
+        (* dprint (fun () -> "[TypeInfo.LF] Entry of " ^ P.typToString e.ctx e.psi e.tc ^ " added at: \n" ^ Location.to_string l ^ "\n"); *)
         Fmt.stringify (P.fmt_ppr_lf_typ e.ctx e.psi P.l0) (Whnf.normTyp e.tc)
         |> Annot.mk_entry
         |> Annot.add l;
@@ -115,11 +112,11 @@ module Comp = struct
     ; tc = t
     }
 
-  let add (l : Loc.t) (e : entry) (_ : string) =
-    if not (Loc.is_ghost l)
+  let add (l : Location.t) (e : entry) (_ : string) =
+    if not (Location.is_ghost l)
     then
       begin
-        (* dprint (fun () -> "[TypeInfo.Comp] Entry of " ^ P.subCompTypToString e.ctx e.tc ^ " added at: \n" ^ Syntax.Loc.to_string l ^ "\n"); *)
+        (* dprint (fun () -> "[TypeInfo.Comp] Entry of " ^ P.subCompTypToString e.ctx e.tc ^ " added at: \n" ^ Location.to_string l ^ "\n"); *)
         Fmt.stringify (P.fmt_ppr_cmp_typ e.ctx P.l0) (Whnf.cnormCTyp e.tc)
         |> Annot.mk_entry
         |> Annot.add l;
@@ -143,8 +140,8 @@ module Sgn = struct
     { sgn = decl
     }
 
-  let add (l : Loc.t) (e : entry) (_ : string) : unit =
-    if not (Loc.is_ghost l)
+  let add (l : Location.t) (e : entry) (_ : string) : unit =
+    if not (Location.is_ghost l)
     then
       begin
         begin
@@ -158,7 +155,7 @@ module Sgn = struct
         |> Annot.add l;
         Hashtbl.add store l e
       end
-  let get : Loc.t -> entry = Hashtbl.find store
+  let get : Location.t -> entry = Hashtbl.find store
   let clear () : unit = Hashtbl.clear store
 end
 
@@ -173,18 +170,18 @@ let print_annot (name : string) : unit =
 
 let type_of_position (line : int) (col : int) : string =
   let sorted =
-    let cmp l1 l2 = Loc.start_offset l1 - Loc.start_offset l2 in
+    let cmp l1 l2 = Location.start_offset l1 - Location.start_offset l2 in
     let l = Hashtbl.fold (fun k v acc -> (k, v) :: acc) Annot.store [] in
     List.sort (fun (key1, _) (key2, _) -> cmp key1 key2) l
   in
-  (* let f (l, _) = print_string ((string_of_int (Loc.start_off l)) ^ ", " ^ (string_of_int (Loc.stop_off l)) ^ "\n") in
+  (* let f (l, _) = print_string ((string_of_int (Location.start_off l)) ^ ", " ^ (string_of_int (Location.stop_off l)) ^ "\n") in
   List.iter f sorted; *)
   let contains_pos (l, x) : bool =
-    let start_c = Loc.start_offset l - Loc.start_bol l in
-    let end_c = Loc.stop_offset l - Loc.stop_bol l in
-    let start_l = Loc.start_line l in
-    let end_l = Loc.stop_line l in
-    (* Format.printf "(%d, %d), (%d, %d), %s\n" (Loc.start_line l) start_c (Loc.stop_line l) end_c x.Annot.typ; *)
+    let start_c = Location.start_offset l - Location.start_bol l in
+    let end_c = Location.stop_offset l - Location.stop_bol l in
+    let start_l = Location.start_line l in
+    let end_l = Location.stop_line l in
+    (* Format.printf "(%d, %d), (%d, %d), %s\n" (Location.start_line l) start_c (Location.stop_line l) end_c x.Annot.typ; *)
     if (start_l = line) && (end_l = line)
     then (start_c <= col) && (col <= end_c)
     else if (start_l = line) && (line < end_l)
diff --git a/src/core/typeinfo.mli b/src/core/typeinfo.mli
index c73c5496d..09832cb80 100644
--- a/src/core/typeinfo.mli
+++ b/src/core/typeinfo.mli
@@ -1,3 +1,5 @@
+open Support
+
 val generate_annotations : bool ref
 val print_annot : string -> unit
 val clear_all : unit -> unit
@@ -8,11 +10,11 @@ module Annot : sig
     { typ : string
     }
 
-  val store : (Syntax.Int.Loc.t, entry) Hashtbl.t
+  val store : (Location.t, entry) Hashtbl.t
   val mk_entry : string -> entry
 
-  val add : Syntax.Int.Loc.t -> entry -> unit
-  val get : Syntax.Int.Loc.t -> entry
+  val add : Location.t -> entry -> unit
+  val get : Location.t -> entry
   val clear : unit -> unit
   val to_string : entry -> string
 end
@@ -26,8 +28,8 @@ module LF : sig
 
   val mk_entry : Syntax.Int.LF.mctx -> Syntax.Int.LF.dctx -> Syntax.Int.LF.tclo -> entry
 
-  val add : Syntax.Int.Loc.t -> entry -> string -> unit
-  val get : Syntax.Int.Loc.t -> entry
+  val add : Location.t -> entry -> string -> unit
+  val get : Location.t -> entry
   val clear : unit -> unit
 end
 
@@ -39,8 +41,8 @@ module Comp : sig
 
   val mk_entry : Syntax.Int.LF.mctx -> Syntax.Int.Comp.tclo -> entry
 
-  val add : Syntax.Int.Loc.t -> entry -> string -> unit
-  val get : Syntax.Int.Loc.t -> entry
+  val add : Location.t -> entry -> string -> unit
+  val get : Location.t -> entry
   val clear : unit -> unit
 end
 
@@ -53,7 +55,7 @@ module Sgn : sig
 
   val mk_entry : typ_or_kind -> entry
 
-  val add : Syntax.Int.Loc.t -> entry -> string -> unit
-  val get : Syntax.Int.Loc.t -> entry
+  val add : Location.t -> entry -> string -> unit
+  val get : Location.t -> entry
   val clear : unit -> unit
 end
diff --git a/src/core/whnf.ml b/src/core/whnf.ml
index bb93ae645..0f8225de9 100644
--- a/src/core/whnf.ml
+++ b/src/core/whnf.ml
@@ -23,7 +23,7 @@ module T = Store.Cid.Typ
 exception Fmvar_not_found
 exception FreeMVar of head
 exception NonInvertible
-exception InvalidLFHole of Loc.t
+exception InvalidLFHole of Location.t
 
 let m_id = MShift 0
 
diff --git a/src/core/whnf.mli b/src/core/whnf.mli
index 6f6cc6fc4..37f7497d8 100644
--- a/src/core/whnf.mli
+++ b/src/core/whnf.mli
@@ -2,7 +2,7 @@
    @author Brigitte Pientka
    modified: Joshua Dunfield
 *)
-
+open Support
 open Syntax.Int.LF
 open Syntax.Int
 
@@ -63,13 +63,13 @@ val raiseType : dctx -> typ -> typ
 
 val etaExpandMV : dctx -> tclo -> Id.name -> sub -> depend -> normal
 
-val etaExpandMMV : Syntax.Loc.t -> mctx -> dctx -> tclo -> Id.name -> sub -> depend -> normal
+val etaExpandMMV : Location.t -> mctx -> dctx -> tclo -> Id.name -> sub -> depend -> normal
 
 
 exception Fmvar_not_found
 exception FreeMVar of head
 exception NonInvertible
-exception InvalidLFHole of Loc.t
+exception InvalidLFHole of Location.t
 
 val newMTypName : ctyp -> Id.name_guide
 
@@ -227,10 +227,10 @@ val lowerTyp : dctx -> tclo -> dctx * tclo
 
 (** Converts an MMVar to a contextual object according to its
     contextual type. *)
-val mmVarToClObj : Loc.t -> mm_var -> cltyp -> clobj
+val mmVarToClObj : Location.t -> mm_var -> cltyp -> clobj
 
 (** Converts an MMVar to a meta object according to its meta type. *)
-val mmVarToMFront : Loc.t -> mm_var -> Comp.meta_typ -> mfront
+val mmVarToMFront : Location.t -> mm_var -> Comp.meta_typ -> mfront
 
-val dotMMVar : Loc.t -> mctx -> msub -> Id.name * ctyp * depend
+val dotMMVar : Location.t -> mctx -> msub -> Id.name * ctyp * depend
                -> Comp.meta_obj * msub
diff --git a/src/harpoon/prover.ml b/src/harpoon/prover.ml
index 04ccb9dc2..c25b4c645 100644
--- a/src/harpoon/prover.ml
+++ b/src/harpoon/prover.ml
@@ -247,7 +247,7 @@ let process_command
          "There is no theorem by name %a."
          Id.print name
 
-  | Command.Rename (x_src, x_dst, level) ->
+  | Command.Rename { rename_from=x_src; rename_to=x_dst; level } ->
      if not (Theorem.rename_variable x_src x_dst level t g) then
        Error.(throw (NoSuchVariable (x_src, level)))
 
diff --git a/src/harpoon/serialization.ml b/src/harpoon/serialization.ml
index 758858380..12043e188 100644
--- a/src/harpoon/serialization.ml
+++ b/src/harpoon/serialization.ml
@@ -107,17 +107,17 @@ let replace_locs (replacees : (Loc.t * (Format.formatter -> unit -> unit)) list)
        end
 
 let update_existing_holes existing_holes =
-  let open Option in
   existing_holes
-  |> filter_map
-       begin fun (loc, ps) ->
-       let open Comp in
-       !(ps.solution)
-       $> fun p ->
-          ( loc
-          , fun fmt _ -> P.fmt_ppr_cmp_proof ps.context.cD ps.context.cG fmt p
-          )
-       end
+  |> List.filter_map
+      begin fun (loc, ps) ->
+        let open Option in
+        let open Comp in
+        !(ps.solution)
+        $> fun p ->
+           ( loc
+           , fun fmt _ -> P.fmt_ppr_cmp_proof ps.context.cD ps.context.cG fmt p
+           )
+      end
   |> replace_locs
 
 let append_sessions target_file_name new_mutual_rec_thmss =
diff --git a/src/harpoon/state.ml b/src/harpoon/state.ml
index b1eee827c..4bde78c0b 100644
--- a/src/harpoon/state.ml
+++ b/src/harpoon/state.ml
@@ -46,7 +46,7 @@ let recover_theorem ppf hooks (cid, gs) =
   let initial_state =
     let s =
       make_proof_state SubgoalPath.start
-        ( Total.annotate Loc.ghost decl.Comp.order tau
+        ( Total.annotate Location.ghost decl.Comp.order tau
         , Whnf.m_id )
     in
     let prf =
diff --git a/src/harpoon/tactic.ml b/src/harpoon/tactic.ml
index 18986081b..29a7aed44 100644
--- a/src/harpoon/tactic.ml
+++ b/src/harpoon/tactic.ml
@@ -269,7 +269,7 @@ let split (k : Command.split_kind) (i : Comp.exp_syn) (tau : Comp.typ) mfs : t =
             meta-context, accounting for dependent pattern matching on
             `m`. *)
          Reconstruct.synPatRefine
-           Loc.ghost
+           Location.ghost
            (Reconstruct.case_type (lazy pat) i)
            (s.context.cD, cD)
            t
@@ -410,15 +410,15 @@ let split (k : Command.split_kind) (i : Comp.exp_syn) (tau : Comp.typ) mfs : t =
        | PatMetaObj (_, (_, LF.CObj cPsi)) ->
           let case_label =
             match cPsi with
-            | LF.Null -> EmptyContext Loc.ghost
-            | LF.(DDec _) -> ExtendedBy (Loc.ghost, k)
+            | LF.Null -> EmptyContext Location.ghost
+            | LF.(DDec _) -> ExtendedBy (Location.ghost, k)
             | _ -> B.Error.violation "[get_context_branch] pattern not a context"
           in
           let label =
             Comp.SubgoalPath.build_context_split i case_label
           in
           let g' = new_state label in
-          let p = incomplete_proof Loc.ghost g' in
+          let p = incomplete_proof Location.ghost g' in
           ( g'
           , context_branch case_label (cG_p, pat) theta context p
           )
@@ -447,7 +447,7 @@ let split (k : Command.split_kind) (i : Comp.exp_syn) (tau : Comp.typ) mfs : t =
           in
           let label = Comp.SubgoalPath.build_meta_split i c in
           let g' = new_state label in
-          let p = incomplete_proof Loc.ghost g' in
+          let p = incomplete_proof Location.ghost g' in
           ( g'
           , meta_branch c (cG_p, pat) theta context p
           )
@@ -461,7 +461,7 @@ let split (k : Command.split_kind) (i : Comp.exp_syn) (tau : Comp.typ) mfs : t =
             Comp.SubgoalPath.build_comp_split i cid
           in
           let g' = new_state label in
-          let p = incomplete_proof Loc.ghost g' in
+          let p = incomplete_proof Location.ghost g' in
           ( g'
           , comp_branch cid (cG_p, pat) theta context p
           )
@@ -667,7 +667,7 @@ let suffices
             Comp.SubgoalPath.(append g.label (build_suffices i_head k))
         }
       in
-      (new_state, (Loc.ghost, tau, incomplete_proof Loc.ghost new_state))
+      (new_state, (Location.ghost, tau, incomplete_proof Location.ghost new_state))
       end
     |> List.split
   in
diff --git a/src/replay/headStrict.ml b/src/replay/headStrict.ml
index 9e1e6d5d0..d88b3aee9 100644
--- a/src/replay/headStrict.ml
+++ b/src/replay/headStrict.ml
@@ -17,7 +17,7 @@ let rec unfold (seed : 's) (next : 's -> ('a * 's) option) : 'a t option =
 
 (** Converts any basic stream into a head-strict stream.
     Since the basic stream might be empty, the return type is in an
-    {!Pervasives.option}.
+    {!Stdlib.option}.
  *)
 module OfBasicStream (S : Types.BasicStream) = struct
   let f (s : 'a S.t) : 'a t option =
diff --git a/src/replay/mupc.ml b/src/replay/mupc.ml
index 6ee75edfa..5d9b5c2ef 100644
--- a/src/replay/mupc.ml
+++ b/src/replay/mupc.ml
@@ -58,7 +58,7 @@ module type Base = sig
   val throw : string -> 'a t
 
   (** A parser that observes the head of the input, returning
-  {!Pervasives.None} if the parser has reached the end of the input. *)
+  {!Stdlib.None} if the parser has reached the end of the input. *)
   val peek : item Token.t option t
 
   (** A variant of {!Mupc.peek} that throws an
diff --git a/src/replay/mupc.mli b/src/replay/mupc.mli
index f73258977..34d95ad41 100644
--- a/src/replay/mupc.mli
+++ b/src/replay/mupc.mli
@@ -74,7 +74,7 @@ module type Base = sig
   val throw : string -> 'a t
 
   (** A parser that observes the head of the input, returning
-  {!Pervasives.None} if the parser has reached the end of the input. *)
+  {!Stdlib.None} if the parser has reached the end of the input. *)
   val peek : item Token.t option t
 
   (** A variant of {!Mupc.peek} that throws an
diff --git a/src/replay/span.mli b/src/replay/span.mli
index 4176371d1..b01abb4df 100644
--- a/src/replay/span.mli
+++ b/src/replay/span.mli
@@ -16,7 +16,7 @@ exception InvalidSpan
 
 (** Constructs a span from a pair of locations.
     If the second location comes before the first, then the result is
-    {!Pervasives.None}.
+    {!Stdlib.None}.
  *)
 val of_pair : Loc.t -> Loc.t -> t option
 
diff --git a/src/support/either.mli b/src/support/either.mli
index 860caaf6e..205149a7c 100644
--- a/src/support/either.mli
+++ b/src/support/either.mli
@@ -44,18 +44,18 @@ val void : ('e, 'a) t -> (unit, unit) t
  *)
 val bind : ('a -> ('e, 'b) t) -> ('e, 'a) t -> ('e, 'b) t
 
-(** Eliminates the union into a {!Pervasives.option}, forgetting the value in
+(** Eliminates the union into a {!Stdlib.option}, forgetting the value in
 the left-hand side. *)
 val forget : ('e, 'a) t -> 'a option
 
-(** Converts a {!Pervasives.option} into a union with a unit left-hand
+(** Converts a {!Stdlib.option} into a union with a unit left-hand
     side.
  *)
 val of_option : 'a option -> (unit, 'a) t
 
-(** Converts a {!Pervasives.option} into a union with a left-hand side
-    constructed from a thunk in case the {!Pervasives.option}
-    contained {!Option.Nothing}.
+(** Converts a {!Stdlib.option} into a union with a left-hand side
+    constructed from a thunk in case the {!Stdlib.option}
+    contained {!Option.None}.
  *)
 val of_option' : (unit -> 'e) -> 'a option -> ('e, 'a) t
 
diff --git a/src/support/list.ml b/src/support/list.ml
index cc86dfd88..8f3049631 100644
--- a/src/support/list.ml
+++ b/src/support/list.ml
@@ -23,10 +23,6 @@ let filter_rev p l =
   in
   go [] l
 
-let for_each l f = map f l
-
-let for_each_ l f = iter f l
-
 let uncons = function
   | [] -> None
   | x :: xs -> Some (x, xs)
@@ -67,7 +63,7 @@ let mapi2 f l1 l2 =
     | [], [] -> return []
     | x :: xs, y :: ys ->
       mapi2 (index + 1) xs ys (fun tl -> return (f index x y :: tl))
-    | _ -> raise (Invalid_argument "mapi2")
+    | _ -> raise (Invalid_argument "List.mapi2")
   in
   mapi2 0 l1 l2 Fun.id
 
@@ -79,3 +75,21 @@ let rec drop n = function
 let ap xs = map2 (fun x f -> f x) xs
 
 let ap_one x = map (fun f -> f x)
+
+let split l =
+  let rec split l return =
+    match l with
+    | [] -> return ([], [])
+    | (x, y) :: l -> split l (fun (xs, ys) -> return (x :: xs, y :: ys))
+  in
+  split l Fun.id
+
+let combine l1 l2 =
+  let rec combine l1 l2 return =
+    match l1, l2 with
+    | [], [] -> return []
+    | a1 :: l1, a2 :: l2 ->
+      combine l1 l2 (fun rest -> return ((a1, a2) :: rest))
+    | _ -> raise (Invalid_argument "List.combine")
+  in
+  combine l1 l2 Fun.id
diff --git a/src/support/list.mli b/src/support/list.mli
index ffcd5cdb9..7257ec920 100644
--- a/src/support/list.mli
+++ b/src/support/list.mli
@@ -25,14 +25,6 @@ val nonempty : 'a list -> bool
 *)
 val filter_rev : ('a -> bool) -> 'a list -> 'a list
 
-(** [for_each l f] is [map f l].
-*)
-val for_each : 'a list -> ('a -> 'b) -> 'b list
-
-(** [for_each_ l f] is [iter f l]
-*)
-val for_each_ : 'a list -> ('a -> unit) -> unit
-
 (** [uncons l] is [Some (hd l, tl l)] if [l <> []] and [None] otherwise.
 *)
 val uncons : 'a list -> ('a * 'a list) option
@@ -82,9 +74,22 @@ val mapi2 : (int -> 'a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
 val drop : int -> 'a list -> 'a list
 
 (** [ap [x1; x2; ...; xn] [f1; f2; ...; fn]] is [[f1 x1; f2 x2; ...; fn xn]].
+    @raise Invalid_argument if the two lists are determined to have different
+    lengths.
 *)
 val ap : 'a list -> ('a -> 'b) list -> 'b list
 
 (** [ap_one x [f1; f2; ...; fn]] is [[f1 x; f2 x; ...; fn x]].
 *)
 val ap_one : 'a -> ('a -> 'b) list -> 'b list
+
+(** Transform a list of pairs into a pair of lists:
+    [split [(a1, b1); ...; (an, bn)]] is [([a1; ...; an], [b1; ...; bn])].
+*)
+val split : ('a * 'b) list -> 'a list * 'b list
+
+(** Transform a pair of lists into a list of pairs:
+   [combine [a1; ...; an] [b1; ...; bn]] is [[(a1, b1); ...; (an, bn)]].
+   @raise Invalid_argument if the two lists have different lengths.
+*)
+val combine : 'a list -> 'b list -> ('a * 'b) list
diff --git a/src/support/misc.ml b/src/support/misc.ml
index 93df7e083..23eaec89d 100644
--- a/src/support/misc.ml
+++ b/src/support/misc.ml
@@ -17,8 +17,8 @@ exception NotImplemented of string
 let not_implemented (msg : string) : 'a = raise (NotImplemented msg)
 
 (** Enumerates a list using a state transformer to generate indices.
-    The initial seed {!s!} contains the initial state and the function
-    {!f!} transforms this state to compute a new state and an index.
+    The initial seed [s] contains the initial state and the function
+    [f] transforms this state to compute a new state and an index.
     These indices are sequentially zipped with the given list to
     produce an indexed list, and the final state is returned.
  *)
diff --git a/src/support/nonempty.ml b/src/support/nonempty.ml
index ecc0f9d90..c169a69a6 100644
--- a/src/support/nonempty.ml
+++ b/src/support/nonempty.ml
@@ -26,7 +26,9 @@ let rec last (h, t) =
 
 let length (_, l) = 1 + List.length l
 
-let from x l = x , l
+let from x l = x, l
+
+let singleton x = x, []
 
 let rec fold_right f g (h, l) =
   match l with
@@ -36,6 +38,8 @@ let rec fold_right f g (h, l) =
 let fold_left (type a) (type b) (f : a -> b) (g : b -> a -> b) (x, l) =
   List.fold_left g (f x) l
 
+let destructure f l = f (head l) (tail l)
+
 let of_list (l : 'a list) : 'a t option =
   match l with
   | [] -> None
@@ -53,7 +57,19 @@ let to_list ((x, l) : 'a t) : 'a list =
   x :: l
 
 let map (f : 'a -> 'b) (x, l : 'a t) : 'b t =
-  (f x, List.map f l)
+  let h = f x in
+  let t = List.map f l in
+  h, t
+
+let map2 f (h1, t1) (h2, t2) =
+  f h1 h2, List.map2 f t1 t2
+
+let filter_map f (h, t) =
+  let rest = List.filter_map f t in
+  f h
+  |> Option.fold
+    ~none:rest
+    ~some:(fun h -> h :: rest)
 
 let iter (f : 'a -> unit) (x, l : 'a t) : unit =
   List.iter f (x :: l)
@@ -91,7 +107,7 @@ let group_by (p : 'a -> 'key) (l : 'a list) : ('key * 'a t) list =
       DynArray.add d x;
       Hashtbl.replace h k d
     in
-    List.for_each_ l (fun x -> insert (p x) x)
+    List.iter (fun x -> insert (p x) x) l
   in
   (* The use of unsafe_of_list here is justified because every
      dynarray we create has one element added immediately to it, and is
@@ -101,6 +117,21 @@ let group_by (p : 'a -> 'key) (l : 'a list) : ('key * 'a t) list =
   |> Seq.map (Pair.rmap Fun.(unsafe_of_list ++ DynArray.to_list))
   |> Seq.to_list
 
+let split ((x, y), t) =
+  let (xs, ys) = List.split t in
+  (x, xs), (y, ys)
+
+let combine (a, l1) (b, l2) =
+  ((a, b), List.combine l1 l2)
+
+let partition f (h, l) =
+  let (l1, l2) = List.partition f l in
+  if f h then (h :: l1, l2) else (l1, h :: l2)
+
+let ap xs = map2 (fun x f -> f x) xs
+
+let ap_one x = map (fun f -> f x)
+
 module Syntax = struct
   let ($>) (p : 'a t) (f : 'a -> 'b) : 'b t =
     map f p
diff --git a/src/support/nonempty.mli b/src/support/nonempty.mli
index 8cc177582..e3a191308 100644
--- a/src/support/nonempty.mli
+++ b/src/support/nonempty.mli
@@ -13,6 +13,9 @@ val last : 'a t -> 'a
 (** Constructs a nonempty list given an element. *)
 val from : 'a -> 'a list -> 'a t
 
+(** [singleton e] is the non-empty list with the single element [e] in it. *)
+val singleton : 'a -> 'a t
+
 (** Elimination principle for `Nonempty.t'. *)
 val fold_right : ('a -> 'b) (* for the Sing case *) ->
                  ('a -> 'b -> 'b) (* for the Cons case *) ->
@@ -25,6 +28,11 @@ val fold_left : ('a -> 'b) (* for the Sing case *) ->
                 'a t ->
                 'b
 
+(** [destructure f l] is [f h t], where [h] and [t] are the head and tail of [l]
+    respectively.
+*)
+val destructure : ('a -> 'a list -> 'b) -> 'a t -> 'b
+
 (** Counts the number of elements in the nonempty list. *)
 val length : 'a t -> int
 
@@ -37,6 +45,18 @@ val to_list : 'a t -> 'a list
 (** Maps a function over the nonempty list. *)
 val map : ('a -> 'b) -> 'a t -> 'b t
 
+(** [map2 f (a1, [a2; ...; an]) (b1, [b2; ...; bn])] is
+    [(f a1 b1, [f a2 b2; ...; f an bn])].
+    @raise Invalid_argument if the two lists are determined to have different
+    lengths.
+*)
+val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
+
+(** [filter_map f l] applies [f] to every element of [l], filters out the [None]
+    elements and returns the list of the arguments of the [Some] elements.
+*)
+val filter_map : ('a -> 'b option) -> 'a t -> 'b list
+
 (** Runs an effectful function over the nonempty list. *)
 val iter : ('a -> unit) -> 'a t -> unit
 
@@ -75,6 +95,38 @@ val print : ?pp_sep:(Format.formatter -> unit -> unit) ->
             'a t ->
             unit
 
+(** Transform a non-empty list of pairs into a pair of non-empty lists:
+    [split ((a1, b1), [(a2, b2); ...; (an, bn)])] is
+    [(a1, [a2; ...; an]), (b1, [b2; ...; bn])].
+*)
+val split : ('a * 'b) t -> 'a t * 'b t
+
+(** Transform a pair of lists into a list of pairs:
+    [combine (a1, [a2; ...; an]) (b1, [b2; ...; bn])] is
+    [((a1, b1), [(a2, b2); ...; (an, bn)])].
+    @raise Invalid_argument if the two lists have different lengths.
+*)
+val combine : 'a t -> 'b t -> ('a * 'b) t
+
+(** [partition f l] returns a pair of lists [(l1, l2)], where [l1] is the list
+    of all the elements of [l] that satisfy the predicate [f], and [l2] is the
+    list of all the elements of [l] that do not satisfy [f]. The order of
+    elements in the input list is preserved. At least one of [l1] and [l2] is
+    non-empty.
+*)
+val partition : ('a -> bool) -> 'a t -> 'a list * 'a list
+
+(** [ap (x1, [x2; ...; xn]) (f1, [f2; ...; fn])] is
+    [(f1 x1, [f2 x2; ...; fn xn])].
+    @raise Invalid_argument if the two lists are determined to have different
+    lengths.
+*)
+val ap : 'a t -> ('a -> 'b) t -> 'b t
+
+(** [ap_one x (f1, [f2; ...; fn])] is [(f1 x, [f2 x; ...; fn x])].
+*)
+val ap_one : 'a -> ('a -> 'b) t -> 'b t
+
 module Syntax : sig
   val ($>) : 'a t -> ('a -> 'b) -> 'b t
 end
diff --git a/src/support/option.ml b/src/support/option.ml
index 7964bedd0..5c4354521 100644
--- a/src/support/option.ml
+++ b/src/support/option.ml
@@ -85,17 +85,8 @@ let ( &> ) (o : 'a option) (o' : 'b option) : 'b option =
 let void (o : 'a option) : unit option =
   o $> fun _ -> ()
 
-let rec filter_map (f : 'a -> 'b option) (l : 'a list) : 'b list =
-  match l with
-  | [] -> []
-  | x :: xs ->
-     f x
-     |> eliminate
-       (fun () -> filter_map f xs)
-       (fun y -> y :: filter_map f xs)
-
 let cat_options (l : 'a option list) : 'a list =
-  filter_map Fun.id l
+  List.filter_map Fun.id l
 
 (** Specialized effectful eliminator for option types. *)
 let when_some (l : 'a option) (f : 'a -> unit) : unit =
diff --git a/src/support/option.mli b/src/support/option.mli
index 81bd8e21c..3ffd2fe6b 100644
--- a/src/support/option.mli
+++ b/src/support/option.mli
@@ -59,14 +59,6 @@ val ( &> ) : 'a option -> 'b option -> 'b option
 
 val void : 'a option -> unit option
 
-(**
- * Applies a transformation to a list that may fail, removing failed results.
- * Side-effects are guaranteed to run from left to right.
- * This is the same as composing `List.map` with `cat_options`, but
- * incurs only one traversal of the list.
- *)
-val filter_map : ('a -> 'b option) -> 'a list -> 'b list
-
 (**
  * Removes all `None` options from the list.
  *
diff --git a/t/code/error/total/nonrecursive/dst.bel.out b/t/code/error/total/nonrecursive/dst.bel.out
index ec90a8a8c..aba126b81 100644
--- a/t/code/error/total/nonrecursive/dst.bel.out
+++ b/t/code/error/total/nonrecursive/dst.bel.out
@@ -1,3 +1,3 @@
 ./t/code/error/total/nonrecursive/dst.bel, line 7, column 7:
 Type-checking error.
-A recursive call to nonrecursive fucntion bad2 is forbidden.
+A recursive call to nonrecursive function bad2 is forbidden.