coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Derive -> derive occurences	Pierre Boutillier	2015-01-12
\|
*	Removing the XML plugin.	Pierre-Marie Pédrot	2014-09-08
\| \| \| \| \|	Left a README, just in case someone will discover the remnants of it decades from now.
*	Derive plugin.	Arnaud Spiwack	2013-12-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	A small plugin to support program deriving (à la Richard Bird) in Coq. It's fairly simple: Require Coq.Derive.Derive. Derive f From g Upto eq As h. Produces a goal (actually two, but the first one is automatically shelved): \|- eq g ?42 And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).
*	Remove the Dp plugin.	gmelquio	2012-04-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Why2 has not been maintained for the last few years and the Why3 plugin should be a suitable replacement in most cases. Removed tactics: simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy. Removed commands: Dp_hint, Dp_timeout, Dp_prelude, Dp_predefined, Dp_debug, Dp_trace. Note that the "admit" tactic was actually provided by the Dp plugin. It has been moved to extratactics.ml4. Ported from v8.4 r15186. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a Btauto plugin, that solves boolean tautologies.	ppedrot	2012-01-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "syntax for exponents"	glondu	2011-02-25
\| \| \| \| \| \| \| \|	This reverts pottier's commit r13849. It references a ncring_plugin.cma for which there is no rule. I guess he forgot to commit something... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntax for exponents	pottier	2011-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7
*	plugin groebner updated and renamed as nsatz; first version of the doc of ↵	pottier	2010-06-03
\| \| \| \| \| \|	nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Misc small fixes : warning, dep cycles, ocamlbuild...	letouzey	2010-04-26
\| \| \| \| \| \| \| \| \| \| \| \|	- git ignore g_decl_mode.ml - exhaustive match for pp_vernac (BeginSubproof, ...) - for ocamlbuild, remove a spurious cycle in recordops.mli (unnecessary open of Classops), and fixes of *.itargets and _tags The compilation via ocamlbuild still need some work, since plugin firstorder now depends on the new plugin decl_mode git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Win32 cross-compilation from debian: build of coqide.exe and other binaries	letouzey	2010-02-24
	Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org to build some (unofficial) mingw32-liblablgtk2 debian packages. Then ./configure -local && ./build win32 is enough to get all native win32 binaries and plugin cmxs from a confortable linux box. Next step: an auto-installer :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7