diff options
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 7b8b93377b..fa263cbeb7 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -28,18 +28,21 @@ 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. - ~lax is for debug printing, when the constr might not be well typed in + ~lax is for debug printing, when the constr might not be well typed in 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 @@ -92,5 +95,3 @@ val toggle_scope_printing : val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit - - |