diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 11 | ||||
| -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 | 4 | ||||
| -rw-r--r-- | src/tac2quote.ml | 4 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 |
7 files changed, 17 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 |