coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug NewInduction pour les inductifs de type 'ordinaux'	herbelin	2003-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug internalisation des Extern: la globalisation doit etre stricte	herbelin	2003-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4453 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à la V8 par défaut	herbelin	2003-09-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Interface Eauto	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indépendance vis à vis de Declare	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4372 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2003-09-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4352 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection traducteur contre meta de Grammar tactic	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4327 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	switching back to old tauto	corbinea	2003-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4219 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added hints into Ground	corbinea	2003-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4215 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de newtauto	corbinea	2003-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4214 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2003-06-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4209 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Une completion de l'interpretation des TacAlias pour la partie interpretable	herbelin	2003-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4206 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground Update.	corbinea	2003-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option translate_syntax pour caractériser l'interprétation du ↵	herbelin	2003-06-12
\| \| \| \| \| \|	traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traducteur + passage des noms de tactiques à kernel_name pour ↵	herbelin	2003-06-10
\| \| \| \| \| \|	compatibilité avec les foncteurs + réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground and CCsolve updates	corbinea	2003-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration affichage locations; prise en compte variables dans lettac; ↵	herbelin	2003-05-24
\| \| \| \| \| \|	ajout FreshId git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation d'un bug de backtracking qui lui-même succédait à une ↵	herbelin	2003-05-22
\| \| \| \| \| \|	inefficacité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4063 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preservation affichage des ?n en V7	herbelin	2003-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵	herbelin	2003-05-21
\| \| \| \| \| \|	les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Separation entre les propositions de syntaxe - suite	herbelin	2003-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Enhancement of the Ground tactic, addition of GTauto and GIntuition.	corbinea	2003-05-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3991 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
\| \| \| \| \| \| \|	définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the Ground tactic.	corbinea	2003-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵	letouzey	2003-04-16
\| \| \| \| \| \|	list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des appels de tactiques définies sans arguments	herbelin	2003-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug: lookup inapproprie dans subst_tactic	herbelin	2003-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Relachement globalisation Unfold en usage interactif	herbelin	2003-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Trop de restriction pour les TacDef	herbelin	2003-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des variables de grammaires de tactiques et dédollarisation ↵	herbelin	2003-04-08
\| \| \| \| \| \|	des metaident git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3854 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey	2003-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Replace aux égalités entre preuves	herbelin	2003-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3833 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un message à FailTac	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un message à FailTac; localisation des appels à des tactiques ↵	herbelin	2003-03-31
\| \| \| \| \| \|	définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
\| \| \| \| \| \| \|	idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed Relative names not,iff in Camlp4 quotation.	corbinea	2003-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Introducing Christine's Intuition1 and adding some invertible hyps.	corbinea	2003-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3780 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7