coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵	xclerc	2013-09-19
\| \| \| \| \| \|	with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
\| \| \| \| \| \| \| \| \| \| \| \|	casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing the last global evar generation in Term_dnet. The very	ppedrot	2013-09-18
\| \| \| \| \| \| \|	fact that the previous implementation was working is still black magic to me, as evars may have collided in intriguing ways... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing unused code from Term_dnet.	ppedrot	2013-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot	2013-09-18
\| \| \| \| \| \| \|	Ultimately all evars should be created with respect to a given evar map, instead of using a global counter. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Taming the simpl evar hack that used to use negative evars.	ppedrot	2013-09-18
\| \| \| \| \| \| \| \|	Now we just generate evars in the given evar map. At least, the test-suite isn't broken... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16782 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Slightly more compact representation of 'a substituted type,	ppedrot	2013-09-14
\| \| \| \| \| \|	removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
*	When Coq is reset-initialed by CoqIDE, do reset jobs counters	gareuselesinge	2013-09-13
\| \| \| \| \| \| \|	Coq is not going to send any feedback message for the brute-force canceled jobs, given that the process was killed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16780 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix error reporting window size calculation	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: new async error reporting window and slaves status	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	STM pretty printer should never fail	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix STM feeback on running jobs	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16776 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Do no compage wg_Notebook terms with (=)	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16775 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Unplugging Autoinstance. The code is still here if someone wishes	ppedrot	2013-09-12
\| \| \| \| \| \|	to fix it, but it should be eventually erased. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: show number of proofs being checked in background	gareuselesinge	2013-09-12
\| \| \| \| \| \|	good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minimal implementation of `Shallow marshalling of Lib	gareuselesinge	2013-09-12
\| \| \| \| \| \|	Just sufficient to make abstract work in such an (empty) lib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Unknown commands starting a proof were not setting the proof mode.	gareuselesinge	2013-09-12
\| \| \| \| \| \|	Fixes Orsay/Containers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove outdated comment	gareuselesinge	2013-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16770 85f007b7-540e-0410-9357-904b9bb8a0f7
*	VernacList handling was lost in STM merge	gareuselesinge	2013-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug in CStack introduced by refactoring	gareuselesinge	2013-09-12
\| \| \| \| \| \|	Refactorings should be tested, right? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Temporary fix of emacs mode for ProofGeneral	letouzey	2013-09-10
\| \| \| \| \| \| \| \| \| \|	To the best of my knowledge, even with the latest cvs version of PG: - the goals must be finally displayed at each step - the <info>...</info> async feedback messages aren't handled yet. I'll check with Enrico what he intended with these two lines, but meanwhile let's comment them... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Change syntax of Hint Resolve to actually accept user-given priorities.	msozeau	2013-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16766 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
\| \| \| \| \| \|	of a [fold] in [nf_*] normalizing functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16764 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Evd.	ppedrot	2013-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16763 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.	ppedrot	2013-09-05
\| \| \| \| \| \| \|	They did not really enhance the safety of the code, as several outer parts acceeded directly to the internal representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More robust argument setter in CoqIDE. It does not crash anymore on bad	ppedrot	2013-09-04
\| \| \| \| \| \|	arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
\| \| \| \| \| \| \|	unsatisfactory as some functions implicitly require some ordering on the evars, but this is already better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some cleanup in Auto	ppedrot	2013-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* test-suite/success/Unicode_utf8:	regisgia	2013-09-02
\| \| \| \| \| \|	Regression test for bug #3020. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* lib/Unicode:	regisgia	2013-09-02
\| \| \| \| \| \| \|	Workaround. Some characters seems to be missing in Camomile's category tables. We add them manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* parsing/Lexer: Cosmetics.	regisgia	2013-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* configure: Remove trailing space.	regisgia	2013-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16753 85f007b7-540e-0410-9357-904b9bb8a0f7
*	summary for ML modules made correct	gareuselesinge	2013-08-30
\| \| \| \| \| \| \| \| \|	This summary entry is special because its unfreeze may load ML code that in turns adds summary entries. Hence it is the first summary piece to be unfreezed, otherwise some summaries may get lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make the jopin-document button wait for slaves to terminate	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing the code of field_simplify_eq.	amahboub	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16749 85f007b7-540e-0410-9357-904b9bb8a0f7
*	When PG is used as interface behave as before STM	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16748 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ind_tables: properly handling side effects	gareuselesinge	2013-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	If a constant is defined as transparent, not only its side effects (opaque sub proofs as in abstract, and transparent ind schemes) are declared globally, but the ones that are schemes are also declared as such. The only sub optimal thing is that the code handling in a special way the side effects of transparent constants is in declare.ml that does not see ind_tables.ml, hence a forward ref to a function is used. IMO, ind_tables has no reason to stay in toplevel/. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
*	recdef: restore old semantics (pre STM)	gareuselesinge	2013-08-30
\| \| \| \| \| \| \| \|	The Stm commit switched from an home made handling of failures to a with_state_protection. This was wrong, since in case of success the global state has to be left altered. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo in error message	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	safe Conv_oracle state for type checking	gareuselesinge	2013-08-30
\| \| \| \| \| \| \|	safe_typing is not purely functional, hence we cannot chain it as if it was a pure computation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stm: if slave process dies badly go back to local lazy evaluation	gareuselesinge	2013-08-30
\| \| \| \| \| \| \| \| \| \| \|	Processing the proof in a slave process may fail for an implementation error, e.g. the state could not be marshalled, or an anomaly is raised by the slave. In this case we fall back to local, lazy, evaluation in the master process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16743 85f007b7-540e-0410-9357-904b9bb8a0f7
*	-coq-slaves: close_on_exec + correct argument passing	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16742 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove Obj.magic from safe typing	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16741 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Trickyer test for Paral-ITP	gareuselesinge	2013-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #3083.	ppedrot	2013-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing some lone List.assoc & List.mem in lib.	ppedrot	2013-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7