From 5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 25 Apr 2016 14:31:11 +0200
Subject: Fixing a "This clause is redundant" error when interpreting the "in"
 clause of a "match" over an irrefutable pattern.

---
 pretyping/cases.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/cases.mli')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 257d1e578..d7fff8af4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -32,6 +32,8 @@ val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> '
 
 val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
 
+val irrefutable : env -> cases_pattern -> bool
+
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
-- 
cgit v1.2.3