diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 18 | ||||
| -rw-r--r-- | src/tac2core.ml | 41 | ||||
| -rw-r--r-- | src/tac2entries.mli | 24 |
3 files changed, 36 insertions, 47 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index e3d48f75ca..e5847119e1 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -326,7 +326,7 @@ GEXTEND Gram [ [ n = Prim.natural -> Loc.tag ~loc:!@loc n ] ] ; q_ident: - [ [ id = ident_or_anti -> Tac2quote.of_anti Tac2quote.of_ident id ] ] + [ [ id = ident_or_anti -> id ] ] ; qhyp: [ [ x = anti -> x @@ -347,7 +347,7 @@ GEXTEND Gram ] ] ; q_bindings: - [ [ bl = with_bindings -> Tac2quote.of_bindings bl ] ] + [ [ bl = with_bindings -> bl ] ] ; intropatterns: [ [ l = LIST0 nonsimple_intropattern -> Loc.tag ~loc:!@loc l ]] @@ -417,10 +417,10 @@ GEXTEND Gram ] ] ; q_intropatterns: - [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ipat ] ] + [ [ ipat = intropatterns -> ipat ] ] ; q_intropattern: - [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ipat ] ] + [ [ ipat = simple_intropattern -> ipat ] ] ; nat_or_anti: [ [ n = lnatural -> QExpr n @@ -487,7 +487,7 @@ GEXTEND Gram ] ] ; q_clause: - [ [ cl = clause -> Tac2quote.of_clause cl ] ] + [ [ cl = clause -> cl ] ] ; concl_occ: [ [ "*"; occs = occs -> occs @@ -506,7 +506,7 @@ GEXTEND Gram ] ] ; q_induction_clause: - [ [ cl = induction_clause -> Tac2quote.of_induction_clause cl ] ] + [ [ cl = induction_clause -> cl ] ] ; orient: [ [ "->" -> Loc.tag ~loc:!@loc (Some true) @@ -539,7 +539,7 @@ GEXTEND Gram ] ] ; q_rewriting: - [ [ r = oriented_rewriter -> Tac2quote.of_rewriting r ] ] + [ [ r = oriented_rewriter -> r ] ] ; tactic_then_last: [ [ "|"; lta = LIST0 OPT tac2expr LEVEL "6" SEP "|" -> lta @@ -556,10 +556,10 @@ GEXTEND Gram ] ] ; q_dispatch: - [ [ d = tactic_then_gen -> Tac2quote.of_dispatch (Loc.tag ~loc:!@loc d) ] ] + [ [ d = tactic_then_gen -> Loc.tag ~loc:!@loc d ] ] ; q_occurrences: - [ [ occs = occs -> Tac2quote.of_occurrences occs ] ] + [ [ occs = occs -> occs ] ] ; END diff --git a/src/tac2core.ml b/src/tac2core.ml index 0415b6f15f..bec1761120 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -14,6 +14,7 @@ open Geninterp open Tac2env open Tac2expr open Tac2interp +open Tac2entries.Pltac open Proofview.Notations (** Standard values *) @@ -868,20 +869,12 @@ end let () = add_scope "tactic" begin function | [] -> (** Default to level 5 parsing *) - let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in + let scope = Extend.Aentryl (tac2expr, 5) in let act tac = tac in Tac2entries.ScopeRule (scope, act) | [SexprInt (loc, n)] -> let () = if n < 0 || n > 6 then scope_fail () in - let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in - let act tac = tac in - Tac2entries.ScopeRule (scope, act) -| _ -> scope_fail () -end - -let () = add_scope "ident" begin function -| [] -> - let scope = Extend.Aentry Tac2entries.Pltac.q_ident in + let scope = Extend.Aentryl (tac2expr, n) in let act tac = tac in Tac2entries.ScopeRule (scope, act) | _ -> scope_fail () @@ -895,27 +888,21 @@ let () = add_scope "thunk" begin function | _ -> scope_fail () end -let () = add_scope "bindings" begin function -| [] -> - let scope = Extend.Aentry Tac2entries.Pltac.q_bindings in - let act tac = tac in - Tac2entries.ScopeRule (scope, act) -| _ -> scope_fail () -end - -let add_expr_scope name entry = +let add_expr_scope name entry f = add_scope name begin function - | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, (fun e -> e)) + | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f) | _ -> scope_fail () end -let () = add_expr_scope "intropattern" Tac2entries.Pltac.q_intropattern -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_expr_scope "ident" q_ident (fun id -> Tac2quote.of_anti Tac2quote.of_ident id) +let () = add_expr_scope "bindings" q_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 "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 +let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences +let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_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 diff --git a/src/tac2entries.mli b/src/tac2entries.mli index cf6cdfa74b..667378030a 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -55,15 +55,17 @@ module Pltac : sig val tac2expr : raw_tacexpr Pcoq.Gram.entry -(** Quoted entries. They directly return an Ltac2 expression *) - -val q_ident : raw_tacexpr Pcoq.Gram.entry -val q_bindings : raw_tacexpr Pcoq.Gram.entry -val q_intropattern : raw_tacexpr Pcoq.Gram.entry -val q_intropatterns : raw_tacexpr Pcoq.Gram.entry -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 +(** Quoted entries. To be used for complex notations. *) + +open Tac2qexpr + +val q_ident : Id.t located or_anti Pcoq.Gram.entry +val q_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_induction_clause : induction_clause Pcoq.Gram.entry +val q_rewriting : rewriting Pcoq.Gram.entry +val q_clause : clause Pcoq.Gram.entry +val q_dispatch : dispatch Pcoq.Gram.entry +val q_occurrences : occurrences Pcoq.Gram.entry end |