diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-03-15 11:23:55 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-15 11:23:55 +0100 |
| commit | ae455fa3aa29c872c9c5b2736fff861afebcd051 (patch) | |
| tree | 1db2df3a7bd9ca076ea4007d59557a549af9dc04 /src/versions/standard/structures.mli | |
| parent | 4a610de645ca2bb505c97dd082220a57595019ad (diff) | |
| download | smtcoq-ae455fa3aa29c872c9c5b2736fff861afebcd051.tar.gz smtcoq-ae455fa3aa29c872c9c5b2736fff861afebcd051.zip | |
V8.9 (#43)
* New syntax for implicit arguments
* Towards 8.9: problems with Micromega plugin
* Move to _CoqProject
* Back to name Makefile
* Switch to Makefile.local instead of -extra
* The compilation issue is a Coq bug
* Ok with 8.9
* INSTALL with 8.9
* Everything ok with 8.9
Diffstat (limited to 'src/versions/standard/structures.mli')
| -rw-r--r-- | src/versions/standard/structures.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 3d6f6b2..3aa8b3b 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -87,13 +87,13 @@ val mkTrace : (* Micromega *) -module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils +module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega_full val micromega_coq_proofTerm : constr lazy_t -val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr +val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr (* Tactics *) @@ -110,11 +110,11 @@ val set_evars_tac : constr -> tactic type constr_expr = Constrexpr.constr_expr val error : string -> 'a val extern_constr : constr -> constr_expr -val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr +val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr -val ppconstr_lsimpleconstr : Notation_term.tolerability +val ppconstr_lsimpleconstr : Notation_gram.tolerability val constrextern_extern_constr : constr -> constr_expr -val get_rel_dec_name : Context.Rel.Declaration.t -> name +val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function |