diff --git a/builtin-doc/coq-builtin-synterp.elpi b/builtin-doc/coq-builtin-synterp.elpi
index 49d420f9a..ac3e63422 100644
--- a/builtin-doc/coq-builtin-synterp.elpi
+++ b/builtin-doc/coq-builtin-synterp.elpi
@@ -90,12 +90,15 @@ external func attributes -> list attribute.
 external pred get-option o:string, o:A.
 
 % The data type of arguments (for commands or tactics)
-kind argument type.
+kind elaborated.argument type.
+typeabbrev argument elaborated.argument.
 external symbol int      : int    -> argument. % Eg. 1 -2.
 external symbol str      : string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 external symbol trm      : term   -> argument. % Eg. (t).
 external symbol open-trm : int -> term -> argument.
 
+external symbol syntactic : syntactic.argument -> argument.
+
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").
 %
@@ -423,6 +426,46 @@ external symbol node : list attribute -> attribute-value = "1".
 kind attribute type.
 external symbol attribute : string -> attribute-value -> attribute = "1". 
 
+% Unprocessed command argument
+kind syntactic.argument type.
+external symbol syntactic.str : string -> syntactic.argument = "1". 
+external symbol syntactic.int : int -> syntactic.argument = "1". 
+external symbol syntactic.trm : syntactic.trm -> syntactic.argument = "1". 
+external symbol syntactic.const-decl : syntactic.const-decl ->
+                                       syntactic.argument = "1". 
+external symbol syntactic.indt-decl : syntactic.indt-decl ->
+                                      syntactic.argument = "1". 
+external symbol syntactic.record-decl : syntactic.record-decl ->
+                                        syntactic.argument = "1". 
+external symbol syntactic.ctx-decl : syntactic.context-decl ->
+                                     syntactic.argument = "1". 
+
+% Unprocessed term argument
+kind syntactic.trm type.
+
+
+% Unprocessed term argument
+kind syntactic.const-decl type.
+
+
+% Unprocessed term argument
+kind syntactic.indt-decl type.
+
+
+% Unprocessed term argument
+kind syntactic.record-decl type.
+
+
+% Unprocessed term argument
+kind syntactic.context-decl type.
+
+
+% Syntactic scope delimiter depth
+kind syntactic.delimiter_depth type.
+
+external symbol syntactic.delimit-unbounded-scope : syntactic.delimiter_depth = "1".
+external symbol syntactic.delimit-only-tmp-scope : syntactic.delimiter_depth = "1".
+
 
 
 
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
index f142b6b5b..ea1dd0f20 100644
--- a/builtin-doc/coq-builtin.elpi
+++ b/builtin-doc/coq-builtin.elpi
@@ -63,12 +63,15 @@ external func attributes -> list attribute.
 external pred get-option o:string, o:A.
 
 % The data type of arguments (for commands or tactics)
-kind argument type.
+kind elaborated.argument type.
+typeabbrev argument elaborated.argument.
 external symbol int      : int    -> argument. % Eg. 1 -2.
 external symbol str      : string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 external symbol trm      : term   -> argument. % Eg. (t).
 external symbol open-trm : int -> term -> argument.
 
+external symbol syntactic : syntactic.argument -> argument.
+
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").
 %
@@ -480,6 +483,7 @@ macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt.
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 
+macro @no-coercion! :- get-option "coq:no_coercion" tt. % ignore coercions during pretyping
 
 macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance
 
@@ -1480,7 +1484,9 @@ external func coq.unify-leq term, term -> diagnostic.
 % hole. Similarly universe levels present in T are disregarded.
 % Supported attributes:
 % - @keepunivs! (default false, do not disregard universe levels)
-% - @no-tc! (default false, do not infer typeclasses) 
+% - @no-tc! (default false, do not infer typeclasses)
+% - @no-coercion! (default: false, do not insert coercions)
+% 
 external func coq.elaborate-skeleton term -> term, term, diagnostic.
 
 % [coq.elaborate-ty-skeleton T U E Diagnostic] elabotares T expecting it to
@@ -2290,6 +2296,81 @@ external symbol coq.pp.nl : coq.pp = "1".
 % - @ppwidth! N (default 80, max line length)
 external func coq.pp->string coq.pp -> string.
 
+% Unprocessed command argument
+kind syntactic.argument type.
+external symbol syntactic.str : string -> syntactic.argument = "1". 
+external symbol syntactic.int : int -> syntactic.argument = "1". 
+external symbol syntactic.trm : syntactic.trm -> syntactic.argument = "1". 
+external symbol syntactic.const-decl : syntactic.const-decl ->
+                                       syntactic.argument = "1". 
+external symbol syntactic.indt-decl : syntactic.indt-decl ->
+                                      syntactic.argument = "1". 
+external symbol syntactic.record-decl : syntactic.record-decl ->
+                                        syntactic.argument = "1". 
+external symbol syntactic.ctx-decl : syntactic.context-decl ->
+                                     syntactic.argument = "1". 
+
+% Unprocessed term argument
+kind syntactic.trm type.
+
+
+% Unprocessed term argument
+kind syntactic.const-decl type.
+
+
+% Unprocessed term argument
+kind syntactic.indt-decl type.
+
+
+% Unprocessed term argument
+kind syntactic.record-decl type.
+
+
+% Unprocessed term argument
+kind syntactic.context-decl type.
+
+
+% Syntactic scope delimiter depth
+kind syntactic.delimiter_depth type.
+
+external symbol syntactic.delimit-unbounded-scope : syntactic.delimiter_depth = "1".
+external symbol syntactic.delimit-only-tmp-scope : syntactic.delimiter_depth = "1".
+
+% [syntactic.argument->elaborated.argument SyntaxArg Arg Diagnostic]
+% Elaborates the syntactic argument with the settings of
+% #[arguments(elaborated)]
+external func syntactic.argument->elaborated.argument syntactic.argument -> argument, 
+                                                     diagnostic.
+
+% [syntactic.argument->unelaborated.argument SyntaxArg Arg Diagnostic]
+% Elaborates the syntactic argument with the settings of
+% #[arguments(unelaborated)]
+external func syntactic.argument->unelaborated.argument syntactic.argument -> argument, 
+                                                       diagnostic.
+
+% [syntactic.push-scope SyntaxTerm DelimiterDepth ScopeName
+% ScopedSyntaxTerm] Pushes the scope ScopeName on top of SyntaxTerm.
+external func syntactic.push-scope syntactic.trm, 
+                                  syntactic.delimiter_depth, 
+                                  string -> syntactic.trm.
+
+% [syntactic.elaborate SyntacticTerm TypeConstraint Term Diagnostic]
+% 
+% Elaborates SyntaxTerm using TypeConstraint (if provided).
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+% - @no-coercion! (default: false, do not insert coercions)
+% 
+external func syntactic.elaborate syntactic.trm, term -> term, diagnostic.
+
+% [syntactic.elaborate-ty SyntacticTerm Term Diagnostic] 
+% Elaborates SyntaxTerm as a Type.
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+% - @no-coercion! (default: false, do not insert coercions)
+% 
+external func syntactic.elaborate-ty syntactic.trm -> term, diagnostic.
+
 
 
 
diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi
index 3c16f2399..951e0c427 100644
--- a/elpi/coq-HOAS.elpi
+++ b/elpi/coq-HOAS.elpi
@@ -308,6 +308,7 @@ macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt.
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 
+macro @no-coercion! :- get-option "coq:no_coercion" tt. % ignore coercions during pretyping
 
 macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance
 
diff --git a/elpi/coq-arg-HOAS.elpi b/elpi/coq-arg-HOAS.elpi
index 25f96d79b..8376e00bd 100644
--- a/elpi/coq-arg-HOAS.elpi
+++ b/elpi/coq-arg-HOAS.elpi
@@ -48,12 +48,15 @@ external func attributes -> list attribute.
 external pred get-option o:string, o:A.
 
 % The data type of arguments (for commands or tactics)
-kind argument type.
+kind elaborated.argument type.
+typeabbrev argument elaborated.argument.
 external symbol int      : int    -> argument. % Eg. 1 -2.
 external symbol str      : string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 external symbol trm      : term   -> argument. % Eg. (t).
 external symbol open-trm : int -> term -> argument.
 
+external symbol syntactic : syntactic.argument -> argument.
+
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").
 %
diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml
index 196704c80..bf9029c78 100644
--- a/src/rocq_elpi_HOAS.ml
+++ b/src/rocq_elpi_HOAS.ml
@@ -311,6 +311,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  no_coercion: bool option;
   algunivs : bool option;
 }
 let default_options () = {
@@ -330,15 +331,16 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
+  no_coercion = None;
   algunivs = None;
 }
 let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
   ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
-  ~redflags ~no_tc ~algunivs =
+  ~redflags ~no_tc ~no_coercion ~algunivs =
   let user_warns = Some UserWarn.{ depr; warn } in
   { hoas_holes; local; user_warns; primitive; failsafe; ppwidth; pp;
     pplevel; using; inline; uinstance; universe_decl; reversible; keepunivs;
-    redflags; no_tc; algunivs; }
+    redflags; no_tc; no_coercion; algunivs; }
 let make_warn = UserWarn.make_warn
 
 type 'a coq_context = {
@@ -1314,12 +1316,13 @@ let get_options ~depth hyps state =
     let universe_decl = get_universe_decl () in
     let reversible = get_bool_option "coq:reversible" in
     let no_tc = get_bool_option "coq:no_tc" in
+    let no_coercion = get_bool_option "coq:no_coercion" in
     let keepunivs = get_bool_option "coq:keepunivs" in
     let redflags = get_redflags_option () in
     let algunivs = get_bool_option "coq:keepalgunivs" in
     make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
       ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
-      ~redflags ~no_tc ~algunivs
+      ~redflags ~no_tc ~no_coercion ~algunivs
 let mk_coq_context ~options state =
   let env = get_global_env state in
   let section = section_ids env in
diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli
index 1cbdf4701..ed9233dc6 100644
--- a/src/rocq_elpi_HOAS.mli
+++ b/src/rocq_elpi_HOAS.mli
@@ -48,6 +48,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  no_coercion: bool option;
   algunivs : bool option;
 }
 
diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml
index 53272ed61..55ddeabab 100644
--- a/src/rocq_elpi_arg_HOAS.ml
+++ b/src/rocq_elpi_arg_HOAS.ml
@@ -4,7 +4,12 @@
 
 module API = Elpi.API
 module E = API.RawData
+module CC = API.ContextualConversion
+module C = API.Conversion
+module D = API.OpaqueData
 module CD = API.RawOpaqueData
+module Alg = API.AlgebraicData
+module P  = API.RawPp
 
 open Rocq_elpi_utils
 open Rocq_elpi_HOAS
@@ -59,20 +64,39 @@ let drop_relevance (a,_,c,d,e) = (a,c,d,e)
 let intern_global_context_synterp (ctx : Constrexpr.local_binder_expr list) : Glob_term.glob_decl list =
   CList.concat_map intern_one ctx |> List.rev
 
+module GS = struct
+  type 'a t = {
+    gs : Genintern.glob_sign;
+    vl : 'a
+  }
+  let get {vl;_} = vl
+  let mk gs vl = {gs; vl}
+end
+
+module IS = struct
+  type 'a t = {
+    is : Geninterp.interp_sign;
+    gs : Genintern.glob_sign;
+    vl : 'a
+  }
+  let get {vl;_} = vl
+  let mk is gs vl = {is; gs; vl}
+  let of_gs is GS.{gs; vl} = {is; gs; vl}
+end
+
 module Cmd = struct
 
 type raw_term = Constrexpr.constr_expr
-type glob_term = Genintern.glob_constr_and_expr
-type top_term =
-  Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr
+type glob_term = raw_term GS.t
+type top_term = raw_term IS.t
 
 type raw_record_decl = Vernacentries.Preprocessed_Mind_decl.record
-type glob_record_decl = Genintern.glob_sign * raw_record_decl
-type top_record_decl = Geninterp.interp_sign * glob_record_decl
+type glob_record_decl = raw_record_decl GS.t
+type top_record_decl = raw_record_decl IS.t
 
 type raw_indt_decl = Vernacentries.Preprocessed_Mind_decl.inductive
-type glob_indt_decl = Genintern.glob_sign * raw_indt_decl
-type top_indt_decl = Geninterp.interp_sign * glob_indt_decl
+type glob_indt_decl = raw_indt_decl GS.t
+type top_indt_decl = raw_indt_decl IS.t
 
 type univpoly = Mono | Poly | CumulPoly
 
@@ -147,8 +171,8 @@ type glob_constant_decl_elpi = {
   typ : Glob_term.glob_constr;
   body : Glob_term.glob_constr option;
 }
-type glob_constant_decl = Genintern.glob_sign * raw_constant_decl
-type top_constant_decl = Geninterp.interp_sign * glob_constant_decl
+type glob_constant_decl = raw_constant_decl GS.t
+type top_constant_decl = raw_constant_decl IS.t
 
 let pr_raw_constant_decl _ _ _ = Pp.str "TODO: pr_raw_constant_decl"
 let pr_glob_constant_decl _ _ _ = Pp.str "TODO: pr_glob_constant_decl"
@@ -156,8 +180,8 @@ let pr_top_constant_decl _ _ _ = Pp.str "TODO: pr_top_constant_decl"
 
 
 type raw_context_decl = Constrexpr.local_binder_expr list
-type glob_context_decl = Genintern.glob_sign * raw_context_decl
-type top_context_decl = Geninterp.interp_sign * glob_context_decl
+type glob_context_decl = raw_context_decl GS.t
+type top_context_decl = raw_context_decl IS.t
 
 let pr_raw_context_decl _ _ _ = Pp.str "TODO: pr_raw_context_decl"
 let pr_glob_context_decl _ _ _ = Pp.str "TODO: pr_glob_context_decl"
@@ -172,19 +196,37 @@ type ('a,'b,'c,'d,'e) t =
   | ConstantDecl : 'd    -> ('a,'b,'c,'d,'e) t
   | Context : 'e         -> ('a,'b,'c,'d,'e) t
 
+let map (type a b c d e v w x y z) :
+  (a -> v) -> (b -> w) -> (c -> x) -> (d -> y) -> (e -> z) ->
+  (a,b,c,d,e) t -> (v,w,x,y,z) t = fun f g h i j -> function
+  | Int _ as x -> x
+  | String _ as x -> x
+  | Term s -> Term (f s)
+  | RecordDecl s -> RecordDecl (g s)
+  | IndtDecl s -> IndtDecl (h s)
+  | ConstantDecl s -> ConstantDecl (i s)
+  | Context c -> Context (j c)
+let inj (type a b c d e v) :
+  (int -> v) ->
+  (string -> v) ->
+  (a -> v) -> (b -> v) -> (c -> v) -> (d -> v) -> (e -> v) ->
+  (a,b,c,d,e) t -> v = fun f0 f1 f g h i j -> function
+  | Int x -> f0 x
+  | String x -> f1 x
+  | Term s -> (f s)
+  | RecordDecl s -> (g s)
+  | IndtDecl s -> (h s)
+  | ConstantDecl s -> (i s)
+  | Context c -> (j c)
+
 type raw  = (raw_term,  raw_record_decl,  raw_indt_decl,  raw_constant_decl,  raw_context_decl)  t
 type glob = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl, glob_context_decl) t
 type top  = (top_term,  top_record_decl,  top_indt_decl,  top_constant_decl,  top_context_decl)  t
 
-let pr_arg f g h i j x = match x with
-| Int n -> Pp.int n
-| String s -> Pp.qstring s
-| Term s -> f s
-| RecordDecl s -> g s
-| IndtDecl s -> h s
-| ConstantDecl s -> i s
-| Context c -> j c
+let raw_of_glob : glob -> raw = map GS.get GS.get GS.get GS.get GS.get
+let raw_of_top : top -> raw = map IS.get IS.get IS.get IS.get IS.get
 
+let pr_arg f g h i j x = inj Pp.int Pp.qstring f g h i j x
 let pp_raw env sigma : raw -> Pp.t =
   pr_arg
     (Ppconstr.pr_constr_expr env sigma)
@@ -200,21 +242,11 @@ let pr_glob_constr_and_expr env sigma = function
     Printer.pr_glob_constr_env env sigma c
 
 let pp_glob env sigma : glob -> Pp.t =
-  pr_arg
-    (pr_glob_constr_and_expr env sigma)
-    (pr_glob_record_decl env sigma)
-    (pr_glob_indt_decl env sigma)
-    (pr_glob_constant_decl env sigma)
-    (pr_glob_context_decl env sigma)
-    
+  fun g -> g |> raw_of_glob |> pp_raw env sigma
+
 let pp_top env sigma : top -> Pp.t =
-  pr_arg
-    (fun (_,x) -> pr_glob_constr_and_expr env sigma x)
-    (pr_top_record_decl env sigma)
-    (pr_top_indt_decl env sigma)
-    (pr_top_constant_decl env sigma)
-    (pr_top_context_decl env sigma)
-    
+  fun g -> g |> raw_of_top |> pp_raw env sigma
+
 let sep_last_qualid = function
   | [] -> "_", []
   | l -> CList.sep_last l
@@ -326,7 +358,7 @@ let of_coq_record_definition id =
     univpoly = univpoly_of ~poly ~cumulative
   } 
 [%%endif]
-let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it
+let intern_record_decl glob_sign (it : raw_record_decl) = it
 
 let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z)
 let dest_entry (_,_,_,_,x) = x
@@ -477,7 +509,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
     List.map (fun (id,ty) -> id.CAst.v,
       intern_global_constr_ty ~expty:(Pretyping.OfType indty) glob_sign_params_self ~intern_env ty) constructors in
   { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
-let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it
+let intern_indt_decl glob_sign (it : raw_indt_decl) = it
 
 let expr_hole = CAst.make @@ Constrexpr.CHole(None)
 
@@ -488,7 +520,7 @@ let raw_context_decl_to_glob_synterp fields =
 let raw_context_decl_to_glob glob_sign fields =
   let _intern_env, fields = intern_global_context ~intern_env:Constrintern.empty_internalization_env glob_sign fields in
   List.rev fields
-let intern_context_decl glob_sign (it : raw_context_decl) = glob_sign, it
+let intern_context_decl glob_sign (it : raw_context_decl) = it
 
 let raw_decl_name_to_glob name =
   let name, space = sep_last_qualid name in
@@ -570,28 +602,15 @@ let raw_constant_decl_to_glob glob_sign ({ name; atts; udecl; typ = (params,typ)
         let state = merge_universe_context state ustate in
         state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in
   state, { name = raw_decl_name_to_glob name; params; typ; udecl; body }
-let intern_constant_decl glob_sign (it : raw_constant_decl) = glob_sign, it
+let intern_constant_decl glob_sign (it : raw_constant_decl) = it
 
-let glob glob_sign : raw -> glob = function
-  | Int _ as x -> x
-  | String _ as x -> x
-  | Term t -> Term (intern_tactic_constr glob_sign t)
-  | RecordDecl t -> RecordDecl (intern_record_decl glob_sign t)
-  | IndtDecl t -> IndtDecl (intern_indt_decl glob_sign t)
-  | ConstantDecl t -> ConstantDecl (intern_constant_decl glob_sign t)
-  | Context c -> Context (intern_context_decl glob_sign c)
+let glob glob_sign raw = glob_sign, raw
+let glob glob_sign : raw -> glob = map (GS.mk glob_sign) (GS.mk glob_sign) (GS.mk glob_sign) (GS.mk glob_sign) (GS.mk glob_sign)
 
 let subst _mod_subst _x =
   CErrors.anomaly Pp.(str "command arguments should not be substituted")
 
-let interp ist env evd : glob -> top = function
-  | Int _ as x -> x
-  | String _ as x -> x
-  | Term t -> Term(ist,t)
-  | RecordDecl t -> (RecordDecl(ist,t))
-  | IndtDecl t -> (IndtDecl(ist,t))
-  | ConstantDecl t -> (ConstantDecl(ist,t))
-  | Context c -> (Context(ist,c))
+let interp ist env evd : glob -> top = map (IS.of_gs ist) (IS.of_gs ist) (IS.of_gs ist) (IS.of_gs ist) (IS.of_gs ist)
 
 end
 
@@ -945,6 +964,15 @@ let tacc = E.Constants.declare_global_symbol "tac"
 let intc = E.Constants.declare_global_symbol "int"
 let ctxc = E.Constants.declare_global_symbol "ctx-decl"
 
+(* HACK: We just want to be able to mention this in other places. *)
+let arg_type = API.Conversion.{
+    ty = TyName "argument";
+    pp_doc = (fun fmt _ -> Format.fprintf fmt "<TODO>");
+    pp = (fun fmt _ -> Format.fprintf fmt "<TODO>");
+    embed = (fun ~depth state s -> state, s, []);
+    readback = (fun ~depth state s -> state, s, []);
+  }
+
 let my_cast_to_string v =
   let open Ltac_plugin in
   try Taccoerce.Value.cast (Genarg.topwit Stdarg.wit_string) v
@@ -1191,30 +1219,31 @@ let interp_mutual_inductive ~flags ~env ~uniform ~private_ind ?typing_flags ~ude
 [%%endif]
 
 
-let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) =
+let in_elpi_cmd_interpreted ~loc ~depth ~base ?calldepth ~kind coq_ctx state (x : Cmd.top) =
   let open Cmd in
   let hyps = [] in
-  match x with
-  | RecordDecl (_ist,(glob_sign,raw_rdecl)) when raw ->
+  match x, kind with
+  | _, Syntactic -> assert false
+  | RecordDecl IS.{is=_ist; gs=glob_sign; vl=raw_rdecl}, Unelaborated ->
       let raw_rdecl = of_coq_record_definition raw_rdecl in
       let glob_rdecl = raw_record_decl_to_glob glob_sign raw_rdecl in
       let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = grecord2lp ~loc ~base ~depth state glob_rdecl in
       state, t, []
-  | RecordDecl (_ist,(glob_sign,raw_rdecl)) ->
+  | RecordDecl IS.{is=_ist; gs=glob_sign; vl=raw_rdecl}, Elaborated ->
       let flags, udecl, primitive_proj, kind, records = dest_rdecl raw_rdecl in
       let flags = handle_template_polymorphism flags in
       (* Definitional type classes cannot be interpreted using this function (why?) *)
       let kind = if kind = Vernacexpr.Class true then Vernacexpr.Class false else kind in
       let e = interp_structure ~flags udecl kind ~primitive_proj records in
       record_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
-  | IndtDecl (_ist,(glob_sign,raw_indt)) when raw ->
+  | IndtDecl IS.{is=_ist; gs=glob_sign; vl=raw_indt}, Unelaborated ->
       let raw_indt = of_coq_inductive_definition raw_indt in
       let glob_indt = raw_indt_decl_to_glob glob_sign raw_indt in
       let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = ginductive2lp ~loc ~depth ~base state glob_indt in
       state, t, []
-  | IndtDecl (_ist,(glob_sign,raw_indt)) -> 
+  | IndtDecl IS.{is=_ist; gs=glob_sign; vl=raw_indt}, Elaborated ->
       let flags, udecl, typing_flags, uniform, private_ind, inductives = dest_idecl raw_indt in
       let flags = handle_template_polymorphism flags in
       let e =
@@ -1224,11 +1253,11 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) =
         | _ -> nYI "(HOAS) mutual inductives"
       in
       inductive_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
-  | ConstantDecl (_ist,(glob_sign,raw_cdecl)) when raw ->
+  | ConstantDecl IS.{is=_ist; gs=glob_sign; vl=raw_cdecl}, Unelaborated ->
       let state, glob_cdecl = raw_constant_decl_to_glob glob_sign raw_cdecl state in
       let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       cdecl2lp ~loc ~depth ~base state glob_cdecl
-  | ConstantDecl (_ist,(glob_sign,({ name; typ = (bl,_) } as raw_cdecl))) ->
+  | ConstantDecl IS.{is=_ist; gs=glob_sign; vl=({ name; typ = (bl,_) } as raw_cdecl)}, Elaborated ->
       let state, udecl, typ, body, gls0 =
         raw_constant_decl_to_constr ~depth coq_ctx state raw_cdecl in
       let state, typ, gls1 = constr2lp_closed ~depth ?calldepth coq_ctx E.no_constraints state typ in
@@ -1244,25 +1273,216 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) =
           let state, ud, gls3 = universe_decl.API.Conversion.embed ~depth state (NonCumul udecl) in
           state, E.mkApp ucdeclc c [body;typ;ud], gls0 @ gls1 @ gls2 @ gls3
       end
-  | Context (_ist,(glob_sign,raw_ctx)) when raw ->
+  | Context IS.{is=_ist; gs=glob_sign; vl=raw_ctx}, Unelaborated ->
       let glob_ctx = raw_context_decl_to_glob glob_sign raw_ctx in
       let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = do_context_glob ~loc glob_ctx ~depth ~base state in
       state, E.mkApp ctxc t [], []
-  | Context (_ist,(glob_sign,raw_ctx)) ->
+  | Context IS.{is=_ist; gs=glob_sign; vl=raw_ctx}, Elaborated ->
       let sigma, ctx = ComAssumption.interp_context coq_ctx.env (get_sigma state) raw_ctx in
       let state, gls0 = set_current_sigma ~depth state sigma in
       let state, t, gls1 = do_context_constr (upcast coq_ctx) E.no_constraints ctx ~depth state in
       state, E.mkApp ctxc t [], gls0 @ gls1
-  | Int x -> in_elpi_int_arg ~depth state x
-  | String x -> in_elpi_string_arg ~depth state x
-  | Term (ist,glob_or_expr) when raw ->
+  | Int x, _ -> in_elpi_int_arg ~depth state x
+  | String x, _ -> in_elpi_string_arg ~depth state x
+  | Term IS.{is=ist; gs=glob_sign; vl=constexpr}, Unelaborated ->
       let sigma = get_sigma state in
+      let glob_or_expr = intern_tactic_constr glob_sign constexpr in
       in_elpi_term_arg ~loc ~depth ~base state coq_ctx hyps sigma ist glob_or_expr
-  | Term (ist,glob_or_expr) ->
+  | Term IS.{is=ist; gs=glob_sign; vl=constexpr}, Elaborated ->
       let sigma = get_sigma state in
+      let glob_or_expr = intern_tactic_constr glob_sign constexpr in
       in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr
 
+
+module Syntactic = struct
+  open Cmd
+
+  module Tag = struct
+    (* The Non-trivial syntactic types do not have comparison functions. We
+       augment the data with a tag to use for sorting.
+    *)
+    type 'a t = {
+      is : Geninterp.interp_sign;
+      gs : Genintern.glob_sign;
+      vl : 'a;
+      tag : int;
+    }
+    let compare_tag {tag=n1;_} {tag=n2;_} = Int.compare n1 n2
+
+    let counter = ref 0
+
+    let fresh IS.{is;gs;vl} =
+      incr counter;
+      let tag = !counter in
+      {is;gs;vl;tag}
+
+    let drop_tag (type a) : a t -> a IS.t = fun {is;gs;vl;tag=_} -> IS.{is;gs;vl}
+
+  end
+
+  type res_term = raw_term Tag.t
+  type res_record_decl = raw_record_decl Tag.t
+  type res_indt_decl = raw_indt_decl Tag.t
+  type res_constant_decl = raw_constant_decl Tag.t
+  type res_context_decl = raw_context_decl Tag.t
+  type res  = (res_term, res_record_decl, res_indt_decl, res_constant_decl, res_context_decl)  t
+
+  let pp_res env sigma : res -> Pp.t = fun r ->
+    Cmd.map Tag.drop_tag Tag.drop_tag Tag.drop_tag Tag.drop_tag Tag.drop_tag r |> pp_top env sigma
+
+  (* We need an order on syntactic terms but Rocq offers nothing of the sort. So
+     we equip each term with a unique integer to decide what to return when the
+     glob constrs are not equal. *)
+  let trm, trm_type = CD.declare {
+      name = "syntactic.trm";
+      doc = "Unprocessed term argument";
+      pp = (fun fmt (t : res_term) ->
+          Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.Term t))));
+      compare = (fun (Tag.{tag=n1; vl=ce1} as t1) (Tag.{tag=n2; vl=ce2} as t2) ->
+          if Constrexpr_ops.constr_expr_eq ce1 ce2
+          then 0
+          else Tag.compare_tag t1 t2
+        );
+      hash =  (fun _ -> 0);
+      hconsed = false;
+      constants = [];
+    }
+
+  let constant_decl, constant_decl_type = CD.declare {
+      name = "syntactic.const-decl";
+      doc = "Unprocessed term argument";
+      pp = (fun fmt (t : res_constant_decl) ->
+          Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.ConstantDecl t))));
+      compare = Tag.compare_tag; (* we do not even try to compare these based on contents *)
+      hash =  (fun _ -> 0);
+      hconsed = false;
+      constants = [];
+    }
+
+  let indt_decl, indt_decl_type = CD.declare {
+      name = "syntactic.indt-decl";
+      doc = "Unprocessed term argument";
+      pp = (fun fmt (t : res_indt_decl) ->
+          Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.IndtDecl t))));
+      compare = Tag.compare_tag; (* we do not even try to compare these based on contents *)
+      hash =  (fun _ -> 0);
+      hconsed = false;
+      constants = [];
+    }
+
+  let record_decl, record_decl_type = CD.declare {
+      name = "syntactic.record-decl";
+      doc = "Unprocessed term argument";
+      pp = (fun fmt (t : res_record_decl) ->
+          Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.RecordDecl t))));
+      compare = Tag.compare_tag; (* we do not even try to compare these based on contents *)
+      hash =  (fun _ -> 0);
+      hconsed = false;
+      constants = [];
+    }
+
+  let context, context_type = CD.declare {
+      name = "syntactic.context-decl";
+      doc = "Unprocessed term argument";
+      pp = (fun fmt (t : res_context_decl) ->
+          Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.Context t))));
+      compare = Tag.compare_tag; (* we do not even try to compare these based on contents *)
+      hash =  (fun _ -> 0);
+      hconsed = false;
+      constants = [];
+    }
+
+  let arg_type = Alg.declare {
+      ty = TyName "syntactic.argument";
+      doc = "Unprocessed command argument";
+      pp = (fun fmt t -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty t)));
+      constructors = [
+        K("syntactic.str", "", A(API.BuiltInData.string, N),
+          B (fun s -> Cmd.String s),
+          M (fun ~ok ~ko -> function Cmd.String s -> ok s | _ -> ko ())
+         );
+        K("syntactic.int", "", A(API.BuiltInData.int, N),
+          B (fun s -> Cmd.Int s),
+          M (fun ~ok ~ko -> function Cmd.Int s -> ok s | _ -> ko ())
+         );
+        K("syntactic.trm", "", A(trm_type, N),
+          B (fun s -> Cmd.Term s),
+          M (fun ~ok ~ko -> function Cmd.Term s -> ok s | _ -> ko ())
+         );
+        K("syntactic.const-decl", "", A(constant_decl_type, N),
+          B (fun s -> Cmd.ConstantDecl s),
+          M (fun ~ok ~ko -> function Cmd.ConstantDecl s -> ok s | _ -> ko ())
+         );
+        K("syntactic.indt-decl", "", A(indt_decl_type, N),
+          B (fun s -> Cmd.IndtDecl s),
+          M (fun ~ok ~ko -> function Cmd.IndtDecl s -> ok s | _ -> ko ())
+         );
+        K("syntactic.record-decl", "", A(record_decl_type, N),
+          B (fun s -> Cmd.RecordDecl s),
+          M (fun ~ok ~ko -> function Cmd.RecordDecl s -> ok s | _ -> ko ())
+         );
+        K("syntactic.ctx-decl", "", A(context_type, N),
+          B (fun s -> Cmd.Context s),
+          M (fun ~ok ~ko -> function Cmd.Context s -> ok s | _ -> ko ())
+         );
+      ];
+    } |> CC.(!<)
+
+  let as_normal_arg = E.Constants.declare_global_symbol "syntactic"
+
+  let delimiter_depth = API.OpaqueData.declare {
+      name = "syntactic.delimiter_depth";
+      doc = "Syntactic scope delimiter depth";
+      pp = Constrexpr.(fun fmt -> function
+          | DelimOnlyTmpScope -> Format.fprintf fmt "DelimOnlyTmpScope"
+          | DelimUnboundedScope -> Format.fprintf fmt "DelimUnboundedScope");
+      compare = Stdlib.compare;
+      hash = Hashtbl.hash;
+      hconsed = true;
+      constants = [
+        ("syntactic.delimit-only-tmp-scope", DelimOnlyTmpScope);
+        ("syntactic.delimit-unbounded-scope", DelimUnboundedScope);
+      ];
+    }
+
+  let ml_data =
+    let open API.BuiltIn in
+    [MLData arg_type;
+     MLData trm_type;
+     MLData constant_decl_type;
+     MLData indt_decl_type;
+     MLData record_decl_type;
+     MLData context_type;
+     MLData delimiter_depth;
+    ]
+
+  let res_of_top : top -> res =
+    Cmd.map
+      Tag.fresh
+      Tag.fresh
+      Tag.fresh
+      Tag.fresh
+      Tag.fresh
+
+  let top_of_res : res -> top =
+    Cmd.map
+      Tag.drop_tag
+      Tag.drop_tag
+      Tag.drop_tag
+      Tag.drop_tag
+      Tag.drop_tag
+end
+
+let in_elpi_cmd ~loc ~depth ~base ?calldepth ~kind coq_ctx state(x : Cmd.top) : API.State.t * E.term * _ =
+  match kind with
+  | Syntactic ->
+    let state, res, extra_goals =
+      Syntactic.arg_type.embed ~depth state (Syntactic.res_of_top x)
+    in
+    state, E.mkApp Syntactic.as_normal_arg res [], extra_goals
+  | _ -> in_elpi_cmd_interpreted ~loc ~depth ~base ?calldepth ~kind coq_ctx state x
+
 type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geninterp.Val.t
 
 let in_coq_arg ~depth proof_context constraints state t =
diff --git a/src/rocq_elpi_arg_HOAS.mli b/src/rocq_elpi_arg_HOAS.mli
index 5dc033260..96aa13a8d 100644
--- a/src/rocq_elpi_arg_HOAS.mli
+++ b/src/rocq_elpi_arg_HOAS.mli
@@ -5,24 +5,47 @@
 open Elpi.API.RawData
 open Rocq_elpi_utils
 
+module API = Elpi.API
+module CD = Elpi.API.RawOpaqueData
+
 type phase = Interp | Synterp | Both
 type proof =
   | Begin of string option (* None = always, Some x only if #[x] present*)
   | End
 
+module GS : sig
+  type 'a t = {
+    gs : Genintern.glob_sign;
+    vl : 'a
+  }
+  val get : 'a t -> 'a
+  val mk : Genintern.glob_sign -> 'a -> 'a t
+end
+
+module IS : sig
+  type 'a t = {
+    is : Geninterp.interp_sign;
+    gs : Genintern.glob_sign;
+    vl : 'a
+  }
+  val get : 'a t -> 'a
+  val mk : Geninterp.interp_sign -> Genintern.glob_sign ->  'a -> 'a t
+  val of_gs : Geninterp.interp_sign -> 'a GS.t -> 'a t
+end
+
 module Cmd : sig
 
 type raw_term = Constrexpr.constr_expr
-type glob_term = Genintern.glob_constr_and_expr
-type top_term = Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr
+type glob_term = raw_term GS.t
+type top_term = raw_term IS.t
 
 type raw_record_decl = Vernacentries.Preprocessed_Mind_decl.record
-type glob_record_decl = Genintern.glob_sign * raw_record_decl
-type top_record_decl = Geninterp.interp_sign * glob_record_decl
+type glob_record_decl = raw_record_decl GS.t
+type top_record_decl = raw_record_decl IS.t
 
 type raw_indt_decl = Vernacentries.Preprocessed_Mind_decl.inductive
-type glob_indt_decl = Genintern.glob_sign * raw_indt_decl
-type top_indt_decl = Geninterp.interp_sign * glob_indt_decl
+type glob_indt_decl = raw_indt_decl GS.t
+type top_indt_decl = raw_indt_decl IS.t
 
 type raw_constant_decl = {
   name : qualified_name;
@@ -33,12 +56,12 @@ type raw_constant_decl = {
   red : Genredexpr.raw_red_expr option;
 }
 val pr_raw_constant_decl : Environ.env -> Evd.evar_map -> raw_constant_decl -> Pp.t
-type glob_constant_decl = Genintern.glob_sign * raw_constant_decl
-type top_constant_decl = Geninterp.interp_sign * glob_constant_decl
+type glob_constant_decl = raw_constant_decl GS.t
+type top_constant_decl = raw_constant_decl IS.t
 
 type raw_context_decl = Constrexpr.local_binder_expr list
-type glob_context_decl = Genintern.glob_sign * raw_context_decl
-type top_context_decl = Geninterp.interp_sign * glob_context_decl
+type glob_context_decl = raw_context_decl GS.t
+type top_context_decl = raw_context_decl IS.t
 
 type ('a,'b,'c,'d,'e) t =
   | Int : int            -> ('a,'b,'c,'d,'e) t
@@ -125,14 +148,56 @@ val in_elpi_tac_econstr :
   Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals
 
 (* for commands *)
+val arg_type : API.Data.term API.Conversion.t
+module Syntactic : sig
+  module Tag :
+    sig
+      type 'a t = {
+        is : Geninterp.interp_sign;
+        gs : Genintern.glob_sign;
+        vl : 'a;
+        tag : int;
+      }
+      val compare_tag : 'a t -> 'b t -> int
+      val counter : int ref
+      val fresh : 'a IS.t -> 'a t
+      val drop_tag : 'a t -> 'a IS.t
+    end
+  type res_term = Cmd.raw_term Tag.t
+  type res_record_decl = Cmd.raw_record_decl Tag.t
+  type res_indt_decl = Cmd.raw_indt_decl Tag.t
+  type res_constant_decl = Cmd.raw_constant_decl Tag.t
+  type res_context_decl = Cmd.raw_context_decl Tag.t
+  type res =
+      (res_term, res_record_decl, res_indt_decl, res_constant_decl,
+       res_context_decl)
+      Cmd.t
+  val pp_res : Environ.env -> Evd.evar_map -> res -> Pp.t
+  val trm : res_term CD.cdata
+  val trm_type : res_term API.Conversion.t
+  val constant_decl : res_constant_decl CD.cdata
+  val constant_decl_type : res_constant_decl API.Conversion.t
+  val indt_decl : res_indt_decl CD.cdata
+  val indt_decl_type : res_indt_decl API.Conversion.t
+  val record_decl : res_record_decl CD.cdata
+  val record_decl_type : res_record_decl API.Conversion.t
+  val context : res_context_decl CD.cdata
+  val context_type : res_context_decl API.Conversion.t
+  val arg_type : res API.Conversion.t
+  val delimiter_depth : Constrexpr.delimiter_depth API.Conversion.t
+  val as_normal_arg : API.RawData.constant
+  val res_of_top : Cmd.top -> res
+  val top_of_res : res -> Cmd.top
+  val ml_data : API.BuiltIn.declaration list
+end
 val in_elpi_cmd :
   loc:Loc.t ->
   depth:int ->
   base:Elpi.API.Compile.program ->
   ?calldepth:int -> 
+  kind:arg_kind ->
   Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.coq_context ->
   Elpi.API.State.t ->
-  raw:bool ->
   Cmd.top ->
   Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals
 val in_elpi_cmd_synterp :
diff --git a/src/rocq_elpi_arg_syntax.mlg b/src/rocq_elpi_arg_syntax.mlg
index c53267780..8b4bede0b 100644
--- a/src/rocq_elpi_arg_syntax.mlg
+++ b/src/rocq_elpi_arg_syntax.mlg
@@ -195,7 +195,21 @@ let skip_and_synterp_attributes = Attributes.Notations.(skip_attribute ++ synter
 let scope_and_skip_and_synterp_attributes = Attributes.Notations.(scope_attribute ++ skip_attribute ++ synterp_attribute)
 
 let raw_args_attributes =
-  Attributes.(qualify_attribute "arguments" (bool_attribute ~name:"raw"))
+  Attributes.qualify_attribute "arguments"
+    (Attributes.attribute_of_list
+      ["elaborated", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Elaborated
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"elaborated\" does not expect a value"));
+       "unelaborated", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Unelaborated
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"unelaborated\" does not expect a value"));
+       "raw", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Unelaborated
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"raw\" does not expect a value"));
+       "syntactic", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Syntactic
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"syntactic\" does not expect a value"));
+      ])    
 
 let validate_attributes a flags =
   let extra, raw_args = Attributes.parse_with_extra a flags in
diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml
index b09a73757..1f42c1428 100644
--- a/src/rocq_elpi_builtins.ml
+++ b/src/rocq_elpi_builtins.ml
@@ -27,6 +27,7 @@ open Names
 
 open Rocq_elpi_utils
 open Rocq_elpi_HOAS
+open Rocq_elpi_arg_HOAS
 
 let string_of_ppcmds options pp =
   let b = Buffer.create 512 in
@@ -1502,9 +1503,58 @@ let apply_proof ~name ~poly env tac pf =
   pv
 [%%endif]
 
+let syntactic_arg_to_arg api ~kind sarg diag ~depth coq_ctx _csts state =
+  let open API.BuiltIn in
+  let open Pred in
+  let open Notation in
+  let open CConv in
+  let open Syntactic in
+  let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
+  let base = Option.get (State.get base state) in
+  try
+    let state, res, extra_goals =
+      Syntactic.top_of_res sarg |>
+      Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind coq_ctx state
+    in
+    state, (!: res +! B.mkOK), extra_goals
+  with e ->
+    diag_error_lazy diag @@ fun () ->
+    let error =
+      string_of_ppcmds coq_ctx.options @@
+      try CErrors.print_no_report e with | _ -> Pp.(str api ++ str ": anomaly printing error")
+    in
+    state, ?: None +! B.mkERROR error, []
 
-
-
+let syntactic_arg_elaborate api t expected_type diag ~depth coq_ctx csts state =
+  let open API.BuiltIn in
+  let open Pred in
+  let open Notation in
+  let open CConv in
+  let open Syntactic in
+  let Tag.{is;gs;vl} = t in
+  let vl = Ltac_plugin.Tacintern.intern_constr gs vl in
+  let sigma = get_sigma state in
+  let flags =
+    let open Pretyping in
+    let flags = all_no_fail_flags in
+    let options = coq_ctx.options in
+    let use_typeclasses = if Option.default false options.no_tc then NoUseTC else UseTC in
+    let use_coercions = not @@ Option.default false options.no_coercion in
+    { flags with use_typeclasses; use_coercions }
+  in
+  try
+    let sigma, vl =
+      Ltac_plugin.Tacinterp.interp_open_constr ~flags ~expected_type is coq_ctx.env sigma vl
+    in
+    let state, extra_goals = set_current_sigma ~depth state sigma in
+    state, (!: vl +! B.mkOK), extra_goals
+  with e ->
+    diag_error_lazy diag @@ fun () ->
+    let error =
+      string_of_ppcmds coq_ctx.options @@
+      try CErrors.print_no_report e with | _ -> Pp.(str api ++ str ": anomaly printing error")
+    in
+    state, ?: None +! B.mkERROR error, []
 
 let coq_misc_builtins =
   let open API.BuiltIn in
@@ -3545,13 +3595,9 @@ Universe constraints are put in the constraint store.|})))),
        let state, assignments = set_current_sigma ~depth state sigma in
        state, r, assignments
      with Pretype_errors.PretypeError (env, sigma, err) ->
-       match diag with
-       | Data B.OK ->
-          (* optimization: don't print the error if caller wants OK *)
-          raise No_clause
-       | _ ->
-          let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
-          state, ?: None +! B.mkERROR error, [])),
+       diag_error_lazy diag @@ fun () ->
+       let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
+       state, ?: None +! B.mkERROR error, [])),
   DocAbove);
 
   MLCode(Pred("coq.typecheck-ty",
@@ -3579,13 +3625,9 @@ Universe constraints are put in the constraint store.|})))),
        let state, assignments = set_current_sigma ~depth state sigma in
        state, r, assignments
      with Pretype_errors.PretypeError (env, sigma, err) ->
-       match diag with
-       | Data B.OK ->
-          (* optimization: don't print the error if caller wants OK *)
-          raise No_clause
-       | _ ->
-          let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
-          state, ?: None +! B.mkERROR error, [])),
+       diag_error_lazy diag @@ fun () ->
+       let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
+       state, ?: None +! B.mkERROR error, [])),
   DocAbove);
 
   MLCode(Pred("coq.unify-eq",
@@ -3600,13 +3642,9 @@ Universe constraints are put in the constraint store.|})))),
        let state, assignments = set_current_sigma ~depth state sigma in
        state, !: B.mkOK, assignments
      with Pretype_errors.PretypeError (env, sigma, err) ->
-       match diag with
-       | Data B.OK ->
-          (* optimization: don't print the error if caller wants OK *)
-          raise No_clause
-       | _ ->
-          let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
-          state, !: (B.mkERROR error), [])),
+       diag_error_lazy diag @@ fun () ->
+       let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
+       state, !: (B.mkERROR error), [])),
   DocAbove);
 
   MLCode(Pred("coq.unify-leq",
@@ -3621,13 +3659,9 @@ Universe constraints are put in the constraint store.|})))),
        let state, assignments = set_current_sigma ~depth state sigma in
        state, !: B.mkOK, assignments
      with Pretype_errors.PretypeError (env, sigma, err) ->
-       match diag with
-       | Data B.OK ->
-          (* optimization: don't print the error if caller wants OK *)
-          raise No_clause
-       | _ ->
-          let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
-          state, !: (B.mkERROR error), [])),
+       diag_error_lazy diag @@ fun () ->
+       let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
+       state, !: (B.mkERROR error), [])),
   DocAbove);
 
    MLCode(Pred("coq.elaborate-skeleton",
@@ -3641,9 +3675,13 @@ not assigned even if the elaborated term has a term in place of the
 hole. Similarly universe levels present in T are disregarded.
 Supported attributes:
 - @keepunivs! (default false, do not disregard universe levels)
-- @no-tc! (default false, do not infer typeclasses) |}))))),
+- @no-tc! (default false, do not infer typeclasses)
+- @no-coercion! (default: false, do not insert coercions)
+|}))))),
   (fun gt ety _ diag ~depth proof_context _ state ->
-    let flags = if proof_context.options.no_tc = Some true then {(Pretyping.default_inference_flags false) with  use_typeclasses = NoUseTC} else Pretyping.default_inference_flags false in
+    let flags = Pretyping.default_inference_flags false in
+    let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in
+    let flags = if proof_context.options.no_coercion = Some true then {flags with use_coercions = false} else flags in
     try
       let sigma = get_sigma state in
       let ety_given, expected_type =
@@ -3670,13 +3708,9 @@ Supported attributes:
           let state, assignments = set_current_sigma ~depth state sigma in
           state, ?: None +! uj_val +! B.mkOK, assignments
     with Pretype_errors.PretypeError (env, sigma, err) ->
-       match diag with
-       | Data B.OK ->
-          (* optimization: don't print the error if caller wants OK *)
-          raise No_clause
-       | _ ->
-          let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
-          state, ?: None +? None +! B.mkERROR error, [])),
+      diag_error_lazy diag @@ fun () ->
+      let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
+      state, ?: None +? None +! B.mkERROR error, [])),
   DocAbove);
 
    MLCode(Pred("coq.elaborate-ty-skeleton",
@@ -3694,7 +3728,9 @@ Supported attributes:
   (fun gt es _ diag ~depth proof_context _ state ->
     try
       let sigma = get_sigma state in
-      let flags = if proof_context.options.no_tc = Some true then {(Pretyping.default_inference_flags false) with  use_typeclasses = NoUseTC} else Pretyping.default_inference_flags false in
+      let flags = Pretyping.default_inference_flags false in
+      let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in
+      let flags = if proof_context.options.no_coercion = Some true then {flags with use_coercions = false} else flags in
       let expected_type = Pretyping.IsType in
       let sigma = Evd.push_future_goals sigma in
       let sigma, uj_val, uj_type =
@@ -3704,13 +3740,9 @@ Supported attributes:
       let state, assignments = set_current_sigma ~depth state sigma in
       state, !: sort +! uj_val +! B.mkOK, assignments
     with Pretype_errors.PretypeError (env, sigma, err) ->
-       match diag with
-       | Data B.OK ->
-          (* optimization: don't print the error if caller wants OK *)
-          raise No_clause
-       | _ ->
-          let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
-          state, ?: None +? None +! B.mkERROR error, [])),
+      diag_error_lazy diag @@ fun () ->
+      let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
+      state, ?: None +? None +! B.mkERROR error, [])),
   DocAbove);
 
   LPDoc "-- Coq's reduction flags    ------------------------------------";
@@ -4410,5 +4442,76 @@ Supported attributes:
   DocAbove)
 
   ]
+  @ Syntactic.ml_data @
+  [MLCode(Pred("syntactic.argument->elaborated.argument",
+    In(Syntactic.arg_type, "SyntaxArg",
+    Out(Rocq_elpi_arg_HOAS.arg_type, "Arg",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(global, "Elaborates the syntactic argument with the settings of #[arguments(elaborated)]")))),
+    fun sarg _ diag ~depth coq_ctx _csts state ->
+      syntactic_arg_to_arg "syntactic.argument->elaborated.argument" ~kind:Elaborated sarg diag ~depth coq_ctx _csts state
+   ),
+   DocAbove);
+   MLCode(Pred("syntactic.argument->unelaborated.argument",
+    In(Syntactic.arg_type, "SyntaxArg",
+    Out(Rocq_elpi_arg_HOAS.arg_type, "Arg",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(global, "Elaborates the syntactic argument with the settings of #[arguments(unelaborated)]")))),
+    fun sarg _ diag ~depth coq_ctx _csts state ->
+      syntactic_arg_to_arg "syntactic.argument->unelaborated.argument" ~kind:Unelaborated sarg diag ~depth coq_ctx _csts state
+    ),
+   DocAbove);
+   MLCode(Pred("syntactic.push-scope",
+    In(Syntactic.trm_type, "SyntaxTerm",
+    In(Syntactic.delimiter_depth, "DelimiterDepth",
+    In(B.string, "ScopeName",
+    Out(Syntactic.trm_type, "ScopedSyntaxTerm",
+    Full(global, "Pushes the scope ScopeName on top of SyntaxTerm."))))),
+    fun t delim_depth scope _ ~depth coq_context _csts state ->
+      let open Syntactic in
+      let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
+      let Tag.{vl; _} = t in
+      let vl = CAst.make ~loc:(Option.default loc vl.CAst.loc) (Constrexpr.CDelimiters (delim_depth, scope, vl)) in
+      let ot = Tag.{t with vl} in
+      state, (!: ot), []
+    ),
+   DocAbove);
+   MLCode(Pred("syntactic.elaborate",
+    In(Syntactic.trm_type, "SyntacticTerm",
+    CIn(B.unspecC term, "TypeConstraint",
+    COut(term, "Term",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(proof_context, {|
+Elaborates SyntaxTerm using TypeConstraint (if provided).
+Supported attributes:
+- @no-tc! (default false, do not infer typeclasses)
+- @no-coercion! (default: false, do not insert coercions)
+|}))))),
+    fun t expected_type _ diag ~depth coq_ctx csts state ->
+      let expected_type =
+        match expected_type with
+        | B.Unspec -> Pretyping.WithoutTypeConstraint
+        | B.Given x -> Pretyping.OfType x in
+      syntactic_arg_elaborate "syntactic.elaborate" t expected_type diag ~depth coq_ctx csts state
+    ),
+   DocAbove);
+      MLCode(Pred("syntactic.elaborate-ty",
+    In(Syntactic.trm_type, "SyntacticTerm",
+    COut(term, "Term",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(proof_context, {|
+Elaborates SyntaxTerm as a Type.
+Supported attributes:
+- @no-tc! (default false, do not infer typeclasses)
+- @no-coercion! (default: false, do not insert coercions)
+|})))),
+    fun t _ diag ~depth coq_ctx csts state ->
+      let expected_type = Pretyping.IsType in
+      syntactic_arg_elaborate "syntactic.elaborate-ty" t expected_type diag ~depth coq_ctx csts state
+    ),
+   DocAbove);
+
+  ]
+
 
 ;;
diff --git a/src/rocq_elpi_builtins_synterp.ml b/src/rocq_elpi_builtins_synterp.ml
index 0f8366bc6..68f1e29a6 100644
--- a/src/rocq_elpi_builtins_synterp.ml
+++ b/src/rocq_elpi_builtins_synterp.ml
@@ -19,6 +19,7 @@ open Names
 
 open Rocq_elpi_utils
 open Rocq_elpi_HOAS
+open Rocq_elpi_arg_HOAS
 
 let prop = { B.any with Conv.ty = Conv.TyName "prop" }
 
@@ -1229,7 +1230,7 @@ Supported attributes:
   ] @ SynterpAction.get_parsing_actions_synterp @ [
   MLData attribute_value;
   MLData attribute;
-  ]
+  ] @ Syntactic.ml_data
 
 let synterp_api_doc = ". bla bla"
 
diff --git a/src/rocq_elpi_programs.ml b/src/rocq_elpi_programs.ml
index 0e10f9f6f..e761f8ea8 100644
--- a/src/rocq_elpi_programs.ml
+++ b/src/rocq_elpi_programs.ml
@@ -163,7 +163,7 @@ type db = {
   units : Names.KNset.t;
 }
 
-type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool }
+type nature = Command of { args : arg_kind } | Tactic | Program of { args : arg_kind }
 
 type program = {
   sources_rev : qualified_name Code.t;
@@ -242,7 +242,7 @@ module type Programs = sig
   val db_inspect : qualified_name -> int
 
   val get_and_compile_existing_db : loc:Loc.t -> qualified_name -> EC.program
-  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (EC.program * bool) option
+  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (EC.program * arg_kind) option
 
 end
 
@@ -804,7 +804,7 @@ let compile ~loc src =
   in
     compile_code src
 
-let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option =
+let get_and_compile ~loc ?even_if_empty name : (EC.program * arg_kind) option =
   let t = Unix.gettimeofday () in
   let res = code ?even_if_empty name |> Option.map (fun src ->
     (* Format.eprintf "compile %a = %a" pp_qualified_name name (Code.pp Chunk.pp) src; *)
@@ -815,9 +815,9 @@ let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option =
     let prog = recache_code 0 old_hash new_hash prog src in
     let raw_args =
       match get_nature name with
-      | Command { raw_args } -> raw_args
-      | Program { raw_args } -> raw_args
-      | Tactic -> true in
+      | Command { args } -> args
+      | Program { args } -> args
+      | Tactic -> Elaborated in
       (prog, raw_args)) in
     Rocq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t))));
     res
diff --git a/src/rocq_elpi_programs.mli b/src/rocq_elpi_programs.mli
index 3b6382e71..49cf0511c 100644
--- a/src/rocq_elpi_programs.mli
+++ b/src/rocq_elpi_programs.mli
@@ -24,7 +24,7 @@ and src_db_header = {
   dast : cunit;
 }
 
-type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool }
+type nature = Command of { args : arg_kind } | Tactic | Program of { args : arg_kind }
 
 
 module Chunk : sig
@@ -120,7 +120,7 @@ module type Programs = sig
   val db_inspect : qualified_name -> int
 
   val get_and_compile_existing_db : loc:Loc.t -> qualified_name -> Compile.program
-  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (Compile.program * bool) option
+  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (Compile.program * arg_kind) option
 
 
 end
diff --git a/src/rocq_elpi_utils.ml b/src/rocq_elpi_utils.ml
index b9938916d..bcd103323 100644
--- a/src/rocq_elpi_utils.ml
+++ b/src/rocq_elpi_utils.ml
@@ -873,3 +873,26 @@ let eta_contract env sigma t =
   in
     (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*)
     map env t
+
+(* Command argument specifiers *)
+type arg_kind =
+  | Elaborated
+  | Unelaborated
+  | Syntactic
+let arg_kind_merge ?loc (old : arg_kind option) (k : arg_kind) =
+  match old with
+  | None -> k
+  | Some old when old = k -> k
+  | _ -> CErrors.user_err ?loc Pp.(str "Syntax error, incompatible values for attribute \"arguments\"")
+
+(* Helper for predicates that produce diagnostics *)
+let diag_error_lazy
+    ?(on_ok=fun () -> raise API.BuiltInPredicate.No_clause)
+    diag_arg
+    (on_other : unit -> 'a) : 'a =
+  let open API.BuiltInPredicate in
+  (* optimization: don't print the error if caller wants OK *)
+  match diag_arg with
+  | Data Elpi.Builtin.OK -> on_ok ()
+  | _ -> on_other ()
+
diff --git a/src/rocq_elpi_utils.mli b/src/rocq_elpi_utils.mli
index f0e0aeba1..103d5929a 100644
--- a/src/rocq_elpi_utils.mli
+++ b/src/rocq_elpi_utils.mli
@@ -89,3 +89,16 @@ val mp2path: Names.ModPath.t -> string list
 val gr2path: Names.GlobRef.t -> string list
 
 val eta_contract : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
+
+(* Command argument specifiers *)
+type arg_kind =
+  | Elaborated
+  | Unelaborated
+  | Syntactic
+val arg_kind_merge : ?loc:Loc.t -> arg_kind option -> arg_kind -> arg_kind
+
+(* Diagnostics *)
+val diag_error_lazy : ?on_ok:(unit -> 'a) -> (* defaults to [raise No_clause] *)
+  Elpi.Builtin.diagnostic Elpi.API.BuiltInPredicate.ioarg ->
+  (unit -> 'a) ->
+  'a
diff --git a/src/rocq_elpi_vernacular.ml b/src/rocq_elpi_vernacular.ml
index f2d9b756c..b620fa8a8 100644
--- a/src/rocq_elpi_vernacular.ml
+++ b/src/rocq_elpi_vernacular.ml
@@ -399,10 +399,10 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x)
   let print ~atts ~loc ~name ~args output =
     skip ~ph:atts (print ~loc ~name ~args) output
 
-  let create_command ~atts:(raw_args) ~loc n =
-    let raw_args = Option.default false raw_args in
+  let create_command ~atts:(args) ~loc n =
+    let args = Option.default Elaborated args in
     let _ = P.ensure_initialized () in
-    P.declare_program n (Command { raw_args });
+    P.declare_program n (Command { args });
     P.init_program n ~loc [P.command_init()];
     set_current_program (snd n)
 
@@ -412,10 +412,10 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x)
     if P.stage = Summary.Stage.Interp then P.init_program n ~loc [P.command_init();P.tactic_init ()];
     set_current_program (snd n)
 
-  let create_program ~atts:(raw_args) ~loc n ~init:(sloc,s) =
-    let raw_args = Option.default false raw_args in
+  let create_program ~atts:(args) ~loc n ~init:(sloc,s) =
+    let args = Option.default Elaborated args in
     let elpi = P.ensure_initialized () in
-    P.declare_program n (Program { raw_args });
+    P.declare_program n (Program { args });
     if P.stage = Summary.Stage.Interp then begin
       let unit = P.unit_from_string ~elpi ~base:(EC.empty_base ~elpi) ~loc sloc s in
       let init = EmbeddedString { sast = unit} in
@@ -454,7 +454,7 @@ end
 
 module type Common = sig
   val get_and_compile :
-    loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * bool) option
+    loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * arg_kind) option
   val run : loc:Loc.t ->
     Elpi.API.Compile.program ->
      query ->
@@ -475,8 +475,8 @@ module type Common = sig
   val bound_steps   : atts:phase option -> int -> unit
   val print         : atts:phase option -> loc:Loc.t -> name:qualified_name -> args:string list -> string -> unit
 
-  val create_program : atts:bool option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
-  val create_command : atts:bool option -> loc:Loc.t -> program_name -> unit
+  val create_program : atts:arg_kind option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
+  val create_command : atts:arg_kind option -> loc:Loc.t -> program_name -> unit
   val create_tactic : loc:Loc.t -> program_name -> unit
   val create_db : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
   val create_file : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
@@ -538,7 +538,7 @@ module Interp = struct
     strbrk "The command lacks code for the synterp phase. In order to add code to this phase use '#[synterp] Elpi Accumulate'. See also https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html#parsing-and-execution"
   
   let run_program ~loc name ~main ~atts ~syndata args more_args =
-    get_and_compile ~loc name |> Option.map (fun (program, raw_args) ->
+    get_and_compile ~loc name |> Option.map (fun (program, kind) ->
       let env = Global.env () in
       let sigma = Evd.from_env env in
       let args = args
@@ -555,7 +555,7 @@ module Interp = struct
       let query state =
         let depth = 0 in
         let state, args, gls = EU.map_acc
-          (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~raw:raw_args Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))
+          (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~kind:kind Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))
           state args in
         let loc = Rocq_elpi_utils.of_coq_loc loc in
 
diff --git a/src/rocq_elpi_vernacular.mli b/src/rocq_elpi_vernacular.mli
index 60ec6bdfc..b77532f39 100644
--- a/src/rocq_elpi_vernacular.mli
+++ b/src/rocq_elpi_vernacular.mli
@@ -20,7 +20,7 @@ type what = Code | Signature
 module type Common = sig
 
   val get_and_compile :
-    loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * bool) option
+    loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * arg_kind) option
   val run : loc:Loc.t ->
     Elpi.API.Compile.program -> query ->
     Elpi.API.Execute.outcome
@@ -42,8 +42,8 @@ module type Common = sig
   val bound_steps   : atts:phase option -> int -> unit
   val print         : atts:phase option -> loc:Loc.t -> name:qualified_name -> args:string list -> string -> unit
 
-  val create_program : atts:bool option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
-  val create_command : atts:bool option -> loc:Loc.t -> program_name -> unit
+  val create_program : atts:arg_kind option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
+  val create_command : atts:arg_kind option -> loc:Loc.t -> program_name -> unit
   val create_tactic : loc:Loc.t -> program_name -> unit
   val create_db : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
   val create_file : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v
index d4e2fefb8..cbe06c16d 100644
--- a/tests/test_API_elaborate.v
+++ b/tests/test_API_elaborate.v
@@ -21,38 +21,38 @@ Coercion g1 : T1 >-> Funclass.
 Coercion g3 : T3 >-> Funclass.
 Coercion h : T2 >-> T3.
 
-Elpi Query lp:{{
+Elpi Query lp:{{/*(*/
 
   std.assert-ok! (coq.elaborate-skeleton {{ fun n (t : T2 n) (x : t) => t 3 }} TY E) "that was easy",
   coq.env.add-const "elab_1" E TY tt _
 
-}}.
+/*)*/}}.
 
 Class foo (n : nat).
 Definition bar n {f : foo n} := n = n.
 #[local] Instance xxx : foo 3. Defined.
 
-Elpi Query lp:{{
+Elpi Query lp:{{/*(*/
 
   std.assert-ok! (coq.elaborate-ty-skeleton {{ bar _ }} TY E) "that was easy",
   coq.env.add-const "elab_2" E (sort TY) tt _
 
-}}.
+/*)*/}}.
 
 Structure s := { field : Type; #[canonical=no] op : field -> field; }.
 Canonical c := {| field := nat; op := (fun x => x) |}.
 
-Elpi Query lp:{{
+Elpi Query lp:{{/*(*/
 
   std.assert-ok! (coq.elaborate-skeleton {{ op _ 3 }} TY E) "that was easy",
   coq.env.add-const "elab_3" E TY tt _
 
-}}.
+/*)*/}}.
 
 (* #[arguments(raw)] *)
 Elpi Command test.API2.
 
-Elpi Accumulate lp:{{
+Elpi Accumulate lp:{{/*(*/
   main [indt-decl D] :- coq.say "raw:" D,
     std.assert-ok! (coq.elaborate-indt-decl-skeleton D D1) "illtyped",
     coq.say "elab1:" D1,
@@ -65,7 +65,7 @@ Elpi Accumulate lp:{{
     std.assert-ok! (coq.elaborate-skeleton BO TY1 BO1) "illtyped",
     coq.env.add-const N BO1 TY1 @transparent! _,
   ].
-}}.
+/*)*/}}.
 
 
 Elpi test.API2 Inductive ind1 (A : T1) | (B : Type) :=
@@ -145,43 +145,205 @@ Check (forall x : ind3, x -> Prop).
 
 Elpi test.API2 Definition def1 A := fun x : A => x.
 
-Elpi Query lp:{{
+Elpi Query lp:{{/*(*/
 
   std.assert-ok! (coq.elaborate-skeleton {{ op lib:elpi.hole 3 }} TY E) "that was easy 2",
   coq.env.add-const "elab_4" E TY tt _
 
-}}.
+/*)*/}}.
 
 Elpi Tactic test.
-Elpi Accumulate lp:{{
+Elpi Accumulate lp:{{/*(*/
 solve _ _ :-
   coq.term->string X S,
   X = global (indc Y),
   coq.say S.
-}}.
+/*)*/}}.
 Goal True.
 Fail elpi test.
 Abort.
 
 Elpi Tactic test2.
-Elpi Accumulate lp:{{
+Elpi Accumulate lp:{{/*(*/
 solve _ _ :-
   coq.term->string (global (indc Y)) S,
   coq.say S.
-}}.
+/*)*/}}.
 Goal True.
 elpi test2.
 Abort.
 
 #[arguments(raw)] Elpi Command detype.
-Elpi Accumulate lp:{{
+Elpi Accumulate lp:{{/*(*/
   main [upoly-const-decl _ _ (parameter _ _ (sort (typ U)) _ as A) (upoly-decl [UL] _ _ _)] :-
     std.assert! (coq.univ.variable U UL) "wtf",
     (@keepunivs! => std.assert-ok! (coq.elaborate-arity-skeleton A _ (parameter _ _ (sort (typ V)) _)) "wtf"),
     std.assert! (U = V) "elaboration refreshes",
     coq.say U V.
-}}.
+/*)*/}}.
 
 
 Elpi detype #[universes(polymorphic)] Definition f@{u|Set < u} (x : Type@{u}) := x.
 
+(** Parser tests *)
+Succeed #[arguments(raw)] Elpi Command argtest.
+Succeed #[arguments(unelaborated)] Elpi Command argtest.
+Succeed #[arguments(elaborated)] Elpi Command argtest.
+Succeed #[arguments(syntactic)] Elpi Command argtest.
+(* The test below should fail but does not for some reason.
+   Also, the error message is terribly. See https://github.com/rocq-prover/rocq/issues/17041 *)
+#[local] Set Warnings "+unsupported-attributes".
+Succeed #[arguments(something_else)] Elpi Command argtest.
+
+(* Arguments do not allow any specified values, not even booleans *)
+Fail #[arguments(raw="test")] Elpi Command detype.
+Fail #[arguments(raw=false)] Elpi Command detype.
+
+(* Syntactic tests *)
+#[arguments(syntactic)] Elpi Command syntax_test1.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.int 1)].
+/*)*/}}.
+Elpi syntax_test1 1.
+Fail Elpi syntax_test1 2.
+
+#[arguments(syntactic)] Elpi Command syntax_test2.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.str "test")].
+/*)*/}}.
+Elpi syntax_test2 "test".
+Fail Elpi syntax_test2 "foo".
+
+#[arguments(syntactic)] Elpi Command syntax_test3.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic Arg] :-
+  syntactic.argument->elaborated.argument Arg (int 1) ok.
+/*)*/}}.
+Elpi syntax_test3 1.
+Fail Elpi syntax_test3 2.
+
+#[arguments(syntactic)] Elpi Command syntax_test4.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic Arg] :-
+  syntactic.argument->elaborated.argument Arg (trm {{(1 + 1)}}) ok.
+/*)*/}}.
+Elpi syntax_test4 (1 + 1).
+Fail Elpi syntax_test4 (2 + 1).
+
+
+(* Test evar dependencies *)
+#[arguments(elaborated)] Elpi Command evar_deps.
+Elpi Accumulate lp:{{/*(*/
+  main [trm T1, trm T2] :-
+   pattern_match T1 {{ 1 + 1 }},
+   pattern_match T2 {{ 1 }}.
+/*)*/}}.
+(* Evars are elaborated/interpreted  before they are unified during the execution of [main]. *)
+Elpi evar_deps (?[x] + ?x) (?x).
+(* Rocq is perhaps a bit too eager to throw away instantiated evars: https://github.com/rocq-prover/rocq/issues/21116 *)
+Fail Elpi evar_deps (eq_refl : (?[x] = 1)) (?x).
+
+#[arguments(syntactic)] Elpi Command syntax_test_evars.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic Arg1, syntactic Arg2] :-
+  syntactic.argument->elaborated.argument Arg1 (trm {{ 1 + 1 }}) ok,
+  syntactic.argument->elaborated.argument Arg2 (trm {{(1)}}) ok.
+/*)*/}}.
+Elpi syntax_test_evars (1 + 1) (1).
+Elpi syntax_test_evars (?[x] + 1) (1).
+Elpi syntax_test_evars (1 + 1) (?[x]).
+(* Our program interpretes and then unifies the evars in the first argument
+before it interpretes the second argument. The named evar disappears after the
+first step and thus the second argument cannot be interpreted any more. *)
+Fail Elpi syntax_test_evars (?[x] + ?x) (?x).
+
+(* We can fix this by taking these steps more slowly. *)
+#[arguments(syntactic)] Elpi Command syntax_test_evars_staged.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic Arg1, syntactic Arg2] :-
+  syntactic.argument->elaborated.argument Arg1 (trm T1) ok,
+  syntactic.argument->elaborated.argument Arg2 (trm T2) ok,
+  T1 = {{ 1 + 1 }},
+  T2 = {{ 1 }}.
+/*)*/}}.
+Elpi syntax_test_evars_staged (1 + 1) (1).
+Elpi syntax_test_evars_staged (?[x] + 1) (1).
+Elpi syntax_test_evars_staged (1 + 1) (?[x]).
+(* Now we interprete both terms first and only then start unifying them. *)
+Elpi syntax_test_evars_staged (?[x] + ?x) (?x).
+
+
+(* Adding scopes to syntactic terms. *)
+Declare Scope test_scope.
+Delimit Scope test_scope with test.
+Notation "'[test_notation' ]" := (tt) : test_scope.
+
+#[arguments(syntactic)] Elpi Command syntax_test6.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.str Scope), syntactic (syntactic.trm Arg1)] :-
+  syntactic.push-scope Arg1 syntactic.delimit-only-tmp-scope Scope ScopedArg,
+  syntactic.argument->elaborated.argument (syntactic.trm ScopedArg) (trm {{ tt }}) ok.
+/*)*/}}.
+Fail Check [test_notation].
+Fail Elpi syntax_test6 "core" ([test_notation ]).
+Succeed Check [test_notation]%test.
+Elpi syntax_test6 "test" ([test_notation ]).
+
+(* Manual Elaboration *)
+
+#[arguments(syntactic)] Elpi Command elaborate_test.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.trm T)] :-
+  syntactic.elaborate T _ T' ok,
+  T' = {{ _ + _ }}.
+/*)*/}}.
+Elpi elaborate_test (1 + 1).
+Elpi elaborate_test (1 + ?[x]).
+Elpi elaborate_test (?[x] + ?x).
+
+Definition f : unit -> nat := fun _ => 0.
+Coercion f : unit >-> nat.
+
+Class Cls := { proj : nat }.
+Instance : Cls := {| proj := 1 |}.
+
+Elpi elaborate_test (1 + tt).     (* coercions *)
+Elpi elaborate_test (tt + 1).
+Elpi elaborate_test (tt + proj).  (* and typeclasses *)
+Elpi elaborate_test (proj + tt).
+
+#[arguments(syntactic)] Elpi Command elaborate_test_ty.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.trm Ty), syntactic (syntactic.trm T)] :-
+  syntactic.elaborate-ty Ty Ty' ok,
+  syntactic.elaborate T Ty' T' ok,
+  ground_term T'.
+/*)*/}}.
+Elpi elaborate_test_ty (nat) (1 + 1).
+Fail Elpi elaborate_test_ty (False) (I).
+Elpi elaborate_test_ty (nat) (tt). (* uses coercion *)
+Elpi elaborate_test_ty (nat) (proj). (* typeclasses *)
+Elpi elaborate_test_ty (Cls -> nat) (@proj).
+
+#[arguments(syntactic)] Elpi Command elaborate_test_ty2.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.trm Ty), syntactic (syntactic.trm T)] :-
+  syntactic.elaborate-ty Ty Ty' ok,
+  (@no-tc! => @no-coercion! => syntactic.elaborate T Ty' T' ok),
+  ground_term T'.
+/*)*/}}.
+Elpi elaborate_test_ty2 (nat) (1 + 1).
+Fail Elpi elaborate_test_ty (False) (I).
+Fail Elpi elaborate_test_ty2 (nat) (tt). (* requires coercions *)
+Fail Elpi elaborate_test_ty2 (nat) (proj). (* requires TC *)
+Elpi elaborate_test_ty2 (Cls -> nat) (@proj).
+
+(* Error messages *)
+#[arguments(syntactic)] Elpi Command error_msgs.
+Elpi Accumulate lp:{{/*(*/
+  main [syntactic (syntactic.str RegExp), syntactic (syntactic.trm T)] :-
+  syntactic.elaborate T _ _ (error E),
+  std.assert! (rex.match RegExp E) "bad message".
+/*)*/}}.
+Elpi error_msgs ".*has type.*True.*" (I + 1).
+Elpi error_msgs ".*Non exhaust.*" (match true with | true => I end).