coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de ↵	herbelin	2002-03-22
\| \| \| \| \| \|	Zsyntax et de Rsyntax (dont les règles ne s'appliquent plus dans le même ordre depuis la modification de l'ordre de chargement des Require) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2564 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An intuitionistic first-order theorem prover -- JProver.	huang	2002-03-22
\| \| \| \| \| \| \|	See the "README" file for more information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7
*	backtrack de l'unification	barras	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2562 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du test des reals	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Décomposition de l'application n-aire en application binaire pour que ↵	herbelin	2002-03-21
\| \| \| \| \| \|	Pattern réussisse sur des motifs partiellement appliqués git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2560 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	2002-03-21
\| \| \| \| \| \| \| \|	soi-même si nécessaire) : l'idée est d'avoir un comportement clair et toujours aussi rapide que possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	considerations de pretty-print	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2558 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deux fichiers supplementaires de customisation d'extraction	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2557 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement du test extraction suite aux modif inining	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modification de l'auto-inlining	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2555 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
\| \| \| \| \| \| \| \|	used to solve the goal remaining after propositional destructuration of the goal and the hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2554 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encore quelques petites modif de l'unification	barras	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2553 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renversement du renommage des variables	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du controle de l'apparition des termes	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reorganisation des simplifications: letin eta-expansé apres le kill-dummy	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2550 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un peu moins d'eta-expansion autour des Glob	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug optimize_fix fait trop tot	letouzey	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2548 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite bug Dglob constant	letouzey	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug avec les MLglob vraiment constants	letouzey	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	travail sur les stratégies de réduction	letouzey	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2545 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remplacement des deux constants prop/arity par une seule dummy + ↵	letouzey	2002-03-19
\| \| \| \| \| \|	pretty-print des fix mutuels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2544 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de l'entrée ne_constrarg_list	delahaye	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2543 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix d'un bug sur le test des inverses	delahaye	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2542 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Exportation de SplitRmult et SplitAbsolu	delahaye	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2541 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement de look_for_interp	delahaye	2002-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2540 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Field ne fait maintenant que les reductions necessaires	delahaye	2002-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2539 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Meilleure gestion de la reduction dans Field	delahaye	2002-03-17
\| \| \| \| \| \| \| \| \| \|	Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	epsilon	letouzey	2002-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2537 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changements récents dans l'extraction	letouzey	2002-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2536 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un peu de mise a jour de la doc extraction	letouzey	2002-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2535 85f007b7-540e-0410-9357-904b9bb8a0f7
*	evite les clash avec le type ocaml unit	letouzey	2002-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2534 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tauto est maintenant stable par "Intro" :	courant	2002-03-15
\| \| \| \| \| \| \| \| \| \| \| \|	Tauto montre (x:nat)(P x) \|- (x:nat)(P x) aussi bien que \|- (x:nat)(P x)->(P x) Intuition aussi. De plus, Intuition résout maintenant tout ce que Tauto sait résoudre ; par exemple (A,B,C:Prop)A\/(B/\C->C/\B) (ce qui n'était pas le cas jusqu'ici). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2533 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros commit: principalement ajout des lambdas arity + leur optimisation en ↵	letouzey	2002-03-15
\| \| \| \| \| \|	temps normal + beaucoup de simplifications diverses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation semi setoid ring	clrenard	2002-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2531 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de lemmes	mohring	2002-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2530 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cleanconfig efface ocamldebug-v7	filliatr	2002-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2529 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2528 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retablissement de interp_tab + injection id -> constr sans goal	delahaye	2002-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2527 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Propagation du pb de conversion dans clenv_unify	herbelin	2002-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2002-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2525 85f007b7-540e-0410-9357-904b9bb8a0f7
*	open Univ inutile	courant	2002-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile	courant	2002-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorisation de la grammaire pour Extraction Language.	letouzey	2002-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renommage de fonctions	barras	2002-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2521 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2520 85f007b7-540e-0410-9357-904b9bb8a0f7
*	raccourci -l en plus de -load-vernac-source	letouzey	2002-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2519 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplify_eq echouait sur des hypotheses trivial comme O=O	barras	2002-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clear ne substitue plus le corps dans le reste du but	barras	2002-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2517 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2002-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'une entree 'binaries' pour recompiler coq mais pas les theories	barras	2002-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2515 85f007b7-540e-0410-9357-904b9bb8a0f7