diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 15:55:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 16:49:13 +0100 |
| commit | 8e77752080b6f0da3ce396e7537db9676e848a70 (patch) | |
| tree | 6594808c65b87513ed9f08e3aff042c2c701d60b /tactics | |
| parent | 5b4fd2f5a3c6d031d551f9b5730fe30a69337c76 (diff) | |
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 14 |
2 files changed, 16 insertions, 0 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 74d98176a..7da6df717 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -19,6 +19,8 @@ open Sigma.Notations DECLARE PLUGIN "coretactics" +(** Basic tactics *) + TACTIC EXTEND reflexivity [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 8f336cdb3..9946aea82 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -17,6 +17,20 @@ open Tacinterp open Misctypes open Locus +(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *) + +let create_generic_quotation name e wit = + let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in + Egramcoq.create_ltac_quotation name inject (e, None) + +let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr +let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr +let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern +let () = create_generic_quotation "int" Pcoq.Prim.integer Stdarg.wit_int +let () = + let inject (loc, v) = Tacexpr.Tacexp v in + Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) + (* Rewriting orientation *) let _ = Metasyntax.add_token_obj "<-" |