From 2cb554aa772c5c6d179c6a4611b70d459073a316 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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.

---
 interp/constrarg.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/constrarg.ml')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 011b31d9a..ca828102b 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -61,6 +61,9 @@ let wit_red_expr = make0 "redexpr"
 let wit_clause_dft_concl  =
   make0 "clause_dft_concl"
 
+let wit_destruction_arg =
+  make0 "destruction_arg"
+
 (** Aliases *)
 
 let wit_reference = wit_ref
-- 
cgit v1.2.3