From d531f81802c0e152e83868f467b46721e65445a9 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 2 Jan 2016 16:55:35 +0100
Subject: Remove duplicate declarations.

---
 pretyping/reductionops.mli | 1 -
 tactics/taccoerce.mli      | 3 ---
 2 files changed, 4 deletions(-)

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 43c98bbd47..30c7ded243 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -222,7 +222,6 @@ val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_prod_assum :
   env ->  evar_map -> constr -> rel_context * constr
-val is_sort : env -> evar_map -> types -> bool
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 0754c15363..56a90e8d5b 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -54,9 +54,6 @@ val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t
 
 val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
-val coerce_to_intro_pattern_naming :
-  Environ.env -> Value.t -> intro_pattern_naming_expr
-
 val coerce_to_intro_pattern_naming :
   Environ.env -> Value.t -> intro_pattern_naming_expr
 
-- 
cgit v1.2.3