diff options
| author | Hugo Herbelin | 2019-11-18 16:04:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | 490704f4b2db98f4ef15f5e380b63e49e13a418b (patch) | |
| tree | 625e60c878e2768dbce36129e1df80ceace17495 /interp/constrextern.mli | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
Moving the diversity of constr printers to a label style.
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index aa6aa5f5f9..fa263cbeb7 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -28,7 +28,8 @@ 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_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr -val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr +val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> + env -> Evd.evar_map -> closed_glob_constr -> constr_expr (** If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed. @@ -36,10 +37,12 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob env, sigma *) -val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr -val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr +val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> + env -> Evd.evar_map -> constr -> constr_expr +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 : bool -> env -> Evd.evar_map -> types -> constr_expr +val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> 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 |