diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 15 | ||||
| -rw-r--r-- | src/tac2core.ml | 2 | ||||
| -rw-r--r-- | src/tac2entries.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.mli | 1 | ||||
| -rw-r--r-- | src/tac2qexpr.mli | 4 | ||||
| -rw-r--r-- | src/tac2quote.ml | 6 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 |
7 files changed, 21 insertions, 10 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index e9d2eb1ca3..e3d48f75ca 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -310,7 +310,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_rewriting q_clause q_dispatch q_occurrences; anti: [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ] ; @@ -449,13 +449,13 @@ GEXTEND Gram ] ] ; occs_nums: - [ [ nl = LIST1 nat_or_anti -> QOnlyOccurrences nl + [ [ nl = LIST1 nat_or_anti -> Loc.tag ~loc:!@loc @@ QOnlyOccurrences nl | "-"; n = nat_or_anti; nl = LIST0 nat_or_anti -> - QAllOccurrencesBut (n::nl) + Loc.tag ~loc:!@loc @@ QAllOccurrencesBut (n::nl) ] ] ; occs: - [ [ "at"; occs = occs_nums -> occs | -> QAllOccurrences ] ] + [ [ "at"; occs = occs_nums -> occs | -> Loc.tag ~loc:!@loc QAllOccurrences ] ] ; hypident: [ [ id = ident_or_anti -> @@ -477,7 +477,7 @@ GEXTEND Gram | hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ -> { q_onhyps = Some hl; q_concl_occs = occs } | hl = LIST0 hypident_occ SEP "," -> - { q_onhyps = Some hl; q_concl_occs = QNoOccurrences } + { q_onhyps = Some hl; q_concl_occs = Loc.tag ~loc:!@loc QNoOccurrences } ] ] ; clause: @@ -491,7 +491,7 @@ GEXTEND Gram ; concl_occ: [ [ "*"; occs = occs -> occs - | -> QNoOccurrences + | -> Loc.tag ~loc:!@loc QNoOccurrences ] ] ; induction_clause: @@ -558,6 +558,9 @@ GEXTEND Gram q_dispatch: [ [ d = tactic_then_gen -> Tac2quote.of_dispatch (Loc.tag ~loc:!@loc d) ] ] ; + q_occurrences: + [ [ occs = occs -> Tac2quote.of_occurrences occs ] ] + ; END (** Extension of constr syntax *) diff --git a/src/tac2core.ml b/src/tac2core.ml index b8e50ad1df..3ce2ed53a8 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -919,10 +919,12 @@ let () = add_expr_scope "intropatterns" Tac2entries.Pltac.q_intropatterns let () = add_expr_scope "induction_clause" Tac2entries.Pltac.q_induction_clause let () = add_expr_scope "rewriting" Tac2entries.Pltac.q_rewriting let () = add_expr_scope "clause" Tac2entries.Pltac.q_clause +let () = add_expr_scope "occurrences" Tac2entries.Pltac.q_occurrences let () = add_expr_scope "dispatch" Tac2entries.Pltac.q_dispatch let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr +let () = add_generic_scope "pattern" Pcoq.Constr.constr wit_pattern (** seq scope, a bit hairy *) diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 729779aef2..2490f6534b 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -32,6 +32,7 @@ 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" let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch" +let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences" end (** Tactic definition *) diff --git a/src/tac2entries.mli b/src/tac2entries.mli index 0dd1d5a113..cf6cdfa74b 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -65,4 +65,5 @@ val q_induction_clause : raw_tacexpr Pcoq.Gram.entry val q_rewriting : raw_tacexpr Pcoq.Gram.entry val q_clause : raw_tacexpr Pcoq.Gram.entry val q_dispatch : raw_tacexpr Pcoq.Gram.entry +val q_occurrences : raw_tacexpr Pcoq.Gram.entry end diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index e2bf10f4e2..a631ffd188 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -52,12 +52,14 @@ and intro_pattern_naming = intro_pattern_naming_r located and intro_pattern_action = intro_pattern_action_r located and or_and_intro_pattern = or_and_intro_pattern_r located -type occurrences = +type occurrences_r = | QAllOccurrences | QAllOccurrencesBut of int located or_anti list | QNoOccurrences | QOnlyOccurrences of int located or_anti list +type occurrences = occurrences_r located + type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_flag type clause_r = diff --git a/src/tac2quote.ml b/src/tac2quote.ml index 73fd7c29c3..b3d174dc2d 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -149,7 +149,7 @@ let of_hyp_location_flag ?loc = function | Locus.InHypTypeOnly -> std_constructor ?loc "InHypTypeOnly" [] | Locus.InHypValueOnly -> std_constructor ?loc "InHypValueOnly" [] -let of_occurrences ?loc occ = match occ with +let of_occurrences (loc, occ) = match occ with | QAllOccurrences -> std_constructor ?loc "AllOccurrences" [] | QAllOccurrencesBut occs -> let map occ = of_anti of_int occ in @@ -164,14 +164,14 @@ let of_occurrences ?loc occ = match occ with let of_hyp_location ?loc ((occs, id), flag) = of_tuple ?loc [ of_anti of_ident id; - of_occurrences ?loc occs; + of_occurrences occs; of_hyp_location_flag ?loc flag; ] let of_clause (loc, cl) = let loc = Option.default dummy_loc loc in let hyps = of_option ~loc (fun l -> of_list ~loc of_hyp_location l) cl.q_onhyps in - let concl = of_occurrences ~loc cl.q_concl_occs in + let concl = of_occurrences cl.q_concl_occs in CTacRec (loc, [ std_proj "on_hyps", hyps; std_proj "on_concl", concl; diff --git a/src/tac2quote.mli b/src/tac2quote.mli index c02493c554..4e563990be 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -47,6 +47,8 @@ val of_induction_clause : induction_clause -> raw_tacexpr val of_rewriting : rewriting -> raw_tacexpr +val of_occurrences : occurrences -> raw_tacexpr + val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr (** id ↦ 'Control.hyp @id' *) |