From ef0ae9cd013886345ae061212e01ef02c621a120 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 1 Apr 2020 12:30:43 +0200 Subject: Compiles with Coq-8.11 --- src/versions/standard/structures.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/versions/standard/structures.mli') diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 950135c..78c948c 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -43,11 +43,11 @@ val mkArrow : types -> types -> constr val pr_constr_env : Environ.env -> constr -> Pp.t val pr_constr : constr -> Pp.t -val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry -val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry +val mkUConst : constr -> Evd.side_effects Declare.proof_entry +val mkTConst : constr -> constr -> types -> Evd.side_effects Declare.proof_entry val declare_new_type : id -> types val declare_new_variable : id -> types -> constr -val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t +val declare_constant : id -> Evd.side_effects Declare.proof_entry -> Names.Constant.t type cast_kind val vmcast : cast_kind -- cgit