coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech	2008-12-06
\| \| \| \| \| \| \| \| \|	unused methods object. Matthieu please review this change (after monday), I might have introduced a bug in rebuild_instance. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Do not catch _all_ exceptions in setoid unification.	msozeau	2008-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11658 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct handling of defined methods (let-ins) in instance declarations.	msozeau	2008-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lasson	msozeau	2008-12-04
\| \| \| \| \| \| \|	for the report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11656 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes for unification and substitution of metas under binders.	msozeau	2008-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	improved simpl	barras	2008-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add new directory for pre-compilation of files needed for further tests.	herbelin	2008-12-02
\| \| \| \| \| \| \|	Application to the test of notation import from within a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
\| \| \| \| \| \| \| \| \| \| \|	- Fixed a virtual bug of unification (ever occurs if w_unify called with a non-empty context of rel's, which is a priori uncommon). - Fixed Notation.out test. - Add better coqide error message in case editor is called on an unnamed file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	another bug with simpl	barras	2008-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inductive parameters: nicer doc examples and error message	letouzey	2008-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test case for previous commit.	msozeau	2008-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix (?) a pattern matching compilation problem:	msozeau	2008-11-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	<< Axiom A : nat -> bool. Definition foo := match A 0 with \| true => true \| k => k end. Print foo. >> [A 0] is duplicated in the [k => k] branch! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11640 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed non-exhaustive pattern matching	barras	2008-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug 1791: simpl was performing eta expansion	barras	2008-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added tests for hyps reordering	barras	2008-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixing problem with CompCert: reordering resulting from tac change was not ↵	barras	2008-11-27
\| \| \| \| \| \|	closed w.r.t. dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bug 1997.	soubiran	2008-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eventually fixing r11612	barras	2008-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11626 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration mineur du comportement de Function	jforest	2008-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
*	first attempt to allow Function to deal with dependent pattern matching. ↵	jforest	2008-11-23
\| \| \| \| \| \|	This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin	2008-11-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin	2008-11-23
\| \| \| \| \| \| \|	(if ever necessary). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor improvement to commit 11619	herbelin	2008-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
\| \| \| \| \| \| \| \|	slight improving of the printing of record. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
\| \| \| \| \| \| \| \| \| \|	revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed problem with r11612	barras	2008-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction of bug #2002	jforest	2008-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add implicit rules for native plugins (.cmxs)	glondu	2008-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11607 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Execute #rectypes directive in embedded OCaml toplevel...	glondu	2008-11-19
\| \| \| \| \| \| \|	...to avoid the need to have cflags.cmi around. This directive will likely be available in the next version of OCaml. See OCaml bug #4460. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo in omega doc	glondu	2008-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	integrate suggestions by B. Baydemir (see #1930)	letouzey	2008-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11600 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey	2008-11-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11595 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct display of constraints for Print Universes "dumpfile"	letouzey	2008-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11593 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration du README.doc et de l'installation de la doc	notin	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restores behaviour of v8.1 for unification problems which fail (backport of ↵	letouzey	2008-11-14
\| \| \| \| \| \|	11585) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11590 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Faster comparison of universes	letouzey	2008-11-14
\| \| \| \| \| \| \| \| \|	- compare the integer indexes first, in order to avoid comparing the dirpath part if possible - use an ad-hoc comparison function rather than Pervasives.compare (slightly faster during my tests on the compcert contrib) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make doc ne compilait plus la doc de stdlib (bug #1996)	notin	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11588 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add missing test-suite files for closed bugs.	msozeau	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11587 85f007b7-540e-0410-9357-904b9bb8a0f7
*	retour sur le commit 11579 qui faisait plante les contribs FSet et color.	soubiran	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative d'amélioration de la robustesse des Makefile générés par	notin	2008-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 ↵	barras	2008-11-13
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1995	notin	2008-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Les signatures des applications de foncteur sont précalculées, cela ↵	soubiran	2008-11-12
\| \| \| \| \| \| \| \| \|	alourdit un peu les vo mais accélère la compilation lorsque les foncteurs sont massivement utilisés. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11579 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)	letouzey	2008-11-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau	2008-11-10
\| \| \| \| \| \| \|	the three cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 85f007b7-540e-0410-9357-904b9bb8a0f7