diff options
| author | Maxime Dénès | 2020-05-14 16:33:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-05-14 16:33:15 +0200 |
| commit | 81fba800a97955368791df115e807cde66eff19c (patch) | |
| tree | c0cb601061912a95a8b5ad031f0378a1e479320b /interp/notation.mli | |
| parent | 8dd5c47007817c104d57a449409a6b9c6f8ef12e (diff) | |
| parent | 101d898869ffa07fc772b303e3dbb7ecd860386b (diff) | |
Merge PR #11922: No more local reduction functions in Reductionops.
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
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 |