coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2963 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
*	Branchement de Assert, Pose et LetTac sur l'algo de création de noms	herbelin	2002-07-30
\| \| \| \| \| \| \|	frais de Intro git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2939 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative de réparation d'un bug Omega: une variable de section qui après ↵	herbelin	2002-06-06
\| \| \| \| \| \|	effacement ne peut être renommée pareille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2763 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
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	labels appliques dans un ordre incorrect	barras	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation convert_hyp; correction problème de dépendance dans letin_tac	herbelin	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2501 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
*	petit nettoyage de kernel/inductive	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement generation de schema d'elimination, False_rec est primitif, ↵	mohring	2002-01-31
\| \| \| \| \| \|	Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise de Intros id au format de Intro en forçant aussi la réduction si demandé	herbelin	2002-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2397 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
*	Parade contre effet indésirable du commit précédent	herbelin	2001-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2277 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration nommage hypothèses NewInduction (et incompatibilités)	herbelin	2001-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 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
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 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
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2164 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
*	Bug Induction (prise en compte let-in + ordre des dépendances dans thin)	herbelin	2001-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2134 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
*	Incompatibilité entre la prise en compte des univers au niveau des ↵	herbelin	2001-10-10
\| \| \| \| \| \|	tactiques et le test de conversion qui oublie la cumulativité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2107 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
*	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵	herbelin	2001-10-05
\| \| \| \| \| \|	'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction (double) bug de Generalize Dependent	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2037 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
*	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
*	Ajout syntaxe "Assert H:T."	herbelin	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1968 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
*	Nettoyage reduce_to_ind et one_step_reduce	herbelin	2001-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 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
*	Renommage TrueCut -> Assert	herbelin	2001-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1887 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵	herbelin	2001-08-07
\| \| \| \| \| \|	tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1883 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin	2001-08-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout code pour un Destruct similaire au NewInduction	herbelin	2001-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne ↵	herbelin	2001-07-13
\| \| \| \| \| \|	prend pas les letin en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1848 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras	2001-06-29
\| \| \| \| \| \| \|	universelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1817 85f007b7-540e-0410-9357-904b9bb8a0f7
*	traitement du let dans red_product (tactique Red)	barras	2001-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commit d'un bug de Apply.	barras	2001-06-27
\| \| \| \| \| \| \| \| \| \|	Avec Apply c, on essaie d'unifier le type de c avec le but courant. Si ca echoue on essaie d'expanser la constante de tete du type du theoreme, et essaie de faire Apply recursivement. Ca ameliore sensiblement la puissance de Apply mais ce n'est pas 100% backward-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1814 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵	herbelin	2001-06-25
\| \| \| \| \| \|	définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte env local (et defs locales) dans Change	herbelin	2001-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ↵	herbelin	2001-06-01
\| \| \| \| \| \|	des variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1776 85f007b7-540e-0410-9357-904b9bb8a0f7