Rely on quoting for lists instead of hardwiring it in the AST.

4 files changed, 6 insertions, 33 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 4a7ba31373..7406a45207 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -125,7 +125,8 @@ GEXTEND Gram
       | "("; a = SELF; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
       | "()" -> CTacCst (!@loc, AbsKn (Tuple 0))
       | "("; ")" -> CTacCst (!@loc, AbsKn (Tuple 0))
-      | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" -> CTacLst (Loc.tag ~loc:!@loc a)
+      | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
+        Tac2quote.of_list ~loc:!@loc (fun x -> x) a
       | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a)
       | a = tactic_atom -> a ]
     ]
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 6c38d1dfd5..8d0f640209 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -827,19 +827,13 @@ let () = add_scope "list0" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
   let scope = Extend.Alist0 scope in
-  let act l =
-    let l = List.map act l in
-    CTacLst (None, l)
-  in
+  let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr (_, str)] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
   let sep = Extend.Atoken (CLexer.terminal str) in
   let scope = Extend.Alist0sep (scope, sep) in
-  let act l =
-    let l = List.map act l in
-    CTacLst (None, l)
-  in
+  let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -848,19 +842,13 @@ let () = add_scope "list1" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
   let scope = Extend.Alist1 scope in
-  let act l =
-    let l = List.map act l in
-    CTacLst (None, l)
-  in
+  let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr (_, str)] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
   let sep = Extend.Atoken (CLexer.terminal str) in
   let scope = Extend.Alist1sep (scope, sep) in
-  let act l =
-    let l = List.map act l in
-    CTacLst (None, l)
-  in
+  let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 7efb85cbb0..76fb50181f 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -99,7 +99,6 @@ type raw_tacexpr =
 | CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
 | CTacLet of Loc.t * rec_flag * (raw_patexpr * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
 | CTacArr of raw_tacexpr list located
-| CTacLst of raw_tacexpr list located
 | CTacCnv of Loc.t * raw_tacexpr * raw_typexpr
 | CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr
 | CTacCse of Loc.t * raw_tacexpr * raw_taccase list
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index b62a574a6c..865935c52d 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -195,7 +195,6 @@ let loc_of_tacexpr = function
 | CTacApp (loc, _, _) -> loc
 | CTacLet (loc, _, _, _) -> loc
 | CTacArr (loc, _) -> Option.default dummy_loc loc
-| CTacLst (loc, _) -> Option.default dummy_loc loc
 | CTacCnv (loc, _, _) -> loc
 | CTacSeq (loc, _, _) -> loc
 | CTacCse (loc, _, _) -> loc
@@ -735,14 +734,6 @@ let rec intern_rec env = function
   let fold e el = intern_rec_with_constraint env e t0 :: el in
   let el = e0 :: List.fold_right fold el [] in
   (GTacArr el, GTypRef (Other t_array, [t0]))
-| CTacLst (loc, []) ->
-  let id = fresh_id env in
-  (c_nil, GTypRef (Other t_list, [GTypVar id]))
-| CTacLst (loc, e0 :: el) ->
-  let (e0, t0) = intern_rec env e0 in
-  let fold e el = c_cons (intern_rec_with_constraint env e t0) el in
-  let el = c_cons e0 (List.fold_right fold el c_nil) in
-  (el, GTypRef (Other t_list, [t0]))
 | CTacCnv (loc, e, tc) ->
   let (e, t) = intern_rec env e in
   let tc = intern_type env tc in
@@ -1229,9 +1220,6 @@ let rec globalize ids e = match e with
 | CTacArr (loc, el) ->
   let el = List.map (fun e -> globalize ids e) el in
   CTacArr (loc, el)
-| CTacLst (loc, el) ->
-  let el = List.map (fun e -> globalize ids e) el in
-  CTacLst (loc, el)
 | CTacCnv (loc, e, t) ->
   let e = globalize ids e in
   CTacCnv (loc, e, t)
@@ -1446,9 +1434,6 @@ let rec subst_rawexpr subst t = match t with
 | CTacArr (loc, el) ->
   let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
   if el' == el then t else CTacArr (loc, el')
-| CTacLst (loc, el) ->
-  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
-  if el' == el then t else CTacLst (loc, el')
 | CTacCnv (loc, e, c) ->
   let e' = subst_rawexpr subst e in
   let c' = subst_rawtype subst c in