coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵	herbelin	2006-07-11
\| \| \| \| \| \|	romega_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	utilisation de la VM pour la normalisation finale de romega	letouzey	2006-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correctifs de bug pour romega:	letouzey	2006-03-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1) dans refl_omega, on donnait a OmegaSolver un generateur de numero d'equations new_eq_id qui pouvait clasher avec les numeros d'equations initiaux créés avec new_omega_id. => on sépare en deux compteurs, un pour les equations omegas, l'autre pour les variables omegas. On en profite pour reinitialiser ces compteurs à chaque session romega, histoire que romega devienne reproductible. 2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti à un endroit. ATTENTION: ceci peut changer le comportement d'omega. Surveiller le resultat du prochain bench nocturne. 3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication dans une hypothese lors du recalcul final. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
\| \| \| \| \| \| \|	et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction des noms v7 de Z en noms v8	herbelin	2005-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7726 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage suite à la détection par défaut des variables inutilisées par ↵	herbelin	2005-11-08
\| \| \| \| \| \|	ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas de dépendance en Omega	herbelin	2005-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6764 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_true	herbelin	2005-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6763 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- changement ordre arguments interp_goal_concl pour permettre application	herbelin	2005-02-21
\| \| \| \| \| \| \| \|	partielle - amélioration traduction en nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction de bugs	herbelin	2005-02-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- filtrage sur Bigint.zero incorrect: zero était considéré comme une variable - coq_false et coq_true au lieu de coq_False et coq_true - vérification chargement ROmega.vo - Divers - changement ordre argument interp_goal_concl pour permettre application partielle - amélioration débogueur - ajout interprétation Zsucc, Zopp, et gel de Zmult si non scalaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation of function names about global references (especially, ↵	herbelin	2005-02-18
\| \| \| \| \| \|	renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)	herbelin	2004-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise ↵	herbelin	2004-12-27
\| \| \| \| \| \|	par romega (omega2.ml, qui, l'occassion, disparat sous ce nom) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 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
*	Reparation ROmega V8/Omega ZERO/POS/NEG	mohring	2004-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adaptation V8 version Pierre Cregut	mohring	2004-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5428 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵	herbelin	2003-11-29
\| \| \| \| \| \|	par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique d'un lemme redondant	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique d'un lemme redondant	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cacher les .v8	herbelin	2003-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un peu plus de souplesse dans la globalisation des noms utilises par les ↵	herbelin	2003-09-26
\| \| \| \| \| \|	tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Branchement constant sur Coqlib	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4354 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
*	MAJ	herbelin	2003-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3598 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification de Simplify (plus de ())	herbelin	2003-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3537 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3394 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 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
*	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
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 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@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des corps de letin dans les hypothèses	herbelin	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2505 85f007b7-540e-0410-9357-904b9bb8a0f7
*	convert_hyp a change de type	barras	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2503 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
*	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
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵	herbelin	2001-10-17
\| \| \| \| \| \|	sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵	herbelin	2001-10-12
\| \| \| \| \| \|	grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 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
*	Romega	mohring	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ V7.1	herbelin	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1993 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation Zne	mohring	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1989 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