Coverage report
77.74%
100%
API/
API.ml
75%
checker/
check.ml
76%
checker/
check_stat.ml
49%
checker/
checker.ml
70%
checker/
closure.ml
13%
checker/
declarations.ml
73%
checker/
environ.ml
61%
checker/
esubst.ml
71%
checker/
indtypes.ml
53%
checker/
inductive.ml
100%
checker/
main.ml
61%
checker/
mod_checking.ml
23%
checker/
modops.ml
43%
checker/
names.ml
1%
checker/
print.ml
62%
checker/
reduction.ml
83%
checker/
safe_typing.ml
0%
checker/
subtyping.ml
73%
checker/
term.ml
0%
checker/
type_errors.ml
81%
checker/
typeops.ml
72%
checker/
univ.ml
55%
checker/
validate.ml
97%
checker/
values.ml
100%
config/
coq_config.ml
92%
engine/
eConstr.ml
90%
engine/
evarutil.ml
90%
engine/
evd.ml
93%
engine/
ftactic.ml
67%
engine/
logic_monad.ml
87%
engine/
namegen.ml
87%
engine/
nameops.ml
82%
engine/
proofview.ml
41%
engine/
proofview_monad.ml
76%
engine/
termops.ml
96%
engine/
uState.ml
80%
engine/
universes.ml
97%
engine/
univops.ml
56%
ide/
document.ml
52%
ide/
ide_slave.ml
0%
ide/
richpp.ml
52%
ide/
serialize.ml
58%
ide/
xml_lexer.ml
53%
ide/
xml_parser.ml
50%
ide/
xml_printer.ml
50%
ide/
xmlprotocol.ml
65%
interp/
constrexpr_ops.ml
83%
interp/
constrextern.ml
91%
interp/
constrintern.ml
96%
interp/
declare.ml
99%
interp/
discharge.ml
88%
interp/
dumpglob.ml
86%
interp/
genintern.ml
91%
interp/
impargs.ml
77%
interp/
implicit_quantifiers.ml
69%
interp/
modintern.ml
84%
interp/
notation.ml
82%
interp/
notation_ops.ml
88%
interp/
ppextend.ml
90%
interp/
reserve.ml
82%
interp/
smartlocate.ml
100%
interp/
stdarg.ml
82%
interp/
syntax_def.ml
100%
interp/
tactypes.ml
100%
interp/
topconstr.ml
100%
intf/
constrexpr.ml
100%
intf/
decl_kinds.ml
100%
intf/
evar_kinds.ml
100%
intf/
extend.ml
100%
intf/
genredexpr.ml
100%
intf/
glob_term.ml
100%
intf/
locus.ml
100%
intf/
misctypes.ml
100%
intf/
notation_term.ml
100%
intf/
pattern.ml
100%
intf/
vernacexpr.ml
89%
kernel/
cClosure.ml
61%
kernel/
cPrimitives.ml
58%
kernel/
cbytecodes.ml
93%
kernel/
cbytegen.ml
94%
kernel/
cemitcodes.ml
79%
kernel/
constr.ml
73%
kernel/
context.ml
86%
kernel/
conv_oracle.ml
93%
kernel/
cooking.ml
100%
kernel/
copcodes.ml
97%
kernel/
csymtable.ml
100%
kernel/
declarations.ml
88%
kernel/
declareops.ml
100%
kernel/
entries.ml
86%
kernel/
environ.ml
64%
kernel/
esubst.ml
100%
kernel/
evar.ml
95%
kernel/
indtypes.ml
91%
kernel/
inductive.ml
85%
kernel/
mod_subst.ml
92%
kernel/
mod_typing.ml
92%
kernel/
modops.ml
88%
kernel/
names.ml
86%
kernel/
nativecode.ml
4%
kernel/
nativeconv.ml
83%
kernel/
nativelambda.ml
79%
kernel/
nativelib.ml
72%
kernel/
nativelibrary.ml
26%
kernel/
nativevalues.ml
77%
kernel/
opaqueproof.ml
92%
kernel/
pre_env.ml
85%
kernel/
reduction.ml
78%
kernel/
retroknowledge.ml
92%
kernel/
safe_typing.ml
93%
kernel/
sorts.ml
90%
kernel/
subtyping.ml
73%
kernel/
term.ml
94%
kernel/
term_typing.ml
52%
kernel/
type_errors.ml
87%
kernel/
typeops.ml
89%
kernel/
uGraph.ml
11%
kernel/
uint31.ml
89%
kernel/
univ.ml
93%
kernel/
vars.ml
66%
kernel/
vconv.ml
65%
kernel/
vm.ml
73%
lib/
aux_file.ml
14%
lib/
backtrace.ml
84%
lib/
bigint.ml
83%
lib/
cArray.ml
62%
lib/
cAst.ml
97%
lib/
cEphemeron.ml
71%
lib/
cErrors.ml
90%
lib/
cList.ml
83%
lib/
cMap.ml
7%
lib/
cObj.ml
4%
lib/
cProfile.ml
0%
lib/
cSet.ml
41%
lib/
cStack.ml
94%
lib/
cString.ml
39%
lib/
cThread.ml
71%
lib/
cUnix.ml
94%
lib/
cWarnings.ml
33%
lib/
canary.ml
45%
lib/
control.ml
75%
lib/
coqProject_file.ml4
100%
lib/
dAst.ml
2%
lib/
deque.ml
63%
lib/
dyn.ml
62%
lib/
envars.ml
57%
lib/
exninfo.ml
68%
lib/
explore.ml
66%
lib/
feedback.ml
80%
lib/
flags.ml
70%
lib/
future.ml
75%
lib/
genarg.ml
67%
lib/
hMap.ml
64%
lib/
hashcons.ml
84%
lib/
hashset.ml
93%
lib/
heap.ml
100%
lib/
hook.ml
16%
lib/
iStream.ml
10%
lib/
int.ml
93%
lib/
loc.ml
70%
lib/
minisys.ml
78%
lib/
monad.ml
75%
lib/
option.ml
89%
lib/
pp.ml
56%
lib/
predicate.ml
92%
lib/
remoteCounter.ml
70%
lib/
rtree.ml
95%
lib/
segmenttree.ml
54%
lib/
spawn.ml
95%
lib/
stateid.ml
67%
lib/
store.ml
77%
lib/
system.ml
7%
lib/
terminal.ml
71%
lib/
trie.ml
74%
lib/
unicode.ml
100%
lib/
unicodetable.ml
91%
lib/
unionfind.ml
51%
lib/
util.ml
85%
library/
coqlib.ml
96%
library/
declaremods.ml
83%
library/
decls.ml
50%
library/
dischargedhypsmap.ml
95%
library/
global.ml
74%
library/
globnames.ml
83%
library/
goptions.ml
95%
library/
heads.ml
80%
library/
keys.ml
56%
library/
kindops.ml
89%
library/
lib.ml
78%
library/
libnames.ml
96%
library/
libobject.ml
85%
library/
library.ml
86%
library/
loadpath.ml
87%
library/
nametab.ml
89%
library/
states.ml
70%
library/
summary.ml
81%
parsing/
cLexer.ml4
85%
parsing/
egramcoq.ml
98%
parsing/
egramml.ml
91%
parsing/
g_constr.ml4
89%
parsing/
g_prim.ml4
94%
parsing/
g_proofs.ml4
95%
parsing/
g_vernac.ml4
88%
parsing/
pcoq.ml
52%
parsing/
tok.ml
67%
plugins/btauto/
g_btauto.ml4
16%
plugins/btauto/
refl_btauto.ml
89%
plugins/cc/
ccalgo.ml
90%
plugins/cc/
ccproof.ml
90%
plugins/cc/
cctac.ml
62%
plugins/cc/
g_congruence.ml4
0%
plugins/derive/
derive.ml
50%
plugins/derive/
g_derive.ml4
83%
plugins/extraction/
common.ml
76%
plugins/extraction/
extract_env.ml
94%
plugins/extraction/
extraction.ml
61%
plugins/extraction/
g_extraction.ml4
76%
plugins/extraction/
haskell.ml
4%
plugins/extraction/
json.ml
82%
plugins/extraction/
mlutil.ml
90%
plugins/extraction/
modutil.ml
91%
plugins/extraction/
ocaml.ml
78%
plugins/extraction/
scheme.ml
72%
plugins/extraction/
table.ml
96%
plugins/firstorder/
formula.ml
80%
plugins/firstorder/
g_ground.ml4
93%
plugins/firstorder/
ground.ml
96%
plugins/firstorder/
instances.ml
95%
plugins/firstorder/
rules.ml
83%
plugins/firstorder/
sequent.ml
97%
plugins/firstorder/
unify.ml
94%
plugins/fourier/
fourier.ml
96%
plugins/fourier/
fourierR.ml
100%
plugins/fourier/
g_fourier.ml4
88%
plugins/funind/
functional_principles_proofs.ml
77%
plugins/funind/
functional_principles_types.ml
44%
plugins/funind/
g_indfun.ml4
69%
plugins/funind/
glob_term_to_relation.ml
63%
plugins/funind/
glob_termops.ml
83%
plugins/funind/
indfun.ml
76%
plugins/funind/
indfun_common.ml
81%
plugins/funind/
invfun.ml
1%
plugins/funind/
merge.ml
84%
plugins/funind/
recdef.ml
85%
plugins/ltac/
coretactics.ml4
75%
plugins/ltac/
evar_tactics.ml
63%
plugins/ltac/
extraargs.ml4
61%
plugins/ltac/
extratactics.ml4
68%
plugins/ltac/
g_auto.ml4
52%
plugins/ltac/
g_class.ml4
100%
plugins/ltac/
g_eqdecide.ml4
87%
plugins/ltac/
g_ltac.ml4
69%
plugins/ltac/
g_obligations.ml4
61%
plugins/ltac/
g_rewrite.ml4
88%
plugins/ltac/
g_tactic.ml4
100%
plugins/ltac/
pltac.ml
67%
plugins/ltac/
pptactic.ml
93%
plugins/ltac/
profile_ltac.ml
55%
plugins/ltac/
profile_ltac_tactics.ml4
87%
plugins/ltac/
rewrite.ml
100%
plugins/ltac/
tacarg.ml
81%
plugins/ltac/
taccoerce.ml
85%
plugins/ltac/
tacentries.ml
89%
plugins/ltac/
tacenv.ml
93%
plugins/ltac/
tacintern.ml
91%
plugins/ltac/
tacinterp.ml
77%
plugins/ltac/
tacsubst.ml
37%
plugins/ltac/
tactic_debug.ml
99%
plugins/ltac/
tactic_matching.ml
88%
plugins/ltac/
tactic_option.ml
92%
plugins/ltac/
tauto.ml
74%
plugins/micromega/
certificate.ml
76%
plugins/micromega/
coq_micromega.ml
83%
plugins/micromega/
g_micromega.ml4
86%
plugins/micromega/
mfourier.ml
58%
plugins/micromega/
micromega.ml
52%
plugins/micromega/
mutils.ml
65%
plugins/micromega/
persistent_cache.ml
82%
plugins/micromega/
polynomial.ml
0%
plugins/micromega/
sos_types.ml
100%
plugins/nsatz/
g_nsatz.ml4
82%
plugins/nsatz/
ideal.ml
93%
plugins/nsatz/
nsatz.ml
59%
plugins/nsatz/
polynom.ml
5%
plugins/nsatz/
utile.ml
91%
plugins/omega/
coq_omega.ml
91%
plugins/omega/
g_omega.ml4
78%
plugins/omega/
omega.ml
100%
plugins/quote/
g_quote.ml4
84%
plugins/quote/
quote.ml
93%
plugins/romega/
const_omega.ml
92%
plugins/romega/
g_romega.ml4
79%
plugins/romega/
refl_omega.ml
100%
plugins/rtauto/
g_rtauto.ml4
73%
plugins/rtauto/
proof_search.ml
90%
plugins/rtauto/
refl_tauto.ml
58%
plugins/setoid_ring/
g_newring.ml4
87%
plugins/setoid_ring/
newring.ml
90%
plugins/ssr/
ssrbwd.ml
82%
plugins/ssr/
ssrcommon.ml
88%
plugins/ssr/
ssrelim.ml
80%
plugins/ssr/
ssrequality.ml
52%
plugins/ssr/
ssrfwd.ml
81%
plugins/ssr/
ssripats.ml
58%
plugins/ssr/
ssrparser.ml4
30%
plugins/ssr/
ssrprinters.ml
89%
plugins/ssr/
ssrtacticals.ml
25%
plugins/ssr/
ssrvernac.ml4
92%
plugins/ssr/
ssrview.ml
78%
plugins/ssrmatching/
ssrmatching.ml4
95%
plugins/syntax/
ascii_syntax.ml
87%
plugins/syntax/
int31_syntax.ml
97%
plugins/syntax/
nat_syntax.ml
93%
plugins/syntax/
r_syntax.ml
94%
plugins/syntax/
string_syntax.ml
94%
plugins/syntax/
z_syntax.ml
95%
pretyping/
arguments_renaming.ml
96%
pretyping/
cases.ml
89%
pretyping/
cbv.ml
88%
pretyping/
classops.ml
86%
pretyping/
coercion.ml
89%
pretyping/
constr_matching.ml
70%
pretyping/
detyping.ml
89%
pretyping/
evarconv.ml
92%
pretyping/
evardefine.ml
96%
pretyping/
evarsolve.ml
88%
pretyping/
find_subterm.ml
86%
pretyping/
geninterp.ml
58%
pretyping/
glob_ops.ml
92%
pretyping/
indrec.ml
79%
pretyping/
inductiveops.ml
89%
pretyping/
locusops.ml
100%
pretyping/
ltac_pretype.ml
59%
pretyping/
miscops.ml
68%
pretyping/
nativenorm.ml
59%
pretyping/
patternops.ml
79%
pretyping/
pretype_errors.ml
94%
pretyping/
pretyping.ml
98%
pretyping/
program.ml
93%
pretyping/
recordops.ml
84%
pretyping/
redops.ml
81%
pretyping/
reductionops.ml
80%
pretyping/
retyping.ml
90%
pretyping/
tacred.ml
89%
pretyping/
typeclasses.ml
50%
pretyping/
typeclasses_errors.ml
94%
pretyping/
typing.ml
90%
pretyping/
unification.ml
100%
pretyping/
univdecls.ml
94%
pretyping/
vnorm.ml
59%
printing/
genprint.ml
86%
printing/
ppconstr.ml
63%
printing/
pputils.ml
59%
printing/
ppvernac.ml
72%
printing/
prettyp.ml
73%
printing/
printer.ml
81%
printing/
printmod.ml
87%
proofs/
clenv.ml
93%
proofs/
clenvtac.ml
59%
proofs/
evar_refiner.ml
94%
proofs/
goal.ml
88%
proofs/
logic.ml
71%
proofs/
miscprint.ml
91%
proofs/
pfedit.ml
78%
proofs/
proof.ml
68%
proofs/
proof_bullet.ml
88%
proofs/
proof_global.ml
100%
proofs/
proof_type.ml
87%
proofs/
redexpr.ml
85%
proofs/
refine.ml
63%
proofs/
refiner.ml
75%
proofs/
tacmach.ml
78%
stm/
asyncTaskQueue.ml
12%
stm/
coqworkmgrApi.ml
86%
stm/
dag.ml
9%
stm/
proofBlockDelimiter.ml
100%
stm/
proofworkertop.ml
67%
stm/
queryworkertop.ml
79%
stm/
spawned.ml
66%
stm/
stm.ml
69%
stm/
tQueue.ml
100%
stm/
tacworkertop.ml
97%
stm/
vcs.ml
79%
stm/
vernac_classifier.ml
1%
stm/
vio_checking.ml
90%
stm/
workerLoop.ml
76%
stm/
workerPool.ml
85%
tactics/
auto.ml
93%
tactics/
autorewrite.ml
91%
tactics/
btermdn.ml
89%
tactics/
class_tactics.ml
96%
tactics/
contradiction.ml
89%
tactics/
dn.ml
82%
tactics/
dnet.ml
74%
tactics/
eauto.ml
93%
tactics/
elim.ml
79%
tactics/
elimschemes.ml
97%
tactics/
eqdecide.ml
94%
tactics/
eqschemes.ml
90%
tactics/
equality.ml
84%
tactics/
hints.ml
84%
tactics/
hipattern.ml
96%
tactics/
ind_tables.ml
84%
tactics/
inv.ml
77%
tactics/
leminv.ml
86%
tactics/
tacticals.ml
92%
tactics/
tactics.ml
70%
tactics/
term_dnet.ml
88%
tools/
coq_makefile.ml
16%
tools/
coqc.ml
20%
tools/
coqdep.ml
50%
tools/
coqdep_boot.ml
72%
tools/
coqdep_common.ml
53%
tools/
coqdep_lexer.ml
66%
tools/coqdoc/
alpha.ml
84%
tools/coqdoc/
cdglobals.ml
49%
tools/coqdoc/
cpretty.ml
87%
tools/coqdoc/
index.ml
36%
tools/coqdoc/
main.ml
61%
tools/coqdoc/
output.ml
81%
tools/coqdoc/
tokens.ml
49%
tools/
coqwc.ml
84%
tools/
fake_ide.ml
77%
tools/
ocamllibdep.ml
100%
tools/
tolink.ml
76%
toplevel/
coqinit.ml
47%
toplevel/
coqloop.ml
64%
toplevel/
coqtop.ml
100%
toplevel/
coqtop_bin.ml
73%
toplevel/
coqtop_byte_bin.ml
100%
toplevel/
coqtop_opt_bin.ml
100%
toplevel/
usage.ml
65%
toplevel/
vernac.ml
81%
vernac/
assumptions.ml
89%
vernac/
auto_ind_decl.ml
75%
vernac/
class.ml
95%
vernac/
classes.ml
96%
vernac/
command.ml
100%
vernac/
declareDef.ml
86%
vernac/
explainErr.ml
55%
vernac/
himsg.ml
86%
vernac/
indschemes.ml
88%
vernac/
lemmas.ml
89%
vernac/
locality.ml
89%
vernac/
metasyntax.ml
73%
vernac/
mltop.ml
87%
vernac/
obligations.ml
87%
vernac/
proof_using.ml
97%
vernac/
record.ml
72%
vernac/
search.ml
78%
vernac/
topfmt.ml
79%
vernac/
vernacentries.ml
46%
vernac/
vernacinterp.ml
47%
vernac/
vernacprop.ml
100%
vernac/
vernacstate.ml