Merge PR #11417: Move kind_of_type from the kernel to EConstr.

Reviewed-by: SkySkimmer
Reviewed-by: gares

6 files changed, 40 insertions, 31 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index de3c660938..f95672a15d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -906,10 +906,11 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
      mk_term ' ' (force_type ty) in
    let strip_cast (sigma, t) =
-     let rec aux t = match EConstr.kind_of_type sigma t with
-     | CastType (t, ty) when !n_binders = 0 && EConstr.isSort sigma ty -> t
-     | ProdType(n,s,t) -> decr n_binders; EConstr.mkProd (n, s, aux t)
-     | LetInType(n,v,ty,t) -> decr n_binders; EConstr.mkLetIn (n, v, ty, aux t)
+     let open EConstr in
+     let rec aux t = match kind_of_type sigma t with
+     | CastType (t, ty) when !n_binders = 0 && isSort sigma ty -> t
+     | ProdType(n,s,t) -> decr n_binders; mkProd (n, s, aux t)
+     | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t)
      | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in
      sigma, aux t in
    let sigma, cty as ty = strip_cast (interp_term ist gl ty) in
@@ -930,11 +931,12 @@ exception NotEnoughProducts
 let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m
 =
   let rec loop ty args sigma n =
+  let open EConstr in
   if n = 0 then
     let args = List.rev args in
      (if beta then Reductionops.whd_beta sigma else fun x -> x)
       (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma
-  else match EConstr.kind_of_type sigma ty with
+  else match kind_of_type sigma ty with
   | ProdType (_, src, tgt) ->
       let sigma = create_evar_defs sigma in
       let (sigma, x) =
@@ -947,7 +949,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   | AtomicType _ ->
       let ty =  (* FIXME *)
         (Reductionops.whd_all env sigma) ty in
-      match EConstr.kind_of_type sigma ty with
+      match kind_of_type sigma ty with
       | ProdType _ -> loop ty args sigma n
       | _ -> raise NotEnoughProducts
   in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 26962ee87b..7baccd3d75 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,16 +34,17 @@ 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
-  | AtomicType (hd, args) when EConstr.isRel sigma hd ->
-    ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t
+  let open EConstr in
+  let rec loop ctx t = match kind_of_type sigma t with
+  | 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
@@ -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 =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index df001b6084..895f491510 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -13,7 +13,6 @@
 open Ltac_plugin
 open Util
 open Names
-open Term
 open Constr
 open Context
 open Vars
@@ -379,7 +378,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
         let hd_ty = Retyping.get_type_of env sigma hd in
         let names = let rec aux t = function 0 -> [] | n ->
           let t = Reductionops.whd_all env sigma t in
-          match EConstr.kind_of_type sigma t with
+          let open EConstr in
+          match kind_of_type sigma t with
           | ProdType (name, _, t) -> name.binder_name :: aux t (n-1)
           | _ -> assert false in aux hd_ty (Array.length args) in
         hd_ty, Util.List.map_filter (fun (t, name) ->
@@ -412,7 +412,8 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
       let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
-      match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
+      let open EConstr in
+      match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 235dfc257d..a6b9a43778 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -361,8 +361,9 @@ let intro_lock ipats =
         let c = Proofview.Goal.concl gl in
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        match EConstr.kind_of_type sigma c with
-        | Term.AtomicType(hd, args) when
+        let open EConstr in
+        match kind_of_type sigma c with
+        | AtomicType(hd, args) when
             Array.length args >= 2 && is_app_evar sigma (Array.last args) &&
             Ssrequality.ssr_is_setoid env sigma hd args
             (* if the last condition above [ssr_is_setoid ...] holds
@@ -375,8 +376,8 @@ let intro_lock ipats =
           protect_subgoal env sigma hd args
         | _ ->
         let t = Reductionops.whd_all env sigma c in
-        match EConstr.kind_of_type sigma t with
-        | Term.AtomicType(hd, args) when
+        match kind_of_type sigma t with
+        | AtomicType(hd, args) when
             Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
             Array.length args = 3 && is_app_evar sigma args.(2) ->
           protect_subgoal env sigma hd args
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 580c0423e9..843adb40ac 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -610,8 +610,9 @@ let tclCompileIPats = IpatMachine.tclCompileIPats
 let with_defective maintac deps clr = Goal.enter begin fun g ->
   let sigma, concl = Goal.(sigma g, concl g) in
   let top_id =
-    match EConstr.kind_of_type sigma concl with
-    | Term.ProdType ({binder_name=Name id}, _, _)
+    let open EConstr in
+    match kind_of_type sigma concl with
+    | ProdType ({binder_name=Name id}, _, _)
       when Ssrcommon.is_discharged_id id -> id
     | _ -> Ssrcommon.top_id in
   let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in
@@ -641,10 +642,11 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
     | Some (IPatId ipat) when not is_rec ->
        let rec intro_eq () = Goal.enter begin fun g ->
          let sigma, env, concl = Goal.(sigma g, env g, concl g) in
-         match EConstr.kind_of_type sigma concl with
-         | Term.ProdType (_, src, tgt) -> begin
-             match EConstr.kind_of_type sigma src with
-             | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
+         let open EConstr in
+         match kind_of_type sigma concl with
+         | ProdType (_, src, tgt) -> begin
+             match kind_of_type sigma src with
+             | AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
                 V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*>
                 Ssrcommon.tclINTRO_ID ipat
              | _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq ()
@@ -669,8 +671,9 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
          let sigma, eq =
            EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in
          let ctx, last = EConstr.decompose_prod_assum sigma concl in
-         let args = match EConstr.kind_of_type sigma last with
-           | Term.AtomicType (hd, args) ->
+         let open EConstr in
+         let args = match kind_of_type sigma last with
+           | AtomicType (hd, args) ->
                if Ssrcommon.is_protect hd env sigma then args
                else Ssrcommon.errorstrm
                   (Pp.str "Too many names in intro pattern")
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index f91b5e7aa2..d051836ebc 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -95,8 +95,9 @@ applied to the first assumption in the goal *)
 let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl ->
   let concl = Goal.concl gl in
   let id = (* We keep the orig name for checks in "in" tcl *)
-    match EConstr.kind_of_type (Goal.sigma gl) concl with
-    | Term.ProdType({binder_name=Name.Name id}, _, _)
+    let open EConstr in
+    match kind_of_type (Goal.sigma gl) concl with
+    | ProdType({binder_name=Name.Name id}, _, _)
       when Ssrcommon.is_discharged_id id -> id
     | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in
   let view = EConstr.mkVar id in