coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Prise en compte des alias syntaxiques vers des references dans divers lieux ↵	herbelin	2003-11-12
\| \| \| \| \| \|	de globalisation des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4869 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 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
*	Traduction semantique des InHyp de clause en InHypValue si local def; ↵	herbelin	2003-11-09
\| \| \| \| \| \|	simplification suite fusion eq/eqT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4840 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ↵	herbelin	2003-11-09
\| \| \| \| \| \|	de Generalize Dependent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4834 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code obsolete	herbelin	2003-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4833 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2003-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4830 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
*	Amelioration message d'erreur avec pretyping; prise en compte syntactic def ↵	herbelin	2003-11-04
\| \| \| \| \| \|	dans Unfold git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4788 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug Double Inversion	herbelin	2003-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
\| \| \| \| \| \| \|	Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec ↵	herbelin	2003-10-21
\| \| \| \| \| \|	alpha-conversion et seulement apres avec conversion (suggestion de Carlos Simpson) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug FreshId	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4683 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des hints autorewrite	herbelin	2003-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4678 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de l'utilisation de contradiction	herbelin	2003-10-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Contradiction au cas d'hypotheses ~A et A dans le contexte	herbelin	2003-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4673 85f007b7-540e-0410-9357-904b9bb8a0f7
*	subst marche dans les deux sens	filliatr	2003-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle syntaxe de ltac	barras	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un Try supplementaire utile pour la compatibilite, car bring_hyps dans ↵	herbelin	2003-10-13
\| \| \| \| \| \|	generalizeRewriteIntros peut echouer (typage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation comportement decompEq pour corriger un bug introduit dans le ↵	herbelin	2003-10-11
\| \| \| \| \| \|	Inversion acceptant le nommage des hypotheses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4602 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug calcul du nom de la premiere equation	herbelin	2003-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4601 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4581 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dead of 'a somewhat cryptic module'	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; ↵	herbelin	2003-10-10
\| \| \| \| \| \|	pf_get_new_id moved to Tacmach) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4570 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Unification lemInv et lemInv_in	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4568 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
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4565 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des buts par Pfedit pour utilisation par les tactiques ↵	herbelin	2003-10-10
\| \| \| \| \| \|	(Setoid_replace) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4562 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
*	Bug utilisation nametab pour ltac	herbelin	2003-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4550 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des abbreviations pour constrintern.ml; generic argument IdentArg	herbelin	2003-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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