coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des ↵	herbelin	2005-12-26
\| \| \| \| \| \|	G_new en G_.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Allow auto to have a parametric argument (wish #967)	herbelin	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵	herbelin	2005-03-07
\| \| \| \| \| \|	statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵	herbelin	2004-12-29
\| \| \| \| \| \|	convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration type casted_open_constr pour tactique refine car l'unification ↵	herbelin	2004-12-09
\| \| \| \| \| \|	n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵	herbelin	2004-12-06
\| \| \| \| \| \|	tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug tactique fix	herbelin	2004-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5981 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression quotify	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	moved instantiate binding to extratactics	corbinea	2004-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	more evar stuff	corbinea	2004-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵	herbelin	2004-03-02
\| \| \| \| \| \|	variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵	herbelin	2004-03-01
\| \| \| \| \| \|	des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
\| \| \| \| \| \| \| \| \|	- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs avec Pose et Assert	barras	2004-01-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en valeur intropattern de paires et acceptation dans le 'as' de ↵	herbelin	2003-12-22
\| \| \| \| \| \|	induction/inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5128 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle tactique EExists	clrenard	2003-12-01
\| \| \| \| \| \| \|	Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation des politiques de nommage de NewDestruct sur arguments ↵	herbelin	2003-11-25
\| \| \| \| \| \|	recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵	barras	2003-11-13
\| \| \| \| \| \|	Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	factorisation et generalisation des clauses	barras	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits changements de syntaxe	barras	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'as' avant 'using' dans 'destruct'	herbelin	2003-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4838 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added Instantiate ... in	corbinea	2003-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Il ne faut pas mettre le constrarg des tactiques au niveau lconstr	herbelin	2003-11-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lettac -> set	barras	2003-10-16
\| \| \| \| \| \| \|	suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour nouvelle syntaxe	barras	2003-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cablage en dur de inversion	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵	herbelin	2003-09-12
\| \| \| \| \| \| \| \| \|	choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
\| \| \| \| \| \| \| \|	et tactiques; qqes bugs d'affichage; passage de la précédence des projections de 10 à 9 avec associativité à gauche git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pb de mot-cle	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4272 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
*	Bug compilation	herbelin	2003-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4192 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'	herbelin	2003-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4184 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
*	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
*	Factorisation des produits de même type; parenthèses autour des x:=c et ↵	herbelin	2003-04-29
\| \| \| \| \| \|	n:=c dans les 'with bindings' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3974 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
*	Bug pattern_occ_hyp_list	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3818 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