diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 12:34:30 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 12:34:30 +0100 |
| commit | 78bad016e389cd78635d40281bfefd7136733b7e (patch) | |
| tree | 51f90da34d2444734868d7954412ac08ddc0f5c6 /interp | |
| parent | f8eb2ed4ddbe2199187696f51c42734014f4d9d0 (diff) | |
| parent | 9d991d36c07efbb6428e277573bd43f6d56788fc (diff) | |
merge
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.mli | 3 | ||||
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 5 |
3 files changed, 5 insertions, 7 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index b797e455c..ff8ca0b7c 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Termops open Environ open Libnames @@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - rel_context -> local_binder list + Context.Rel.t -> local_binder list (** Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f9de8c466..68bc0b109 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -101,7 +101,7 @@ let global_reference id = let construct_reference ctx id = try - Term.mkVar (let _ = Context.lookup_named id ctx in id) + Term.mkVar (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id @@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = str "variable " ++ pr_id id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) - let _ = Context.lookup_named id namedctx in + let _ = Context.Named.lookup id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b671c9881..c851fbb36 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 |