Port is_Set and is_Type to EConstr, as was is_Prop already.

6 files changed, 25 insertions, 17 deletions

diff --git a/API/API.mli b/API/API.mli
index 8b0bef48c9..c90244dcd0 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2810,6 +2810,8 @@ sig
   val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val clear_named_body : Names.Id.t -> Environ.env -> Environ.env
   val is_Prop : Evd.evar_map -> EConstr.constr -> bool
+  val is_Set : Evd.evar_map -> EConstr.constr -> bool
+  val is_Type : Evd.evar_map -> EConstr.constr -> bool
   val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool
 
   val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
diff --git a/engine/termops.ml b/engine/termops.ml
index 2bd0c06d6d..e2bdf72387 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1165,6 +1165,24 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
   | Cast (c,_,_) -> is_Prop sigma c
   | _ -> false
 
+let rec is_Set sigma c = match EConstr.kind sigma c with
+  | Sort u ->
+    begin match EConstr.ESorts.kind sigma u with
+    | Prop Pos -> true
+    | _ -> false
+    end
+  | Cast (c,_,_) -> is_Set sigma c
+  | _ -> false
+
+let rec is_Type sigma c = match EConstr.kind sigma c with
+  | Sort u ->
+    begin match EConstr.ESorts.kind sigma u with
+    | Type _ -> true
+    | _ -> false
+    end
+  | Cast (c,_,_) -> is_Type sigma c
+  | _ -> false
+
 (* eq_constr extended with universe erasure *)
 let compare_constr_univ sigma f cv_pb t1 t2 =
   let open EConstr in
diff --git a/engine/termops.mli b/engine/termops.mli
index 2624afd30d..ef2c52a455 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -267,6 +267,8 @@ val isGlobalRef : Evd.evar_map -> constr -> bool
 val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
 
 val is_Prop : Evd.evar_map -> constr -> bool
+val is_Set : Evd.evar_map -> constr -> bool
+val is_Type : Evd.evar_map -> constr -> bool
 
 (** Combinators on judgments *)
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d07b2e0b45..99493d6982 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1773,11 +1773,6 @@ let onClearedName2 id tac =
       tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
     end)
 
-let rec is_Prop sigma c = match EConstr.kind sigma c with
-  | Sort s -> Sorts.is_prop (ESorts.kind sigma s)
-  | Cast (c,_,_) -> is_Prop sigma c
-  | _ -> false
-
 let destructure_hyps =
   Proofview.Goal.enter begin fun gl ->
   let type_of = Tacmach.New.pf_unsafe_type_of gl in
@@ -1809,7 +1804,7 @@ let destructure_hyps =
           | Kimp(t1,t2) ->
 	      (* t1 and t2 might be in Type rather than Prop.
 		 For t1, the decidability check will ensure being Prop. *)
-              if is_Prop sigma (type_of t2)
+              if Termops.is_Prop sigma (type_of t2)
               then
 		let d1 = decidability t1 in
 		tclTHENLIST [
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 79d2c3333b..0afa694c3c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1103,15 +1103,6 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
 and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
-      let rec is_Type c = match EConstr.kind !evdref c with
-      | Sort s ->
-        begin match ESorts.kind !evdref s with
-        | Type _ -> true
-        | Prop _ -> false
-        end
-      | Cast (c, _, _) -> is_Type c
-      | _ -> false
-      in
       (match valcon with
        | Some v ->
            let s =
@@ -1119,7 +1110,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
 	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
 	       match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
                | Sort s -> ESorts.kind sigma s
-               | Evar ev when is_Type (existential_type sigma ev) ->
+               | Evar ev when is_Type sigma (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
                | _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
            in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2be10a0397..b8f0c4099d 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -418,7 +418,7 @@ let explain_not_product env sigma c =
   let pr = pr_lconstr_env env sigma c in
   str "The type of this term is a product" ++ spc () ++
   str "while it is expected to be" ++
-  (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+  (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
 
 (* TODO: use the names *)
 (* (co)fixpoints *)