diff options
| author | Pierre-Marie Pédrot | 2017-08-04 18:02:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-05 01:08:23 +0200 |
| commit | 1f2de88e09c7bb1c0aa111db0d7d50b83f8a62d4 (patch) | |
| tree | 11d9fab847de5cef36f1d3b0e8ee9ee2f1d3da62 /src/g_ltac2.ml4 | |
| parent | de88ba86e9d2a77883365503759eaec96928e9c4 (diff) | |
Exporting the rewrite tactic.
Diffstat (limited to 'src/g_ltac2.ml4')
| -rw-r--r-- | src/g_ltac2.ml4 | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 48a593df28..8b373647f3 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -309,7 +309,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_rewriting q_clause; anti: [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ] ; @@ -479,12 +479,14 @@ GEXTEND Gram { q_onhyps = Some hl; q_concl_occs = QNoOccurrences } ] ] ; - opt_clause: - [ [ "in"; cl = in_clause -> Some cl - | "at"; occs = occs_nums -> Some { q_onhyps = Some []; q_concl_occs = occs } - | -> None + clause: + [ [ "in"; cl = in_clause -> cl + | "at"; occs = occs_nums -> { q_onhyps = Some []; q_concl_occs = occs } ] ] ; + q_clause: + [ [ cl = clause -> Tac2quote.of_clause cl ] ] + ; concl_occ: [ [ "*"; occs = occs -> occs | -> QNoOccurrences @@ -492,7 +494,7 @@ GEXTEND Gram ; induction_clause: [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; - cl = opt_clause -> + cl = OPT clause -> Loc.tag ~loc:!@loc @@ { indcl_arg = c; indcl_eqn = eq; |