Introducing quotations for move locations.

7 files changed, 30 insertions, 1 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 67254d0781..5c285010e9 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -369,7 +369,7 @@ GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
           q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
           q_destruction_arg q_reference q_with_bindings q_constr_matching
-          q_hintdb;
+          q_hintdb q_move_location;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -692,6 +692,16 @@ GEXTEND Gram
   q_constr_matching:
     [ [ m = match_list -> m ] ]
   ;
+  move_location:
+    [ [ "at"; IDENT "top" -> Loc.tag ~loc:!@loc @@ QMoveFirst
+      | "at"; IDENT "bottom" -> Loc.tag ~loc:!@loc @@ QMoveLast
+      | IDENT "after"; id = ident_or_anti -> Loc.tag ~loc:!@loc @@ QMoveAfter id
+      | IDENT "before"; id = ident_or_anti -> Loc.tag ~loc:!@loc @@ QMoveBefore id
+    ] ]
+  ;
+  q_move_location:
+    [ [ mv = move_location -> mv ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index a735dd19d9..37f1c99b15 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1142,6 +1142,7 @@ let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences
 let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
 let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
 let () = add_expr_scope "reference" q_reference Tac2quote.of_reference
+let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_location
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 121841e8dc..9fd03ff5aa 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -39,6 +39,7 @@ let q_reference = Pcoq.Gram.entry_create "tactic:q_reference"
 let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
 let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
 let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
+let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 91e2a683d8..dda1653593 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -74,6 +74,7 @@ val q_reference : Libnames.reference or_anti Pcoq.Gram.entry
 val q_strategy_flag : strategy_flag Pcoq.Gram.entry
 val q_constr_matching : constr_matching Pcoq.Gram.entry
 val q_hintdb : hintdb Pcoq.Gram.entry
+val q_move_location : move_location Pcoq.Gram.entry
 end
 
 (** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 4bbaf43d8d..7d02022e07 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -131,3 +131,11 @@ type hintdb_r =
 | QHintDbs of Id.t located or_anti list
 
 type hintdb = hintdb_r located
+
+type move_location_r =
+| QMoveAfter of Id.t located or_anti
+| QMoveBefore of Id.t located or_anti
+| QMoveFirst
+| QMoveLast
+
+type move_location = move_location_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index f87985435c..f14612d58f 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -364,3 +364,9 @@ let of_constr_matching (loc, m) =
     constructor ?loc (pattern_core "ConstrMatchContext") [pat; e]
   in
   of_list ?loc map m
+
+let of_move_location (loc, mv) = match mv with
+| QMoveAfter id -> std_constructor ?loc "MoveAfter" [of_anti of_ident id]
+| QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
+| QMoveFirst -> std_constructor ?loc "MoveFirst" []
+| QMoveLast -> std_constructor ?loc "MoveLast" []
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index b85f3438a3..db2fda3831 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -56,6 +56,8 @@ val of_occurrences : occurrences -> raw_tacexpr
 
 val of_hintdb : hintdb -> raw_tacexpr
 
+val of_move_location : move_location -> raw_tacexpr
+
 val of_reference : Libnames.reference or_anti -> raw_tacexpr
 
 val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr