diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /interp/constrintern.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r-- | interp/constrintern.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 22cf910b..61e7c6f5 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ open Libnames @@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map ref -> local_binder list -> - internalization_env * ((env * rel_context) * Impargs.manual_implicits) + internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) @@ -178,7 +177,7 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : named_context -> Id.t -> constr +val construct_reference : Context.Named.t -> Id.t -> constr val global_reference : Id.t -> constr val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr @@ -186,8 +185,8 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr guaranteed to have the same domain as the input one. *) val interp_notation_constr : ?impls:internalization_env -> notation_interp_env -> constr_expr -> - (subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr + (bool * subscopes * notation_var_internalization_type) Id.Map.t * + notation_constr * reversibility_flag (** Globalization options *) val parsing_explicit : bool ref |