coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[ltac] Remove unused functions / constructors.	Emilio Jesus Gallego Arias	2018-07-14
\| \| \| \|	Catched by compiling the ml files from ml4.
*	Unify pre_env and env	Maxime Dénès	2018-05-28
\| \| \| \| \|	We now have only two notions of environments in the kernel: env and safe_env.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	New IR in VM: Clambda.	Maxime Dénès	2018-02-23
\| \| \| \| \| \| \| \| \| \| \| \|	This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Fix segfault in native compiler on int31 division.	Maxime Dénès	2014-10-10
\| \| \| \|	Thanks to Yves for reporting it!
*	Make the retroknowledge marshalable.	Arnaud Spiwack	2014-09-24
\| \| \| \| \| \|	Essential for parallel processing of Coq documents. It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
*	Machine arithmetic operations for native compiler.	Maxime Dénès	2014-04-09
\| \| \| \| \|	This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
*	Full support for int31 values in native compiler.	Maxime Dénès	2014-04-09
\|
*	Partial support for open terms in int31.	Maxime Dénès	2014-04-09
\|
*	Had to split Nativelambda in two files because of Retroknowledge	Maxime Dénès	2014-04-09
\| \| \| \|	dependencies.
*	Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had	Pierre-Marie Pédrot	2014-03-14
\| \| \| \|	no particular purpose.
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey	2012-08-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
\| \| \| \| \| \|	Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
\| \| \| \| \| \| \| \|	pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de head0 et tail0 en natif	bgregoir	2007-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
	details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7