diff options
| author | Pierre-Marie Pédrot | 2019-03-14 19:00:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:03:19 +0200 |
| commit | 2a79abc613bdf19b53685a40c993f964455904fe (patch) | |
| tree | c0fd8ab20f683c3141934d060852dcda0d569f00 /interp/constrintern.ml | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
No more local reduction functions in Reductionops.
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f82783f47d..a1aac60b35 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -187,7 +187,7 @@ let empty_internalization_env = Id.Map.empty let compute_internalization_data env sigma id ty typ impl = let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in - (ty, impl, compute_arguments_scope sigma typ, var_uid id) + (ty, impl, compute_arguments_scope env sigma typ, var_uid id) let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 @@ -2358,9 +2358,9 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty -let scope_of_type_kind sigma = function +let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope sigma typ + | OfType typ -> compute_type_scope env sigma typ | WithoutTypeConstraint | UnknownIfTermOrType -> None let allowed_binder_kind_of_type_kind = function @@ -2377,7 +2377,7 @@ let empty_ltac_sign = { let intern_gen kind env sigma ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = - let tmp_scope = scope_of_type_kind sigma kind in + let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; @@ -2462,7 +2462,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = - let tmp_scope = scope_of_type_kind sigma kind in + let tmp_scope = scope_of_type_kind env sigma kind in let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env |