Up – Package index » coq-core » Sources » tuto1_plugin » inspector.mlcoq-core README Library btauto_plugin Library cc_plugin Library coq-core.boot Library coq-core.clib Library coq-core.config Library coq-core.coqworkmgrapi Library coq-core.engine Library coq-core.gramlib Library coq-core.interp Library coq-core.kernel Library coq-core.lib Library coq-core.library Library coq-core.parsing Library coq-core.plugins Library coq-core.pretyping Library coq-core.printing Library coq-core.proofs Library coq-core.stm Library coq-core.sysinit Library coq-core.tactics Library coq-core.top_printers Library coq-core.toplevel Library coq-core.vernac Library coq-core.vm Library derive_plugin Library extraction_plugin Library firstorder_plugin Library funind_plugin Library ltac2_plugin Library ltac_plugin Library micromega_plugin Library nsatz_plugin Library number_string_notation_plugin Library ring_plugin Library rtauto_plugin Library ssreflect_plugin Library ssrmatching_plugin Library tauto_plugin Library tuto0_plugin Library tuto1_plugin Library tuto2_plugin Library tuto3_plugin Library zify_plugin Sources btauto_plugin cc_plugin coq-core.boot coq-core.clib coq-core.config coq-core.coqworkmgrapi coq-core.engine coq-core.gramlib coq-core.interp coq-core.kernel coq-core.lib coq-core.library coq-core.parsing coq-core.pretyping coq-core.printing coq-core.proofs coq-core.stm coq-core.sysinit coq-core.tactics coq-core.top_printers coq-core.toplevel coq-core.vernac coq-core.vm derive_plugin extraction_plugin firstorder_plugin funind_plugin ltac2_plugin ltac_plugin micromega_plugin nsatz_plugin number_string_notation_plugin ring_plugin rtauto_plugin ssreflect_plugin ssrmatching_plugin tauto_plugin tuto0_plugin tuto1_plugin tuto2_plugin tuto3_plugin zify_plugin 1
2
3
4
5
6
7
8
open Pp
let print_input ( a : ' a ) ( printer : ' a -> Pp . t ) ( type_str : string ) : unit =
let msg = printer a ++ strbrk ( Printf . sprintf " is a %s." type_str ) in
Feedback . msg_notice msg