Do not return STRING scopes in the tuple produced by "seq" scopes.

5 files changed, 23 insertions, 38 deletions

diff --git a/doc/ltac2.md b/doc/ltac2.md
index 55780a7712..a645331e2d 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -615,8 +615,10 @@ The following scopes are built-in.
   + parses the string *s* as a keyword, if it is already a
     keyword, otherwise as an IDENT. Returns `()`.
 - seq(*scope₁*, ..., *scopeₙ*):
-  + parses *scope₁*, ..., *scopeₙ* in this order, and produces a n-tuple made
-    out of the parsed values in the same order. It is forbidden for the various
+  + parses *scope₁*, ..., *scopeₙ* in this order, and produces a tuple made
+    out of the parsed values in the same order. As an optimization, all
+    subscopes of the form STRING are left out of the returned tuple, instead
+    of returning a useless unit value. It is forbidden for the various
     subscopes to refer to the global entry using self of next.
 
 For now there is no way to declare new scopes from Ltac2 side, but this is
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 8d0f640209..7a8f3ceb44 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -963,13 +963,12 @@ let rec generalize_symbol :
 
 type _ converter =
 | CvNil : (Loc.t -> raw_tacexpr) converter
-| CvCns : 'act converter * ('a -> raw_tacexpr) -> ('a -> 'act) converter
+| CvCns : 'act converter * ('a -> raw_tacexpr) option -> ('a -> 'act) converter
 
 let rec apply : type a. a converter -> raw_tacexpr list -> a = function
-| CvNil -> fun accu loc ->
-  let cst = CTacCst (loc, AbsKn (Tuple (List.length accu))) in
-  CTacApp (loc, cst, accu)
-| CvCns (c, f) -> fun accu x -> apply c (f x :: accu)
+| CvNil -> fun accu loc -> Tac2quote.of_tuple ~loc accu
+| CvCns (c, None) -> fun accu x -> apply c accu
+| CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu)
 
 type seqrule =
 | Seqrule : ('act, Loc.t -> raw_tacexpr) norec_rule * 'act converter -> seqrule
@@ -983,6 +982,10 @@ let rec make_seq_rule = function
   let scope = generalize_symbol scope in
   let Seqrule (r, c) = make_seq_rule rem in
   let r = { norec_rule = Next (r.norec_rule, scope.any_symbol) } in
+  let f = match tok with
+  | SexprStr _ -> None (** Leave out mere strings *)
+  | _ -> Some f
+  in
   Seqrule (r, CvCns (c, f))
 
 let () = add_scope "seq" begin fun toks ->
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 9778bd18ae..dbd2fd0529 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -46,7 +46,12 @@ let of_pair f g (loc, (e1, e2)) =
   let loc = Option.default dummy_loc loc in
   CTacApp (loc, CTacCst (loc, AbsKn (Tuple 2)), [f e1; g e2])
 
-let of_tuple ?loc el =
+let of_tuple ?loc el = match el with
+| [] ->
+  let loc = Option.default dummy_loc loc in
+  CTacCst (loc, AbsKn (Tuple 0))
+| [e] -> e
+| el ->
   let loc = Option.default dummy_loc loc in
   let len = List.length el in
   CTacApp (loc, CTacCst (loc, AbsKn (Tuple len)), el)
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index bd2303ac98..7f3d9dce6e 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -24,6 +24,8 @@ val of_int : int located -> raw_tacexpr
 
 val of_pair : ('a -> raw_tacexpr) -> ('b -> raw_tacexpr) -> ('a * 'b) located -> raw_tacexpr
 
+val of_tuple : ?loc:Loc.t -> raw_tacexpr list -> raw_tacexpr
+
 val of_variable : Id.t located -> raw_tacexpr
 
 val of_ident : Id.t located -> raw_tacexpr
diff --git a/theories/Notations.v b/theories/Notations.v
index 2d52904faf..bb27a34627 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -175,14 +175,7 @@ Ltac2 Notation econstructor := econstructor.
 Ltac2 Notation "econstructor" n(tactic) bnd(thunk(bindings)) := constructor0 true n bnd.
 
 Ltac2 elim0 ev c bnd use :=
-  let f ev ((c, bnd, use)) :=
-    let use := match use with
-    | None => None
-    | Some u =>
-      let ((_, c, wth)) := u in Some (c, wth)
-    end in
-    Std.elim ev (c, bnd) use
-  in
+  let f ev ((c, bnd, use)) := Std.elim ev (c, bnd) use in
   enter_h ev f (fun () => c (), bnd (), use ()).
 
 Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
@@ -219,14 +212,7 @@ Ltac2 Notation "apply"
   apply0 true false cb cl.
 
 Ltac2 induction0 ev ic use :=
-  let f ev use :=
-    let use := match use with
-    | None => None
-    | Some u =>
-      let ((_, c, wth)) := u in Some (c, wth)
-    end in
-    Std.induction ev ic use
-  in
+  let f ev use := Std.induction ev ic use in
   enter_h ev f use.
 
 Ltac2 Notation "induction"
@@ -240,14 +226,7 @@ Ltac2 Notation "einduction"
   induction0 true ic use.
 
 Ltac2 destruct0 ev ic use :=
-  let f ev use :=
-    let use := match use with
-    | None => None
-    | Some u =>
-      let ((_, c, wth)) := u in Some (c, wth)
-    end in
-    Std.destruct ev ic use
-  in
+  let f ev use := Std.destruct ev ic use in
   enter_h ev f use.
 
 Ltac2 Notation "destruct"
@@ -312,12 +291,6 @@ Ltac2 Notation "native_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause
 Ltac2 Notation native_compute := native_compute.
 
 Ltac2 rewrite0 ev rw cl tac :=
-  let tac := match tac with
-  | None => None
-  | Some p =>
-    let ((_, tac)) := p in
-    Some tac
-  end in
   let cl := default_on_concl cl in
   Std.rewrite ev rw cl tac.