More notations for primitive tactics.

8 files changed, 40 insertions, 7 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 5d5bc6b941..be7f830605 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -368,7 +368,7 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 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_reference q_with_bindings q_constr_matching;
+          q_destruction_arg q_reference q_with_bindings q_constr_matching;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -500,11 +500,14 @@ GEXTEND Gram
     [ [ c = Constr.constr; l = with_bindings -> Loc.tag ~loc:!@loc @@ (c, l) ] ]
   ;
   destruction_arg:
-    [ [ n = lnatural -> QElimOnAnonHyp n
-      | id = lident -> QElimOnIdent id
-      | c = constr_with_bindings -> QElimOnConstr c
+    [ [ n = lnatural -> Loc.tag ~loc:!@loc @@ QElimOnAnonHyp n
+      | id = lident -> Loc.tag ~loc:!@loc @@ QElimOnIdent id
+      | c = constr_with_bindings -> Loc.tag ~loc:!@loc @@ QElimOnConstr c
     ] ]
   ;
+  q_destruction_arg:
+    [ [ arg = destruction_arg -> arg ] ]
+  ;
   as_or_and_ipat:
     [ [ "as"; ipat = or_and_intropattern -> Some ipat
       | -> None
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 17fccf3ac7..867c9ae806 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1133,6 +1133,7 @@ let () = add_expr_scope "bindings" q_bindings Tac2quote.of_bindings
 let () = add_expr_scope "with_bindings" q_with_bindings Tac2quote.of_bindings
 let () = add_expr_scope "intropattern" q_intropattern Tac2quote.of_intro_pattern
 let () = add_expr_scope "intropatterns" q_intropatterns Tac2quote.of_intro_patterns
+let () = add_expr_scope "destruction_arg" q_destruction_arg Tac2quote.of_destruction_arg
 let () = add_expr_scope "induction_clause" q_induction_clause Tac2quote.of_induction_clause
 let () = add_expr_scope "rewriting" q_rewriting Tac2quote.of_rewriting
 let () = add_expr_scope "clause" q_clause Tac2quote.of_clause
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 7a900e8bf0..afbbcfc15e 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -29,6 +29,7 @@ let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
 let q_with_bindings = Pcoq.Gram.entry_create "tactic:q_with_bindings"
 let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
 let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
+let q_destruction_arg = Pcoq.Gram.entry_create "tactic:q_destruction_arg"
 let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
 let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
 let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index dde877666a..581d04d8cc 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -64,6 +64,7 @@ val q_bindings : bindings Pcoq.Gram.entry
 val q_with_bindings : bindings Pcoq.Gram.entry
 val q_intropattern : intro_pattern Pcoq.Gram.entry
 val q_intropatterns : intro_pattern list located Pcoq.Gram.entry
+val q_destruction_arg : destruction_arg Pcoq.Gram.entry
 val q_induction_clause : induction_clause Pcoq.Gram.entry
 val q_rewriting : rewriting Pcoq.Gram.entry
 val q_clause : clause Pcoq.Gram.entry
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index a284c1e756..577fe8edfe 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -68,11 +68,13 @@ type clause = clause_r located
 
 type constr_with_bindings = (Constrexpr.constr_expr * bindings) located
 
-type destruction_arg =
+type destruction_arg_r =
 | QElimOnConstr of constr_with_bindings
 | QElimOnIdent of Id.t located
 | QElimOnAnonHyp of int located
 
+type destruction_arg = destruction_arg_r located
+
 type induction_clause_r = {
   indcl_arg : destruction_arg;
   indcl_eqn : intro_pattern_naming option;
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index d38d7414fe..ed4cef2e2a 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -191,7 +191,7 @@ let of_clause (loc, cl) =
     std_proj "on_concl", concl;
   ])
 
-let of_destruction_arg ?loc = function
+let of_destruction_arg (loc, arg) = match arg with
 | QElimOnConstr c ->
   let arg = thunk (of_constr_with_bindings c) in
   std_constructor ?loc "ElimOnConstr" [arg]
@@ -199,7 +199,7 @@ let of_destruction_arg ?loc = function
 | QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int n]
 
 let of_induction_clause (loc, cl) =
-  let arg = of_destruction_arg ?loc cl.indcl_arg in
+  let arg = of_destruction_arg cl.indcl_arg in
   let eqn = of_option ?loc of_intro_pattern_naming cl.indcl_eqn in
   let as_ = of_option ?loc of_or_and_intro_pattern cl.indcl_as in
   let in_ = of_option ?loc of_clause cl.indcl_in in
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index c3374ac24e..875230b7e3 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -46,6 +46,8 @@ val of_intro_patterns : intro_pattern list located -> raw_tacexpr
 
 val of_clause : clause -> raw_tacexpr
 
+val of_destruction_arg : destruction_arg -> raw_tacexpr
+
 val of_induction_clause : induction_clause -> raw_tacexpr
 
 val of_rewriting : rewriting -> raw_tacexpr
diff --git a/theories/Notations.v b/theories/Notations.v
index 5ed47336ad..ad89bc5cfc 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -383,6 +383,12 @@ Ltac2 Notation "eexact" c(thunk(open_constr)) := exact0 true c.
 
 Ltac2 Notation reflexivity := Std.reflexivity ().
 
+Ltac2 symmetry0 cl :=
+  Std.symmetry (default_on_concl cl).
+
+Ltac2 Notation "symmetry" cl(opt(clause)) := symmetry0 cl.
+Ltac2 Notation symmetry := symmetry.
+
 Ltac2 Notation assumption := Std.assumption ().
 
 Ltac2 Notation etransitivity := Std.etransitivity ().
@@ -412,3 +418,20 @@ end.
 
 Ltac2 Notation "subst" ids(list0(ident)) := subst0 ids.
 Ltac2 Notation subst := subst.
+
+Ltac2 Notation "discriminate" arg(opt(destruction_arg)) :=
+  Std.discriminate false arg.
+
+Ltac2 Notation "ediscriminate" arg(opt(destruction_arg)) :=
+  Std.discriminate true arg.
+
+Ltac2 Notation "injection" arg(opt(destruction_arg)) ipat(opt(seq("as", intropatterns))):=
+  Std.injection false ipat arg.
+
+Ltac2 Notation "einjection" arg(opt(destruction_arg)) ipat(opt(seq("as", intropatterns))):=
+  Std.injection true ipat arg.
+
+(** Congruence *)
+
+Ltac2 f_equal0 () := ltac1:(f_equal).
+Ltac2 Notation f_equal := f_equal0 ().