coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	MAJ	herbelin	2006-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9219 85f007b7-540e-0410-9357-904b9bb8a0f7
*	avertissement a propos du commit 9211 dans CHANGES	letouzey	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1204 + maj CHANGES	notin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin	2006-09-22
\| \| \| \| \| \| \| \|	Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9142 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9111 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
\| \| \| \| \| \| \| \| \| \| \| \| \|	- extension de l'unification au cas de motifs (au sens de Dale Miller) [appel de solve_pattern_eqn dans evar_conv_x], - correction de bugs présumés dans real_clean et do_restrict_hyp (prise en compte de la taille courante du contexte de de Bruijn), - ajout d'une heuristique de beta-reduction de tete dans real_clean (cf test-suite/success/unification.v), - suppression de certains "try ... with _ => ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9088 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ doc/refman	notin	2006-07-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9040 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-07-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9039 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-07-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9031 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ doc	herbelin	2006-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9021 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ du manuel de référence	notin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8956 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 ↵	jforest	2006-06-12
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle MAJ	herbelin	2006-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8939 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changements de dernieres minutes pour la 8.1 beta:	letouzey	2006-06-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- qualification correcte des noms en Haskell - on imprime les types de toutes les fonctions en Haskell - en Ocaml, les appels recursifs d'une f : 'a truc doivent se faire avec les _meme_ parametres de types 'a. Exemple illegal: let rec f = function [] -> 0 \| l -> f [l];; On met maintenant des Obj.magic en conséquence. En Haskell (avec typage fourni), ca passe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8930 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle MAJ	herbelin	2006-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8927 85f007b7-540e-0410-9357-904b9bb8a0f7
*	replace by	herbelin	2006-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8918 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Whelp	herbelin	2006-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8916 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8859 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de mes modifs recentes	letouzey	2006-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8830 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Centralisation de la détection lettre/symbole par le lexeur dans les plages ↵	herbelin	2006-05-10
\| \| \| \| \| \|	unicode; ajout de nouvelles plages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)	courtieu	2006-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8697 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8137 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'exists! x:A, P	herbelin	2006-02-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin	2006-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bibliothèque String de Laurent Théry	herbelin	2006-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Idem numbering of 'Unfold', 'simpl', ...	herbelin	2006-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin	2006-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile	herbelin	2006-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7995 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ (synonymes de Lemma; auto using)	herbelin	2006-01-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7945 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export eassumption	herbelin	2006-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extended Unicode support	herbelin	2006-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom	herbelin	2006-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
\| \| \| \| \| \| \| \|	- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout paramétricité du nom de la base de hint dans auto et trivial	herbelin	2006-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur; ↵	herbelin	2005-12-26
\| \| \| \| \| \|	changements collatéraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2005-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7714 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Declare Implicit Tactic	herbelin	2005-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7365 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add a left and right tactic for classical logic	narboux	2005-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fold	herbelin	2005-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added entry constr_may_eval for tactic extensions (new syntax)	herbelin	2005-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7162 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New environment variable COQREMOTEBROWSER to set the command used by Coq	sacerdot	2005-05-26
\| \| \| \| \| \| \| \|	and coqide to control a remote browser. It uses the standard syntax where "%s" is the placeholder for the URL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7077 85f007b7-540e-0410-9357-904b9bb8a0f7