diff options
| author | Hugo Herbelin | 2018-03-27 02:37:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-06-27 22:01:36 +0200 |
| commit | 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 (patch) | |
| tree | 77f792ccddcc48229c08f321666c85debc4b008f /interp/implicit_quantifiers.mli | |
| parent | c33988dafcad14f9f0c10a287d2cfb2790e253c4 (diff) | |
Swapping Context and Constr: defining declarations on constr in Constr.
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
Diffstat (limited to 'interp/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index a8492095ec..437fef1753 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,14 +38,14 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t (* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a |