coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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
*	Add printer for Pp.std_ppcmds...	msozeau	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10531 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New "Preterm [ of id ] " command to show the preterm before giving it to	msozeau	2008-02-08
\| \| \| \| \| \| \|	Coq (solves part 2 of bug #1784). Add corresponding documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10530 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backport code from command.ml to subtac_command.ml for definining	msozeau	2008-02-08
\| \| \| \| \| \| \| \| \| \|	recursive definitions. Now program accepts cofixpoints and uses the new way infer structurally decreasing arguments. Also, checks for correct recursive calls before giving the definition to the obligations machine (solves part 1 of bug #1784). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
*	more complete FSets.v	letouzey	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10528 85f007b7-540e-0410-9357-904b9bb8a0f7
*	updates concerning FSets	letouzey	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10527 85f007b7-540e-0410-9357-904b9bb8a0f7
*	one forgotten compatibility lemma	letouzey	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli dans r10524	notin	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10525 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de Coqdoc + ajout de Include dans les mots clés ↵	notin	2008-02-08
\| \| \| \| \| \|	reconnus par Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'une toute petite amélioration de l'unification de	herbelin	2008-02-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	apply : si on a trouvé une méta, alors, on l'utilise pour instancier les trous lors de la tentative de conversion modulo delta. Cela permet ainsi de résoudre de petits cas d'unification, tel que celui annoncé échouant dans le "beginner question" du 6 fevrier 2008 de coq-club. Solde au passage de modifs cosmétiques de setoid_replace.ml avant abandon probable du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite 10518	herbelin	2008-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10521 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin	2008-02-06
\| \| \| \| \| \| \| \| \| \| \|	Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de Set Strongly Strict Implicit : il contient maintenant Set Strict Implicit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Détection plus souple et message un peu moins radical en cas de	herbelin	2008-02-06
\| \| \| \| \| \| \|	fichiers emacs ouverts au moment de la création des dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10519 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug à l'interprétation de "change" (on exigeait que	herbelin	2008-02-06
\| \| \| \| \| \| \| \|	l'argument soit un type même lorsque c'était un terme qu'on convertissait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Résolution d'une confusion dans le rôle des variables CAMLP4 et CAMLP4LIB:	herbelin	2008-02-06
\| \| \| \| \| \| \| \|	- CAMLP4 dit si on utilise camlp4 ou camlp5 - CAMLP4LIB est le chemin camlp4/5 à donner en option -I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10517 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix obligations not being discharged due to new definition of complement.	msozeau	2008-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New algorithm to resolve morphisms, after discussion with Nicolas	msozeau	2008-02-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Work-in-progress to make eauto accept a list of goals as input and	msozeau	2008-02-06
\| \| \| \| \| \| \| \| \|	return a solution for the whole set of goals at once only. Add "debug eauto" and "dfs eauto" syntaxes to get better control on the algorithm from the surface interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre l'erreur mentionnée dans le rapport de bug 1790	herbelin	2008-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	kill some useless module aliases E:=X (for better name printing, see Elie's ↵	letouzey	2008-02-05
\| \| \| \| \| \|	14097) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7