diff options
| author | Maxime Dénès | 2018-03-04 16:50:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:50:36 +0100 |
| commit | b3a8761790c0905aad8e5d3102fab606fe5e7fd6 (patch) | |
| tree | ce5fbe8cb717bad677ad755e7875413d3e5d0e84 /interp/notation.mli | |
| parent | 9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (diff) | |
| parent | 886a9c2fb25e32bd87b3fce38023b3e701134d23 (diff) | |
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
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 a4c79d6d35..79b56bd410 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -163,10 +163,10 @@ val subst_scope_class : Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit -val declare_ref_arguments_scope : global_reference -> unit +val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit -val compute_arguments_scope : Constr.types -> scope_name option list -val compute_type_scope : Constr.types -> scope_name option +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 (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option |