diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 02:37:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-27 22:01:36 +0200 |
| commit | 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 (patch) | |
| tree | 77f792ccddcc48229c08f321666c85debc4b008f /vernac/himsg.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 'vernac/himsg.mli')
| -rw-r--r-- | vernac/himsg.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 1d3807502..91caddcf1 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t +val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t val explain_typeclass_error : env -> typeclass_error -> Pp.t |