diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-04-01 12:30:43 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-04-01 12:30:43 +0200 |
| commit | ef0ae9cd013886345ae061212e01ef02c621a120 (patch) | |
| tree | f954ab2dc5e1e547c86dad1d13e639bd389ee364 /src/versions/standard/structures.mli | |
| parent | 632b7b11b25f78461872f50621b325321678810c (diff) | |
| download | smtcoq-ef0ae9cd013886345ae061212e01ef02c621a120.tar.gz smtcoq-ef0ae9cd013886345ae061212e01ef02c621a120.zip | |
Compiles with Coq-8.11
Diffstat (limited to 'src/versions/standard/structures.mli')
| -rw-r--r-- | src/versions/standard/structures.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |