coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-09-15	[micromega] Use `minus_one` built-in zarith constant.	Emilio Jesus Gallego Arias

2020-09-14	[ocamlformat] Update to ocamlformat 0.15.0	Emilio Jesus Gallego Arias
	This is necessary to support OCaml 4.11 in development.
2020-03-04	[micromega] Add numerical compatibility layer.	Emilio Jesus Gallego Arias
	Only significant change is in gcd / lcm which now are typed in `Z.t`
2019-12-13	[micromega] Enable ocamlformat.	Emilio Jesus Gallego Arias

2018-10-16	[micromega] remove dead code	Vincent Laporte

2018-06-07	Micromega clean-up	Maxime Dénès
	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.
2017-04-27	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

2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey

2014-09-25	Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",	Xavier Clerc
	as "\|\|" is actually redefined in "plugins/micromega/sos_lib.ml".
2014-09-25	Remove some 'deprecated' warnings.	Xavier Clerc

2013-12-03	Silence compilation warning by avoiding some deprecated constructs.	Guillaume Melquiond

2013-10-24	Oups, repair the compilation (micromega + Morphism_prop)	letouzey
	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
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-16	Reintroduce "or" instead of "\|\|" as the latter is redifined in "sos_lib.ml" ↵	xclerc
	with a different semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16888 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-28	Cleaning opening of the standard List module.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15500 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu
	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
2010-04-11	Remove unused functions run_sdpa	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08	Sos.ml: no more warnings	letouzey
	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
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-25	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵	fbesson
	85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-20	new csdp cache + improved error message	fbesson
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-31	addition of lia.cache - csdp.cache is now handled by micromega not csdpcert	fbesson
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30	micromega : Better parsing of formulae - smaller proof terms for Z - ↵	fbesson
	redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7