diff options
| -rw-r--r-- | src/g_ltac2.ml4 | 12 | ||||
| -rw-r--r-- | src/tac2core.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.mli | 1 | ||||
| -rw-r--r-- | src/tac2qexpr.mli | 8 | ||||
| -rw-r--r-- | src/tac2quote.ml | 6 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 | ||||
| -rw-r--r-- | theories/Std.v | 7 |
8 files changed, 37 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 diff --git a/theories/Std.v b/theories/Std.v index 02bc4ff450..3f98bdbaab 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -106,6 +106,13 @@ Ltac2 Type rewriting := { Ltac2 Type evar_flag := bool. Ltac2 Type advanced_flag := bool. +Ltac2 Type move_location := [ +| MoveAfter (ident) +| MoveBefore (ident) +| MoveFirst +| MoveLast +]. + Ltac2 Type inversion_kind := [ | SimpleInversion | FullInversion |