diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-20 01:04:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 13:07:22 +0200 |
| commit | 2cb554aa772c5c6d179c6a4611b70d459073a316 (patch) | |
| tree | 4493ad52bb7adf03128de2bba63d46f26a893a77 /parsing/pcoq.ml | |
| parent | 403af31e3d0bc571acf0a66907277ad839c94df4 (diff) | |
Exporting a generic argument induction_arg. As a consequence,
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index efb89cd6e..7d1c63ee0 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -345,6 +345,7 @@ module Tactic = make_gen_entry utactic "uconstr" let quantified_hypothesis = make_gen_entry utactic "quantified_hypothesis" + let destruction_arg = make_gen_entry utactic "destruction_arg" let int_or_var = make_gen_entry utactic "int_or_var" let red_expr = make_gen_entry utactic "red_expr" let simple_intropattern = @@ -520,4 +521,5 @@ let () = Grammar.register0 wit_tactic (Tactic.tactic); Grammar.register0 wit_ltac (Tactic.tactic); Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); + Grammar.register0 wit_destruction_arg (Tactic.destruction_arg); () |