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"?
---
 plugins/ssr/ssrelim.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/ssr/ssrelim.ml')

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 26962ee87b..ada42a1c9b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -13,7 +13,6 @@
 open Util
 open Names
 open Printer
-open Term
 open Constr
 open Context
 open Termops
@@ -35,7 +34,8 @@ module RelDecl = Context.Rel.Declaration
  * argument (index), it computes it's arity and the arity of the eliminator and
  * checks if the eliminator is recursive or not *)
 let analyze_eliminator elimty env sigma =
-  let rec loop ctx t = match EConstr.kind_of_type sigma t with
+  let open EConstr in
+  let rec loop ctx t = match kind_of_type sigma t with
   | AtomicType (hd, args) when EConstr.isRel sigma hd ->
     ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t
   | CastType (t, _) -> loop ctx t
@@ -243,7 +243,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     let sigma = project gl in
     ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
     ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
-  let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with
+  let open EConstr in
+  let inf_deps_r = match kind_of_type (project gl) elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
   let saturate_until gl c c_ty f =
-- 
cgit v1.2.3


From b468bb9e7110be4e1a1c9b13da16720b64d1125e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 5 Feb 2020 16:38:47 +0100
Subject: [cleanup] remove useless EConstr qualifications

---
 plugins/ssr/ssrelim.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/ssr/ssrelim.ml')

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index ada42a1c9b..7baccd3d75 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -36,15 +36,15 @@ module RelDecl = Context.Rel.Declaration
 let analyze_eliminator elimty env sigma =
   let open EConstr in
   let rec loop ctx t = match kind_of_type sigma t with
-  | AtomicType (hd, args) when EConstr.isRel sigma hd ->
-    ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t
+  | AtomicType (hd, args) when isRel sigma hd ->
+    ctx, destRel sigma hd, not (Vars.noccurn sigma 1 t), Array.length args, t
   | CastType (t, _) -> loop ctx t
   | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t
-  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (EConstr.Vars.subst1 b t)
+  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (Vars.subst1 b t)
   | _ ->
-    let env' = EConstr.push_rel_context ctx env in
+    let env' = push_rel_context ctx env in
     let t' = Reductionops.whd_all env' sigma t in
-    if not (EConstr.eq_constr sigma t t') then loop ctx t' else
+    if not (eq_constr sigma t t') then loop ctx t' else
       errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
       str"A (applied) bound variable was expected as the conclusion of "++
       str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
-- 
cgit v1.2.3