Revision 94b1fdd79703ee5c9a164c3ab32e7c8c8db08e28 authored by Lennard Gäher on 17 September 2019, 07:20:29 UTC, committed by Lennard Gäher on 17 September 2019, 07:20:29 UTC
1 parent ccf1674
plugin_core.mli
(* this file is the interface that extracted plugins will use.
*)
type ident = Names.Id.t (* Template.BasicAst.ident *)
type qualid = Libnames.qualid (* Template.BasicAst.ident *)
type kername = Names.KerName.t (* Template.BasicAst.kername *)
type reduction_strategy = Redexpr.red_expr (* Template.TemplateMonad.Common.reductionStrategy *)
type global_reference = Globnames.global_reference (* Template.Ast.global_reference *)
type term = Constr.t (* Template.Ast.term *)
type mutual_inductive_body = Declarations.mutual_inductive_body (* Template.Ast.mutual_inductive_body *)
type constant_entry = Declarations.constant_body (* Template.Ast.constant_entry *)
type mutual_inductive_entry = Entries.mutual_inductive_entry (* Template.Ast.mutual_inductive_entry *)
val rs_cbv : reduction_strategy
val rs_cbn : reduction_strategy
val rs_hnf : reduction_strategy
val rs_all : reduction_strategy
val rs_lazy : reduction_strategy
val rs_unfold : Environ.env -> global_reference -> reduction_strategy
type 'a tm
val run : 'a tm -> Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> 'a -> unit) -> unit
val with_env_evm : (Environ.env -> Evd.evar_map -> 'a tm) -> 'a tm
val run_vernac : 'a tm -> unit
val tmReturn : 'a -> 'a tm
val tmBind : 'a tm -> ('a -> 'b tm) -> 'b tm
val tmMap : ('a -> 'b) -> 'a tm -> 'b tm
val tmPrint : term -> unit tm
val tmMsg : string -> unit tm
val tmFail : Pp.t -> 'a tm
val tmFailString : string -> 'a tm
val tmEval : reduction_strategy -> term -> term tm
val tmDefinition : ident -> ?poly:bool -> term option -> term -> kername tm
val tmAxiom : ident -> ?poly:bool -> term -> kername tm
val tmLemma : ident -> ?poly:bool -> term -> kername tm
val tmFreshName : ident -> ident tm
val tmAbout : qualid -> global_reference option tm
val tmAboutString : string -> global_reference option tm
val tmCurrentModPath : Names.ModPath.t tm
val tmQuoteInductive : kername -> (Names.MutInd.t * mutual_inductive_body) option tm
val tmQuoteUniverses : UGraph.t tm
val tmQuoteConstant : kername -> bool -> constant_entry tm
val tmInductive : mutual_inductive_entry -> unit tm
val tmExistingInstance : kername -> unit tm
val tmInferInstance : term -> term option tm
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...