diff options
Diffstat (limited to 'src/versions/standard/structures.mli')
| -rw-r--r-- | src/versions/standard/structures.mli | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 600503d..f7c4f91 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -1,3 +1,15 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr val gen_constant : string list list -> string -> Term.constr lazy_t val int63_modules : string list list @@ -39,13 +51,13 @@ val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds val lift : int -> Constr.constr -> Constr.constr type rel_decl = Context.Rel.Declaration.t val destruct_rel_decl : rel_decl -> Names.Name.t * Constr.t -type constr_expr = Constrexpr.constr_expr val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr val tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic val tclTHENLAST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic +val vm_conv : Reduction.conv_pb -> Term.types Reduction.kernel_conversion_function val vm_cast_no_check : Term.constr -> unit Proofview.tactic val mk_tactic : (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) -> @@ -53,8 +65,17 @@ val mk_tactic : val set_evars_tac : Term.constr -> unit Proofview.tactic val ppconstr_lsimpleconstr : Ppconstr.precedence val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr +val get_rel_dec_name : Context.Rel.Declaration.t -> Names.Name.t + + +(* New packaging of plugins *) 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 + + +(* Types in the Coq source code *) type tactic = unit Proofview.tactic +type names_id = Names.Id.t +type constr_expr = Constrexpr.constr_expr |