coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	coq_micromega.ml: fix order of recursive calls to rconstant	glondu	2012-01-14
\| \| \| \| \| \| \| \|	Some tests were failing on architectures without native code because the evaluation order of arguments in a function call is not the same on bytecode, leading to different behaviours for the psatzl tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14904 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add distclean back to test-suite/Makefile	glondu	2012-01-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More newlines in debugging output of psatzl	glondu	2012-01-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14902 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
*	Added the decidability of (<=) on nat.	ppedrot	2012-01-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14896 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo	glondu	2012-01-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix printing of instances, generalized arguments.	msozeau	2012-01-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo	glondu	2012-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed the itarget of the previous commit...	ppedrot	2012-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a typeclass-based system to reason on decidable propositions.	ppedrot	2012-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14887 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forbids (as it has always been the behaviour) to have two different open	aspiwack	2012-01-06
\| \| \| \| \| \|	proofs with the same name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes bug #2654 (tactic instantiate failing to update existential variables).	aspiwack	2012-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14883 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin	2012-01-05
\| \| \| \| \| \| \|	useful in the presence of coercions to Funclass. Fixed the bug differently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing Arguments Scope bug when too many scopes are given (bug #2667).	herbelin	2012-01-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Type inference unification: fixed a 8.4 bug in the presence of unification	herbelin	2012-01-04
\| \| \| \| \| \|	with evars under binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile.doc: attempt to solve race condition for creating doc/refman/html.	herbelin	2012-01-03
\| \| \| \| \| \| \| \| \|	Indeed, $INDEXURLS requires files from $INDEXES to be built and all of these files plus target doc/refman/html/index.html ask in parallel to erase and rebuild the doc/refman/html. Tried to use an intermediate phony target to factorize the rebuilding of doc/refman/html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14872 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2669 and more: make full-stdlib	pboutill	2011-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14869 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqdoc: Fixing missing newline when using "Proof term."	herbelin	2011-12-26
\| \| \| \| \| \| \|	(bug apparently introduced by r11880). Fixing also a "body_bol" which apparently should be a "bol". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14866 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin	2011-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
*	update CHANGES w.r.t. simpl	gareuselesinge	2011-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Version number, copyright, credits: missing updates.	herbelin	2011-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4: More exhaustive list of external contributors.	herbelin	2011-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	myocamlbuild: -DWIN32 instead of -DWin32	letouzey	2011-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14849 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Configure: the backslashes in win32 paths should be escaped	letouzey	2011-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14848 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4 + resetting COMPATIBILITY file.	herbelin	2011-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sequel of previous commit	letouzey	2011-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Isolate a few types of Goptions in a pure .mli, solving a dep issue with ↵	letouzey	2011-12-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	ocamlbuild A few types of Goptions are mentioned in toplevel/interface.mli. Since the latter is a pure .mli, this shouldn't trigger a dependency with respect to goptions.ml, but apparently ocamlbuild isn't clever enough to notice this, and hence wants to link a pile of useless stuff with coqide. I'll discuss with Pierre-Marie about the best long-term way to avoid this mess, but in the meantime I split the concerned types of Goptions in a separate Goptionstyp.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14841 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pure interfaces shouldn't be mentionned in .mllib	letouzey	2011-12-21
\| \| \| \| \| \| \| \| \| \| \|	.mllib should only mention code to be linked in .cma and later executable, but not .mli without .ml. Otherwise, really nasty errors occur with ocamlbuild, for instance some rules appears to be ignored and masked by default ones, etc etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14840 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adapt myocamlbuild after changes in coqdep_boot (.beautify)	letouzey	2011-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14839 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning CHANGES file.	herbelin	2011-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notifying removal of accidental unfolding of recursive calls of	herbelin	2011-12-19
\| \| \| \| \| \|	fixpoints by destruct/inversion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14828 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Arguments: check rename even if no implicit is specified	gareuselesinge	2011-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test suite update after r14808	pboutill	2011-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2377 part 2: old revision file is erased by install	pboutill	2011-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed some printing details for dependent evars in emacs mode. Patch	courtieu	2011-12-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	from Hendrik Tews: 1) Print the dependent evars after "No more subgoals" and after "No more subgoals but non-instantiated existential". This is necessary to correctly display the instantiation status of dependent evars, because the last proof command might change them. 2) Change the ``Show Goal "id"'' command to include a header like goal / evar 2 is: This is more consistent with the other Show commands. Moreover it simplifies the use of this command in Proof General, because, with the change, the output contains the goal ID. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin	2011-12-18
\| \| \| \| \| \| \|	unfolded fixpoints when calling destruct). However, this might break compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIde files position is freedesktop compliant.	pboutill	2011-12-18
\| \| \| \| \| \| \|	Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
*	./configure & freedesktop	pboutill	2011-12-18
\| \| \| \| \| \| \| \|	1/ man dir is now prefix/share/man and not prefix/man git diff! 2/ a data dir option for coqide extra data. 3/ typo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2634 (unscoped notations were disturbing the	herbelin	2011-12-18
\| \| \| \| \| \|	interpretation order of scoped notations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Applied patches proposed suggested by Hendrik Tews to fix existential	courtieu	2011-12-18
\| \| \| \| \| \| \| \|	variables printing in emacs mode (put them at the end of input, and fix commas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14818 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Continuing 14812 and 14813 (use type information to reduce the	herbelin	2011-12-18
\| \| \| \| \| \| \| \| \| \|	applicability of first-order unification in tactic unification). Don't try to unify the type (this would require a unification power that unification.ml does not have - and some contribs complain about that). Just reject first-order unification of metavariables of higher-order types when their types are obviously incompatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14817 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
\| \| \| \| \| \| \| \| \|	arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing PrintConstr debugging entry in g_proof.ml4 which was not	herbelin	2011-12-18
\| \| \| \| \| \| \|	working and was causing a warning when declaring the entry of same name in top_printers.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suspending declaration of undefined debug printers.	herbelin	2011-12-18
\| \| \| \| \| \|	(Matthieu, do you have a definition for these printers around?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14814 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
\| \| \| \| \| \| \|	meta in the tactic unification algorithm ("auto" becomes much slower if it takes into account the type of metas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14813 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17
\| \| \| \| \| \| \| \| \| \|	instantiating them in the unification algorithm used for tactics. This allows to discard ill-typed uses of first-order unification which otherwise would have been fatal (this incidentally allows to partially restore some compatibility with 8.3 that was broken after eta was added in unification). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reorganizing Unification.unify_0 so as to more easily share code	herbelin	2011-12-17
\| \| \| \| \| \|	between branches. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14811 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: "beautify" target	pboutill	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14809 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqdep adds %.v.beautified on the left of the ':' when it generates %.v ↵	pboutill	2011-12-17
\| \| \| \| \| \|	dependecies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14808 85f007b7-540e-0410-9357-904b9bb8a0f7