coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Contexte locale non-vide interdit a la fin d'un module ou module type	coq	2002-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Lazy manuelles dans le code	coq	2002-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Lazy experimentale temporaire...	coq	2002-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renoncement	herbelin	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2962 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
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de pop_named	barras	2002-02-22
\| \| \| \| \| \| \|	meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
\| \| \| \| \| \| \| \|	+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
\| \| \| \| \| \| \|	- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait	barras	2002-02-05
\| \| \| \| \| \| \|	boucler la condition de garde git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2454 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
*	types vs constr	herbelin	2001-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 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 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
*	Transparent	barras	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 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
*	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
*	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
*	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
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle implantation de la reduction	barras	2001-03-01
\| \| \| \| \| \| \|	suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un système optionnel de discharge immédiat; prise en ↵	herbelin	2001-02-14
\| \| \| \| \| \|	compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification du make depend; fonctions de stat. util. memoire dans ↵	filliatr	2001-02-08
\| \| \| \| \| \|	certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 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
*	Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name	herbelin	2000-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au ↵	herbelin	2000-11-27
\| \| \| \| \| \|	evaluable_constant qui change de type au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	print_id, print_sp -> pr_id, pr_sp	herbelin	2000-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout push_rels_assum	herbelin	2000-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout sp_of_global; Introduction constant_path = section_path	herbelin	2000-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code more concernant feu les abstractions	herbelin	2000-11-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@845 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵	herbelin	2000-11-06
\| \| \| \| \| \|	DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵	filliatr	2000-11-06
\| \| \| \| \| \|	constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 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
*	Simplifications autour de typed_type (renommé types par analogie avec ↵	herbelin	2000-10-18
\| \| \| \| \| \|	sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique :	herbelin	2000-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	declaration = definition \| assumption mode de reference = named \| rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifierconstrtyped_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout push_rec_types	herbelin	2000-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@695 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Elimination des coupures sur le type constant	herbelin	2000-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rebranchement de la tactique Let	herbelin	2000-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@638 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
*	Disparition du type oper mais nouveau type global_reference	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction de constr	herbelin	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 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
*	Suppression de Abst	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 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
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Centralisation prod_name and co dans Environ; mkLambda_string dans Term	herbelin	2000-05-18
\| \| \| \| \| \| \|	Effets de bords suite à la restructuration des inductives (cf Inductive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du langage de tactiques	delahaye	2000-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7