From 1fe97f12f24f596ab2408348e7556d483ed58e96 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Sep 2006 11:18:17 +0000
Subject: Ajout is_sort: test si se réduit en une sorte

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml  | 4 ++++
 pretyping/reductionops.mli | 1 +
 2 files changed, 5 insertions(+)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2cb7b80f73..76a053872a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -770,6 +770,10 @@ let decomp_sort env sigma t =
   | Sort s -> s
   | _ -> raise NotASort
 
+let is_sort env sigma arity =
+  try let _ = decomp_sort env sigma arity in true 
+  with NotASort -> false
+
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 0ac1fe1188..987d07912f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -164,6 +164,7 @@ val decomp_n_prod :
 val splay_prod_assum :
   env ->  evar_map -> constr -> Sign.rel_context * constr
 val decomp_sort : env -> evar_map -> types -> sorts
+val is_sort : env -> evar_map -> types -> bool
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
-- 
cgit v1.2.3