Collapse file tree

Files

 trunk

Search this repository

/

checker

/

Copy path

Directory actions

More options

More options

Directory actions

More options

More options

Latest commit

letouzey

Merge branch 'v8.5' into trunk

Apr 9, 2015

429f493 · Apr 9, 2015

History

History

Open commit details

This branch is 28986 commits behind rocq-prover/rocq:master.

/

checker

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
.depend		.depend	fixed bug with aliases	May 7, 2008
Makefile		Makefile	fixed bug with aliases	May 7, 2008
check.ml		check.ml	Windows: open .vo files in binary mode	Feb 5, 2015
check.mllib		check.mllib	Using same code for browsing physical directories in coqtop and coqdep.	Feb 16, 2015
check_stat.ml		check_stat.ml	Update headers.	Jan 12, 2015
check_stat.mli		check_stat.mli	Update headers.	Jan 12, 2015
checker.ml		checker.ml	Removing references to deprecated syntax -I/-R -as.	Mar 31, 2015
cic.mli		cic.mli	Fix checker after addition of a universe context in with t := c const…	Feb 26, 2015
closure.ml		closure.ml	Update headers.	Jan 12, 2015
closure.mli		closure.mli	Update headers.	Jan 12, 2015
declarations.ml		declarations.ml	Fix checker after addition of a universe context in with t := c const…	Feb 26, 2015
declarations.mli		declarations.mli	checker and votour ported to new vo format (after -vi2vo)	Feb 26, 2014
environ.ml		environ.ml	Fix checker treatment of inductives using subst_instances instead of …	Sep 5, 2014
environ.mli		environ.mli	Adapt the checker to polymorphic universes and projections (untested).	May 8, 2014
include		include	updated include file for debugging	Jan 6, 2015
indtypes.ml		indtypes.ml	Now accepting unit props in mutual definitions	Mar 2, 2015
indtypes.mli		indtypes.mli	Update headers.	Jan 12, 2015
inductive.ml		inductive.ml	Update headers.	Jan 12, 2015
inductive.mli		inductive.mli	Update headers.	Jan 12, 2015
main.ml		main.ml	added the .vo checker (with independent Makefile)	Apr 21, 2008
mod_checking.ml		mod_checking.ml	Declarations.mli refactoring: module_type_body = module_body	Jan 11, 2015
mod_checking.mli		mod_checking.mli	Update headers.	Jan 12, 2015
modops.ml		modops.ml	Update headers.	Jan 12, 2015
modops.mli		modops.mli	Update headers.	Jan 12, 2015
print.ml		print.ml	Update headers.	Jan 12, 2015
reduction.ml		reduction.ml	coqchk: more prints when -debug	Mar 23, 2015
reduction.mli		reduction.mli	Update headers.	Jan 12, 2015
safe_typing.ml		safe_typing.ml	coqchk: more prints when -debug	Mar 23, 2015
safe_typing.mli		safe_typing.mli	Update headers.	Jan 12, 2015
subtyping.ml		subtyping.ml	Update headers.	Jan 12, 2015
subtyping.mli		subtyping.mli	Update headers.	Jan 12, 2015
term.ml		term.ml	Update headers.	Jan 12, 2015
term.mli		term.mli	Remove unused substitution functions in checker.	Sep 5, 2014
type_errors.ml		type_errors.ml	Update headers.	Jan 12, 2015
type_errors.mli		type_errors.mli	Update headers.	Jan 12, 2015
typeops.ml		typeops.ml	Update headers.	Jan 12, 2015
typeops.mli		typeops.mli	Update headers.	Jan 12, 2015
univ.ml		univ.ml	Fixing bug rocq-prover#4019, and checker blow-up at once.	Feb 11, 2015
univ.mli		univ.mli	Update headers.	Jan 12, 2015
validate.ml		validate.ml	Update headers.	Jan 12, 2015
values.ml		values.ml	Exporting memory representation of STM tasks for votour.	Mar 25, 2015
votour.ml		votour.ml	Exporting memory representation of STM tasks for votour.	Mar 25, 2015
View all files