From 2cb554aa772c5c6d179c6a4611b70d459073a316 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Dec 2015 01:04:15 +0100 Subject: Exporting a generic argument induction_arg. As a consequence, simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq. --- parsing/pcoq.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'parsing/pcoq.ml') 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); () -- cgit v1.2.3