coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	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
*	* 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
*	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
*	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
*	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
*	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
*	* 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
*	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
*	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
*	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
*	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
*	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
*	Changed Tauto so it displays less 'Unfold not iff'	corbinea	2003-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3706 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea	2003-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3603 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bugs Tauto	courant	2002-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3\|- ?]	corbinea	2002-07-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant	2002-07-15
\| \| \| \| \| \| \|	de la forme (E->F)->G. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2002-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea	2002-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2704 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de	herbelin	2002-05-15
\| \| \| \| \| \| \|	gauche à droite des hypothèses dans Intuition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2696 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement VTactic est gardé pour y plonger les tactiques ML, le	herbelin	2002-05-15
\| \| \| \| \| \| \|	VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2693 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
*	nettoyage code	courant	2002-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	2002-03-21
\| \| \| \| \| \| \| \|	soi-même si nécessaire) : l'idée est d'avoir un comportement clair et toujours aussi rapide que possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
\| \| \| \| \| \| \| \|	used to solve the goal remaining after propositional destructuration of the goal and the hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2554 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tauto est maintenant stable par "Intro" :	courant	2002-03-15
\| \| \| \| \| \| \| \| \| \| \| \|	Tauto montre (x:nat)(P x) \|- (x:nat)(P x) aussi bien que \|- (x:nat)(P x)->(P x) Intuition aussi. De plus, Intuition résout maintenant tout ce que Tauto sait résoudre ; par exemple (A,B,C:Prop)A\/(B/\C->C/\B) (ce qui n'était pas le cas jusqu'ici). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2533 85f007b7-540e-0410-9357-904b9bb8a0f7
*	substitution et pattern modulo let	barras	2002-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de la réduction sous forme d'implications d'atomes en fn de tête	herbelin	2001-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2356 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de Hnf plutôt que Red	herbelin	2001-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2355 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelse	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2352 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Insertion de Red sur chaque atome dans Tauto et Intuition	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2347 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative d'amélioration du résultat de Intuition	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye	2001-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye	2001-09-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parsing	herbelin	2001-08-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme	courant	2001-08-08
\| \| \| \| \| \| \| \|	e1 -> e2 avec e1 type inductif ayant un unique constructeur constant. Cas typique : hypothese de la forme ~e=e. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵	herbelin	2001-06-25
\| \| \| \| \| \|	compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix d'un bug de Tauto	delahaye	2001-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug du a un Intros trop violent	delahaye	2001-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du cas True->A\|-B	delahaye	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1699 85f007b7-540e-0410-9357-904b9bb8a0f7