diff options
| author | Gaëtan Gilbert | 2018-02-16 16:07:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-16 16:07:17 +0100 |
| commit | 507cd85244db835f13bc65cb9b92aa903180989c (patch) | |
| tree | 5a77bc12bccd9b6dc5475386fb3f361e2a302dbd | |
| parent | 8dd6d091ffbfa237f7266eeca60187263a9b521f (diff) | |
Fix reduction flags in inferCumulativity
The only difference is when we have a rel local definition in the
initial environment, which isn't actually possible. However that
depends on the specific way we treat parameters.
| -rw-r--r-- | pretyping/inferCumulativity.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a0a8276c5c..b369fe4e45 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -159,8 +159,7 @@ and infer_vect infos variances v = let infer_term cv_pb env variances c = let open CClosure in - let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in - let infos = create_clos_infos reds env in + let infos = create_clos_infos all env in infer_fterm cv_pb infos variances (CClosure.inject c) [] let infer_arity_constructor env variances arcn is_arity params = |