coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵	emakarov	2010-09-06
\| \| \| \| \| \|	pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug #2375 (congruence)	corbinea	2010-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13399 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* removed declare_constant and declare_internal_constant	vsiles	2010-09-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(declare_constant_gen was not exported, leading to a lot of silly tests before calling those functions) and replaced them by declare_constant : ?internal:internal_flat -> ... declare_constant's default behaviour is the same as the old declare_constant. * fixed the default behaviour of inductive scheme failure during coq's compilation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
*	v13392 port from v8.3 to trunk : correct message when defining inductive schemes	vsiles	2010-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13394 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +	herbelin	2010-09-02
\| \| \| \| \| \|	backport of 13391 from 8.3 to trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13393 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved printing of Unfoldable constants in hints databases (used	herbelin	2010-09-02
\| \| \| \| \| \| \|	user-level pr_constant instead of debugging-level pr_con + used ppnl and boxes instead of explicit fnl's so as not to disturb formatting). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13390 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* By default, load proof terms.	regisgia	2010-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* scripts/Coqc toplevel/Usage:	regisgia	2010-08-27
\| \| \| \| \| \|	Export the -load-proofs officially. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* checker/Safe_typing.LightenLibrary:	regisgia	2010-08-27
\| \| \| \| \| \|	Remove the function "save" as the checker only needs to read vo files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* kernel/Safe_typing.LightenLibrary:	regisgia	2010-08-27
\| \| \| \| \| \|	Fix an incorrect initialization of the index counter. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13386 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
\| \| \| \| \| \| \|	Rename "lighten_" into "traverse_" inside the [traverse_library] function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13385 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
\| \| \| \| \| \| \|	Fix a bug in traverse_library. The extraction was not satisfied with [mod_expr] set to [None]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13384 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* toplevel/Coqtop: Reactivate -dont-load-proofs option.	regisgia	2010-08-27
\| \| \| \| \| \|	(This is simply the default behavior from now.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13383 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* library/Library: Reformulate a comment.	regisgia	2010-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13382 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* library/Library: Document.	regisgia	2010-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* checker/SafeTyping kernel/SafeTyping:	regisgia	2010-08-27
\| \| \| \| \| \|	Fix typos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13380 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia	2010-08-27
\| \| \| \| \| \| \| \| \| \| \|	proofs is now the default behavior of coqtop. * lib/Coqtop: Update accordingly. * checker/Check library/Library: Pass the right "load_proofs" flag to LightenLibrary.load. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* Improve documentation of LightenLibrary.	regisgia	2010-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13378 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* (checker\|kernel)/Safe_typing: New LightenLibrary.	regisgia	2010-08-27
\| \| \| \| \| \| \| \| \|	This module introduces an indirection behind opaque const_body to enable the optional demarshalling of them. * library/Library checker/Check: Use LightenLibrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13377 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* library/Library: Remove the use of the old-fashioned lighten_library.	regisgia	2010-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* library/Library: Remove lighten_library definition.	regisgia	2010-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13375 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix an error message ot having the ERror: prefix.	courtieu	2010-08-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13373 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export printing functions for extra arguments. Maybe there's a way to	msozeau	2010-08-03
\| \| \| \| \| \| \|	get them from the grammar entries? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13369 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix [clenv_missing] to compute a better approximation of missing	msozeau	2010-08-02
\| \| \| \| \| \| \| \| \| \|	dependent arguments. It breaks compatibility as some [apply with] clauses are not necessary anymore. Typically when applying [f_equal], the domain type of the function can be infered even if it does not appear directly in the conclusion of the goal. Fixes bug #2154. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed commit r13359 which was incomplete for its "trunk" part. Thanks	herbelin	2010-07-31
\| \| \| \| \| \|	to Julien for noticing it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13366 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adpated the checker to handle coomutative cuts and lazyness	barras	2010-07-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed information in COMPATIBILITY that were intended before all for	herbelin	2010-07-30
\| \| \| \| \| \|	developers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13364 85f007b7-540e-0410-9357-904b9bb8a0f7
*	better fix to bug #2319: types are compiled in the env of the bodies	barras	2010-07-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated test on Nsatz after Loïc moved NsatzR to Nsatz.	herbelin	2010-07-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13361 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Capitulation wrt "change pat with term": instead of solving the	herbelin	2010-07-30
\| \| \| \| \| \| \| \| \| \| \|	problem raised by taral on coq-club Goal forall X : Prop, X -> False -> False. intro. change (?t -> False) with (not t). we just fail with an error message of "mauvaise foi". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13360 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r13359 continued: removed native treatment for λ (lambda) and Π (Pi)	herbelin	2010-07-30
\| \| \| \| \| \| \| \| \| \| \|	what frees the tokens for other uses in non-unicode mode. For Π, users will have to introduce their own recursive notation. For λ, this is provided by the -unicode option (which actually is not documented nor as an option nor in the reference manual; maybe it should simply be now removed since "Require Import Utf8_core" has the same effect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13359 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rather quick hack to make basic unicode notations available by	herbelin	2010-07-29
\| \| \| \| \| \|	requiring a file Utf8_core. That needs to be improved... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin	2010-07-29
\| \| \| \| \| \|	with non-recursive binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13357 85f007b7-540e-0410-9357-904b9bb8a0f7
*	kernel conversion and reduction do not raise assert failure on ill-typed ↵	barras	2010-07-29
\| \| \| \| \| \|	terms, but an anomaly instead. It is caught in pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13353 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test-case for bug #2105	barras	2010-07-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13352 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵	barras	2010-07-29
\| \| \| \| \| \|	predicate in branch read-back (2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13350 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵	barras	2010-07-29
\| \| \| \| \| \|	predicate in branch read-back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13349 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2209, don't use the fragile argument name "y" to pass the	msozeau	2010-07-28
\| \| \| \| \| \| \|	missing argument to a transitivity call. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13347 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rewrite Heap merging so that it extracts to an O(n log n) definition.	msozeau	2010-07-28
\| \| \| \| \| \| \|	Fixes bug #2047. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13345 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oops. commited files I shouldn't have. reverting on r13341	barras	2010-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13342 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ported r13340 to trunk	barras	2010-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13341 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 ↵	pottier	2010-07-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies	barras	2010-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nstaz pour les anneaux integres et les setoides, R Z et Q	pottier	2010-07-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13336 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix computation of fix annotation index: only consider assumptions and	msozeau	2010-07-27
\| \| \| \| \| \| \|	not let-ins in the binding list. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13335 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes:	msozeau	2010-07-27
\| \| \| \| \| \| \| \| \|	- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Set Automatic Coercions Import.	herbelin	2010-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix installation of emacs files	glondu	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13325 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7