coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	patch for C code of addmuldiv31	thery	2008-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo	letouzey	2008-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10592 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New instance returns the (future) identifier of the instance.	msozeau	2008-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10590 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
\| \| \| \| \| \| \| \| \| \|	(Axiom/Variable...). New tactic clapply to apply unapplied class methods in tactic mode, simple solution to the fact that apply does not work up-to classes yet. Add Functions.v for class definitions related to functional morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: variables	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: dépendances + génération des fichiers html	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10585 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de coqdoc : les commentaires simples généraient des lignes vides	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10584 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de Coqdoc (indentation des lignes)	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgotten file in previous commit	lmamane	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10581 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Merge with lmamane's private branch:	lmamane	2008-02-22
\| \| \| \| \| \| \| \| \| \|	- New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	congruence now knows about _ -> _	corbinea	2008-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10579 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petits oublis dans Makefile.doc	notin	2008-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10578 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added products and sorts as possible heads for canonical structures	corbinea	2008-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed pp for declarative mode	corbinea	2008-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10576 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite correction suite à la révision 10571	notin	2008-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de caractères unicode reconnus apr le lexer	notin	2008-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Patch bug #1799	soubiran	2008-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10573 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression d'un include et de 2 variables inutiles	notin	2008-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10572 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suspension de l'introduction de delta dans apply : certaines contribs	herbelin	2008-02-14
\| \| \| \| \| \| \| \| \| \| \|	qui utilisent apply pour l'automatisation explosent (cf CatsInZFC qui passe de 20mn de compilation à 7h), d'autres instancient les métas par des expressions plus dépliées qu'avant, ce qui conduit à des échecs après coup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plongement de doc/Makefile dans la nouvelle architecutre des Makefile	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de Coqdoc avec l'option -R	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some bad emacs messup that was commited...	msozeau	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reconnaissance des tokens dans les notations (suite à la revision r10562)	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added default canonical structures (see example in test-suite)	corbinea	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14
\| \| \| \| \| \| \| \| \| \| \|	class_tactics for further customizations. Add Equivalence.v for typeclass definitions on equivalences and clrewrite.v test-suite for clrewrite. Debugging the tactic I found missing morphisms that are now in Morphisms.v and removed some that made proof search fail or take too long, not sure it's complete however. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10565 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move class_setoid to class_tactics.	msozeau	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10564 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debugging of the class_setoid tactic and eauto. Prepare for move from	msozeau	2008-02-13
\| \| \| \| \| \| \|	class_setoid to class_tactics... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1512	notin	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implement KEEP_ML4_PREPROCESSED option in build system	lmamane	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implement NO_RECALC_DEPS option in build system	lmamane	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'option -glob-from de Coqdoc: les globalisations sont	notin	2008-02-13
\| \| \| \| \| \| \| \|	lues directement des fichiers .glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin	2008-02-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place d'une option "modulo_conv" pour contrôler l'usage de cette delta. - Pour éviter que rewrite ne réussise trop souvent, la delta est désactivée pour les tactiques d'élimination (une étude fine reste à faire). - On n'utilise aussi delta que sur les sous-termes du problème d'unification initial. C'est une heuristique qui est intuitive mais qui reste à être évaluée. - Au bilan, le surcoût en temps de compilation des theories est d'un peu moins d'1%. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de ce qui semble être un petit bug dans la gestion de la	herbelin	2008-02-13
\| \| \| \| \| \| \| \| \| \| \|	marge de manoeuvre vis a vis de eta dans l'unification : la convention est qu'on donne la forme eta-reduite avec l'indication du nombre d'expansions autorisées mais ce nombre était incorrect pour l'unification pattern de w_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de clear	notin	2008-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug 1795 (occur check was not correctly done)	herbelin	2008-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression code mort oublié lors du commit 10495	herbelin	2008-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10550 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Granting wish 1794 (the name provided in the "using" clause of the	herbelin	2008-02-10
\| \| \| \| \| \| \| \| \|	"abstract" tactical is now as a regular ltac parameter of the "identifier" type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backport Program Instance into Instance. Proper early error message if	msozeau	2008-02-10
\| \| \| \| \| \| \| \| \| \|	trying to declare an instance with an already existing name. Add possibility of not giving all the fields in Instance declarations, using Refine.refine to generate the subgoals. No control over opacity in this case though... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proposal of a nice notation for constructors xI and xO of type positive	letouzey	2008-02-10
\| \| \| \| \| \| \| \|	More details in the header of BinPos.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Major revision: use of Function, including some non-structural ones	letouzey	2008-02-10
\| \| \| \| \| \| \| \| \|	Sequel of commit 10545 on FSetAVL. This time, no compile-time penality since there are fewer non-structural functions in FMapAVL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Major revision of FSetAVL: more Function, including some non-structural ones	letouzey	2008-02-09
\| \| \| \| \| \| \| \| \| \| \| \| \|	NB: this change adds about 10s of compile-time to a file that is already taking about 30s on my machine. If somebody strongly objects to this, contact me. I really think that the gain in uniformity, clarity, and computability (in Coq) worth the extra compile-time: no more function-by-tactic, everything (vm_)computes, and quite efficiently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10545 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Solde de code mort et petites optimisations sur lesquels je suis	herbelin	2008-02-09
\| \| \| \| \| \| \|	tombé au cours du temps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
\| \| \| \| \| \| \| \| \|	only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
*	misc improvements	letouzey	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10539 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of CHANGES and refman doc for the implicit argument binder	msozeau	2008-02-08
\| \| \| \| \| \| \|	`X`. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	better comments in FMapInterface	letouzey	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10536 85f007b7-540e-0410-9357-904b9bb8a0f7
*	better comments in FSetInterface	letouzey	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10535 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Change implementation of resolution for typeclasses to use a customized	msozeau	2008-02-08
\| \| \| \| \| \| \| \|	eauto instead of an arbitrary tactic. Export more from eauto to allow easier debugging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add more information to IllFormedRecBody exceptions, to show the exact	msozeau	2008-02-08
\| \| \| \| \| \| \| \|	definition on which it is failing (useful for Program definitions and others too). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10533 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10532 85f007b7-540e-0410-9357-904b9bb8a0f7