From 238b0cb82a1e66332131f10de79f4abe55d4b0b2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jan 2020 13:40:10 +0100
Subject: Move kind_of_type from the kernel to ssr.

It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.

Fixes #9390: What is the purpose of the function "kind_of_type"?
---
 pretyping/arguments_renaming.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 36f35a67c3..59ca418a39 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -11,7 +11,6 @@
 (*i*)
 open Names
 open Globnames
-open Term
 open Constr
 open Context
 open Environ
@@ -78,14 +77,14 @@ let rename_type ty ref =
   let rec rename_type_aux c = function
     | [] -> c
     | rename :: rest as renamings ->
-        match kind_of_type c with
-        | ProdType (old, s, t) ->
+        match Constr.kind c with
+        | Prod (old, s, t) ->
             mkProd (name_override old rename, s, rename_type_aux t rest)
-        | LetInType(old, s, b, t) ->
+        | LetIn (old, s, b, t) ->
             mkLetIn (old ,s, b, rename_type_aux t renamings)
-        | CastType (t,_) -> rename_type_aux t renamings
-        | SortType _ -> c
-        | AtomicType _ -> c in
+        | Cast (t,_, _) -> rename_type_aux t renamings
+        | _ -> c
+  in
   try rename_type_aux ty (arguments_names ref)
   with Not_found -> ty
 
-- 
cgit v1.2.3