coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Micromega clean-up	Maxime Dénès	2018-06-07
\| \| \| \| \| \| \| \| \|	We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
*	Micromega: do not use Filename.temp_dir_path, remove unused values	Gaetan Gilbert	2017-04-27
\|
*	Rename Sos_lib.(\|\|) -> parser_or to avoid (deprecated) Pervasives.or	Gaetan Gilbert	2017-04-27
\|
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
\|
*	Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",	Xavier Clerc	2014-09-25
\| \| \| \|	as "\|\|" is actually redefined in "plugins/micromega/sos_lib.ml".
*	Remove some 'deprecated' warnings.	Xavier Clerc	2014-09-25
\|
*	Silence compilation warning by avoiding some deprecated constructs.	Guillaume Melquiond	2013-12-03
\|
*	Oups, repair the compilation (micromega + Morphism_prop)	letouzey	2013-10-24
\| \| \| \| \| \| \| \| \| \| \| \| \|	It seems I forgot to fully recompile after my last bunch of syntactic changes about List.assoc_f, that weren't so syntactic after all, sorry : - Util isn't used in micromega, hence no List.assoc_f there - There is something wrong in my modifications of Notation_ops that breaks the compilation of Morphism_prop. For the moment I don't see what, so I revert all the modifications of this file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16930 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reintroduce "or" instead of "\|\|" as the latter is redifined in "sos_lib.ml" ↵	xclerc	2013-10-16
\| \| \| \| \| \|	with a different semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc	2013-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
\| \| \| \| \| \|	See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove unused functions run_sdpa	glondu	2010-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Sos.ml: no more warnings	letouzey	2009-12-08
\| \| \| \| \| \| \| \| \|	apart for a few non-exhaustive patterns, there was also some unused let-in variables. Hard to check whether the apparently useless code is doing some side-effect or not... It seems not, so I've removed completely the corresponding code. Frederic, is that ok ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12570 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
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵	fbesson	2009-08-25
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	new csdp cache + improved error message	fbesson	2009-08-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
*	addition of lia.cache - csdp.cache is now handled by micromega not csdpcert	fbesson	2009-07-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
*	micromega : Better parsing of formulae - smaller proof terms for Z - ↵	fbesson	2009-07-30
\| \| \| \| \| \|	redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7