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/notation.mli | |
| 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/notation.mli')
| -rw-r--r-- | interp/notation.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 842f2b1458..b427aa9bb3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -264,13 +264,13 @@ type scope_class val scope_class_compare : scope_class -> scope_class -> int val subst_scope_class : - Mod_subst.substitution -> scope_class -> scope_class option + Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit -val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list -val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option +val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list +val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option |