diff options
| -rw-r--r-- | pretyping/reductionops.ml | 9 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 |
2 files changed, 9 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c9ab57d02c..f6859bc199 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -632,7 +632,7 @@ let splay_lambda env sigma = let splay_prod_assum env sigma = let rec prodec_rec env l c = let t = whd_betadeltaiota_nolet env sigma c in - match kind_of_term c with + match kind_of_term t with | Prod (x,t,c) -> prodec_rec (push_rel (x,None,t) env) (Sign.add_rel_decl (x, None, t) l) c @@ -662,6 +662,13 @@ let decomp_n_prod env sigma n = in decrec env n Sign.empty_rel_context +exception NotASort + +let decomp_sort env sigma t = + match kind_of_term (whd_betadeltaiota env sigma t) with + | Sort s -> s + | _ -> raise NotASort + (* One step of approximation *) let rec apprec env sigma s = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 42a53224a6..8d04cb7998 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -132,6 +132,7 @@ val decomp_n_prod : env -> evar_map -> int -> constr -> Sign.rel_context * constr val splay_prod_assum : env -> evar_map -> constr -> Sign.rel_context * constr +val decomp_sort : env -> evar_map -> types -> sorts type 'a miota_args = { mP : constr; (* the result type *) |