coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	maj	filliatr	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3434 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3428 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du vernac Proof with	gregoire	2002-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3420 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrections de gestion des univers et modules + meilleure gestions des ↵	coq	2002-12-09
\| \| \| \| \| \|	noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3383 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3370 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3346 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3338 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3318 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation de la librairie des réels	desmettr	2002-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3306 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Option pour compiler une version 'light' des réels	desmettr	2002-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3299 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2002-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3296 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3286 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3274 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵	herbelin	2002-11-24
\| \| \| \| \| \|	améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3249 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3246 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj apres reparation d'un bug coqdep	letouzey	2002-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3244 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3230 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3215 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
*	maj	filliatr	2002-11-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3200 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3170 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3150 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commit du calcul des dependances un peu plus robuste	barras	2002-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3146 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3131 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
*	maj	filliatr	2002-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3058 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-09-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3050 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	La notation with dependante + affichage dependante de moduels corrige	coq	2002-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7