diff options
Diffstat (limited to 'src/versions/native/structures.mli')
| -rw-r--r-- | src/versions/native/structures.mli | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index b4d9731..9ec21d2 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -24,7 +24,6 @@ val mkTrace : 'b -> 'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr type names_id_t = Names.identifier -val dummy_loc : Pp.loc val mkUConst : Term.constr -> Entries.definition_entry val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry val error : string -> 'a @@ -40,8 +39,11 @@ val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic val assert_before : Names.name -> Term.types -> Proof_type.tactic + val vm_conv : Reduction.conv_pb -> Term.types Reduction.conversion_function val vm_cast_no_check : Term.constr -> Proof_type.tactic +val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr + val mk_tactic : (Environ.env -> Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) -> @@ -50,16 +52,24 @@ val set_evars_tac : 'a -> Proof_type.tactic val ppconstr_lsimpleconstr : Ppconstr.precedence val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr val get_rel_dec_name : 'a -> Names.name +val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr -(* Old packaging of plugins *) +(* Micromega *) module Micromega_plugin_Certificate = Certificate module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils +val micromega_coq_proofTerm : Term.constr lazy_t +val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr + (* Types in the Coq source code *) type tactic = Proof_type.tactic type names_id = Names.identifier type constr_expr = Topconstr.constr_expr + +(* EConstr *) +type econstr = Term.constr +val econstr_of_constr : Term.constr -> econstr |