coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
\| \| \| \| \| \| \| \| \| \| \|	the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 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
*	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
*	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵	herbelin	2003-09-12
\| \| \| \| \| \|	interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
*	V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclass	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pb quand une meme classe est definie dans 2 fichiers	herbelin	2003-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4138 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tables logarithmiques pour les coercions + nettoyage	herbelin	2003-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 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
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
\| \| \| \| \| \| \| \| \| \| \|	- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 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
*	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
*	Le chargement des coercions est nécessaire même si le module n'est pas ouvert	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2409 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
*	Mise en place de coercion dans les motifs	herbelin	2001-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2285 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin	2001-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage coercions et classes	herbelin	2001-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2179 85f007b7-540e-0410-9357-904b9bb8a0f7
*	GROS COMMIT:	barras	2001-11-05
\| \| \| \| \| \| \| \| \| \|	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	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
*	Les tables de coercions ne doivent pas survivre aux sections	herbelin	2001-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1833 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Débogage discharge des coercions; nettoyage	herbelin	2001-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1827 85f007b7-540e-0410-9357-904b9bb8a0f7
*	message Ambiguous paths seulement si verbose	filliatr	2001-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1824 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
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une commande pour afficher chaque coercion à la ↵	herbelin	2001-02-06
\| \| \| \| \| \|	demandeparsing/g_basevernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1332 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration de classops; évolution en une version mieux intégrée au ↵	herbelin	2001-02-05
\| \| \| \| \| \|	reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1327 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un nom long pour les variables de section qui font classe ou coercion; ↵	herbelin	2000-12-25
\| \| \| \| \| \|	réorganisation; bugs discharge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1201 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de certains sp_of_id par des locate	herbelin	2000-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@956 85f007b7-540e-0410-9357-904b9bb8a0f7
*	certains effets disparaissent a la sortie des sections, d'autres non (selon ↵	filliatr	2000-11-24
\| \| \| \| \| \|	Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de global_reference dans rawconstr	herbelin	2000-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	methode export	filliatr	2000-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵	herbelin	2000-11-10
\| \| \| \| \| \|	library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression des (* open Generic *)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage AppL en App	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction pour make doc	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
\| \| \| \| \| \| \|	Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation bug des coercions (cas ou on importe une coercion faisant	barras	2000-08-08
\| \| \| \| \| \| \|	reference a une classe non importee) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement non-affichage des coercions dans termast	herbelin	2000-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@264 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
\| \| \| \| \| \| \| \| \|	les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement type add_anonymous_leaf	filliatr	1999-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@206 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifs suite à intégration de class.ml	herbelin	1999-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@192 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichage classes et coercions	filliatr	1999-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@187 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	portage Astterm (partiellement)	filliatr	1999-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Classops; ajout de fonctions dans Declare en consequence	filliatr	1999-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des progres dans l'integration	herbelin	1999-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@140 85f007b7-540e-0410-9357-904b9bb8a0f7