coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs de vérification de la bonne fondation en présence de définitions ↵	herbelin	2001-10-03
\| \| \| \| \| \|	locales dans le type de l'inductif décroissant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction messages d'erreur	herbelin	2001-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	repare la perte d'opacite a la fermeture de section	barras	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2050 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparent	barras	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage des commentaires	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilté make doc	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2030 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Romega	mohring	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵	herbelin	2001-09-19
\| \| \| \| \| \|	des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des dir_path vide	herbelin	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Romega/names/Makefile	mohring	2001-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	exceptions	barras	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mauvais rattrapage d'exception	barras	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵	herbelin	2001-09-10
\| \| \| \| \| \|	éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage aux univers algébriques	herbelin	2001-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1941 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage aux univers algébriques	herbelin	2001-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de Type_1, inutile, et non prévu dans le modèle des univers ↵	herbelin	2001-09-09
\| \| \| \| \| \|	algébriques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1937 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mécanisme pour faire remonter les contraintes de typage sur les variables ↵	herbelin	2001-09-09
\| \| \| \| \| \|	de section au niveau du discharge, sans avoir à garder tout l'environnement de la section; suppression retypage du type des constantes déchargées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1935 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mécanisme pour faire remonter les contraintes de typage sur les variables ↵	herbelin	2001-09-09
\| \| \| \| \| \|	de section au niveau du discharge, sans avoir à garder tout l'environnement de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)	herbelin	2001-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Version de la reduction dans Closure plus econome en memoire:	barras	2001-09-05
\| \| \| \| \| \| \| \|	- la pile ne contient plus les arguments appliques deja consommes - ajout d'un "lock" sur les glacons en cours de calcul git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras	2001-09-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1920 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
*	Ajout add_prefix/add_suffix	herbelin	2001-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1868 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Comentaire errone.	clrenard	2001-07-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2001-07-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵	herbelin	2001-07-21
\| \| \| \| \| \|	par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout hashconsing univers	herbelin	2001-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Depliage des let-in dans le test de garde	herbelin	2001-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1822 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Normalisation du predicat synthetise pour les Case	clrenard	2001-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Facilites pour le debogguage des univers.	coq	2001-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option -quality	filliatr	2001-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un Let	letouzey	2001-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1763 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin	2001-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
\| \| \| \| \| \| \|	ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une fonction de remplacement d'un sous-terme par un terme.	clrenard	2001-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nettoyage extraction	filliatr	2001-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de la structure des points fixes	barras	2001-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
*	interdiction occ positives ET negatives dans Pattern	werner	2001-04-24
\| \| \| \| \| \| \| \|	(en fait dans term.ml, fonction subst_occ_gen BW git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1698 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reduction des let in dans whd_programs	filliatr	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1664 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un typage sûr pour Goal et Check	filliatr	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1647 85f007b7-540e-0410-9357-904b9bb8a0f7
*	to_constr renvoie directement un constr pour contourner l'ancien ↵	herbelin	2001-04-15
\| \| \| \| \| \|	Term.mk_constr qui ne respectait pas l'invariant des applications (>=1 arg et pas d'imbrication) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1595 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de mk_constr qui ne respectait pas l'invariant des applications ↵	herbelin	2001-04-15
\| \| \| \| \| \|	(>=1 arg et pas d'imbrication) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1594 85f007b7-540e-0410-9357-904b9bb8a0f7
*	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les ↵	filliatr	2001-04-11
\| \| \| \| \| \|	terms contenant des Evar pas des Metas; mise à jour des exemples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	réparation Correctness; options Extraction (changement de syntaxe)	filliatr	2001-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour pour ocamlweb	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1517 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration de la structure des univers	barras	2001-03-28
\| \| \| \| \| \| \| \|	elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
\| \| \| \| \| \| \|	les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7