coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	maj	filliatr	2002-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2688 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mention -dump-glob	filliatr	2002-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2687 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Changement de l'ordre de filtrage dans "Match Context"	herbelin	2002-05-14
\| \| \| \| \| \| \| \| \| \| \|	- Protection des "Match Context" contre les exceptions non UserError ni Fail - Remplacement des fermetures ML dans VTactic et VFTactic par des expressions de tactiques pour permettre l'intégration de Tactic Definition dans les états - Changement en conséquence de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'une construction spéciale SECVAR pour gérer la	herbelin	2002-05-14
\| \| \| \| \| \| \| \| \|	globalisation des variables de section (en espérant plus de robustesse vis à vis des bugs récurrents de Infix pour les variables avec implicites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2684 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petite erreur de syntaxe	barras	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2683 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modification de clenv_merge:	barras	2002-05-14
\| \| \| \| \| \| \| \| \|	on ajoute en premier lieu les contraintes concernant le terme puis apres celles concernant le type de chaque instantiation, au lieu d'alterner l'ajout de contraintes de terme et de type. A l'essai. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2682 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la modification des sortes d'elimination	mohring	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite	barras	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de eq en eqT comme equivalence de setoide par defaut.	clrenard	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2679 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encore des lemmes sur Zdiv	filliatr	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2678 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveaux lemmes dans Zdiv (Claude Marche)	filliatr	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation des de Bruijn pour la constructions des records et de leur ↵	herbelin	2002-05-13
\| \| \| \| \| \|	projections; plus de projection si le nom est '_' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2676 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas de projection si le nom d'un champ est '_' dans un Record	herbelin	2002-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de souplesse pour les constructeurs encapsulés sous des définitions	herbelin	2002-05-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmétique	herbelin	2002-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation	herbelin	2002-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2667 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2002-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2666 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification du filtrage si la premiere ligne de motifs est inevitable + ↵	herbelin	2002-05-03
\| \| \| \| \| \|	autres bugs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2665 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor correction of get_lem_name	coq	2002-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2664 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nettoyage code	courant	2002-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit bug dans les noms de fichiers	letouzey	2002-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2662 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lemmes sur Zdiv/Zmod	filliatr	2002-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	jLogic disparaît	herbelin	2002-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique ↵	filliatr	2002-04-19
\| \| \| \| \| \|	FourierR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression d'un warning plus surprenant qu'utile	herbelin	2002-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2658 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	letouzey	2002-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	werner	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2656 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout remarques diverses et tactiques	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typed unification in the case of Pattern	barras	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques bugs avec inject_nat	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 85f007b7-540e-0410-9357-904b9bb8a0f7
*	jLogic.mli remplace par jolic.mli	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2652 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2651 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2649 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement/renommage de Class.stre_max en Declare.strength_min	herbelin	2002-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2648 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2002-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2647 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refine the procedure that generalizes context to current goal.	huang	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	integration de coq-inferior par Marco Maggesi	filliatr	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2645 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq-inferior, by Marco Maggesi	filliatr	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj doc extraction dans repertoire contrib/extraction	letouzey	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	backtrack unification	barras	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition	courant	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2641 85f007b7-540e-0410-9357-904b9bb8a0f7
*	q: Commande introuvable.	herbelin	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2640 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Interdiction de nommer une constante comme une variable de section (plus ↵	herbelin	2002-04-12
\| \| \| \| \| \|	simple que d'afficher en nom long...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2637 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj test des reals	letouzey	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2636 85f007b7-540e-0410-9357-904b9bb8a0f7