diff options
| author | herbelin | 2006-03-28 16:05:43 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-28 16:05:43 +0000 |
| commit | 7f3d1f577b2d539eb8019b6390c7400d4a29a36b (patch) | |
| tree | f4fd93bba937216db099a261e5e502a9db53bf6f | |
| parent | 49ef74982e3d810b9296dd62a7ba30053ceb8e63 (diff) | |
Correction bug/typo dans splay_prod_assum et ajout decomp_sort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8668 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 *) |