diff options
| author | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
| commit | 3ae4231d30edfa928595b6fa886ce6df1a495089 (patch) | |
| tree | d6c1d749e6435570e3437f012aad8e6d6797c432 /interp/constrextern.mli | |
| parent | 1d8698e97dee385151ef92efd924560b296f8d50 (diff) | |
| parent | ea16c402392722a44bf2227aef7ff73faef70d3a (diff) | |
Merge PR #11795: Print implicit arguments in types of references
Ack-by: herbelin
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index fe64661a66..f85e49d2df 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -25,7 +25,7 @@ open Ltac_pretype val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -42,7 +42,7 @@ val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid -val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr +val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list |