coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Utilisation du mot-clé lazymatch pour le match paresseux (à défaut ↵	herbelin	2006-07-11
\| \| \| \| \| \|	d'avoir trouver mieux) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9037 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵	herbelin	2006-05-30
\| \| \| \| \| \|	permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une ↵	herbelin	2006-03-05
\| \| \| \| \| \|	référence explicitement de ltac + suppression de la répétition de l'entrée 'reference' dans tactic_atom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵	herbelin	2006-01-21
\| \| \| \| \| \|	fail peuvent maintenant être des listes de string, int et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵	herbelin	2005-05-17
\| \| \| \| \| \|	aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵	herbelin	2004-10-11
\| \| \| \| \| \|	evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 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
*	Changement de natural en int_or_var pour 'do' et 'fail' pour ↵	herbelin	2004-03-02
\| \| \| \| \| \|	paramétrisation dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 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
*	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
*	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
*	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 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
*	Ajout FreshId	herbelin	2003-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4072 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; réparation local défs récursive dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 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
*	reparations suite a la nouvelle syntaxe:	barras	2003-03-14
\| \| \| \| \| \| \| \|	- syntaxe des modules - syntaxe existentielle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3769 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
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵	herbelin	2003-01-19
\| \| \| \| \| \|	la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 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
*	L'application de ltac attend une référence; meilleure protection contre	herbelin	2002-10-14
\| \| \| \| \| \| \|	les erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵	herbelin	2002-10-13
\| \| \| \| \| \|	hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Eval, Inst et Check	delahaye	2002-05-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 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@2695 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Meilleure gestion de la reduction dans Field	delahaye	2002-03-17
\| \| \| \| \| \| \| \| \| \|	Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	On ne peut plus appliquer des arguments à une syntaxe primitive	herbelin	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2317 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
*	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
*	Changements dans le traitement des qualid's	delahaye	2001-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1859 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