1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 845c4eee1..0720273bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -113,11 +113,6 @@ let decompose_these c l =
   general_decompose (fun (_,t) -> head_in indl t gl) c
   end
 
-let decompose_nonrec c =
-  general_decompose
-    (fun (_,t) -> is_non_recursive_type t)
-    c
-
 let decompose_and c =
   general_decompose
     (fun (_,t) -> is_record t)