diff options
Diffstat (limited to 'toplevel/record.mli')
| -rw-r--r-- | toplevel/record.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/record.mli b/toplevel/record.mli index 1419b9c3c..90b40020e 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -12,6 +12,7 @@ open Names open Term open Sign +open Vernacexpr (*i*) (* [declare_projections ref coers params fields] declare projections of @@ -22,5 +23,5 @@ val declare_projections : inductive -> bool list -> rel_context -> constant option list val definition_structure : - bool * identifier * (identifier * Genarg.constr_ast) list * - (bool * Vernacexpr.local_decl_expr) list * identifier * sorts -> unit + identifier with_coercion * (identifier * Genarg.constr_ast) list * + (local_decl_expr with_coercion) list * identifier * sorts -> unit |