diff options
| author | Maxime Dénès | 2020-02-12 10:27:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:42 +0200 |
| commit | c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 (patch) | |
| tree | 9ebe8a6c3959c670a9cff263cfa6d08f196bbc99 /interp/constrintern.mli | |
| parent | d03529ab8fec0cad5705b5f775e43ef26c0dedcb (diff) | |
Remove special case for implicit inductive parameters
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 9d36bf2151..fb1c6684a1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -48,10 +48,6 @@ type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) - Id.t list * - (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" - in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Impargs.implicit_status list * (* signature of impargs of the variable *) Notation_term.scope_name option list (* subscopes of the args of the variable *) @@ -132,7 +128,7 @@ val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> evar_map * (constr * Impargs.manual_implicits) -val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map -> +val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * (types * Impargs.manual_implicits) |