aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Un ++ au lieu d'un ;Gravatar herbelin2001-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections post contournement des streams avec ++Gravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage exceptions liées au vieux CaseGravatar herbelin2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + ↵Gravatar herbelin2001-12-16
| | | | | | suppression des @Coercion, @Local et @Local Coercion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2299 85f007b7-540e-0410-9357-904b9bb8a0f7
* compat ocaml 3.03Gravatar filliatr2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
* - condition de garde (suite)Gravatar barras2001-12-10
| | | | | | | - commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation de LocateGravatar barras2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message CasesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des '?' aussi dans le type des définitionsGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2228 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'une méthode directe pour indiquer le type des déclarations ↵Gravatar herbelin2001-11-19
| | | | | | à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage coercions et classesGravatar herbelin2001-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2179 85f007b7-540e-0410-9357-904b9bb8a0f7
* Choucroute entre les tables de synchronisation, les options -silent et les ↵Gravatar letouzey2001-11-08
| | | | | | etats initiaux de coq. Pour l'instant je remets Silent en asynchrone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2169 85f007b7-540e-0410-9357-904b9bb8a0f7
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2164 85f007b7-540e-0410-9357-904b9bb8a0f7
* OopsGravatar barras2001-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2159 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-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
* Reorganisation de Goption. Passage des options l'utilisant en synchroneGravatar letouzey2001-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification précoce qu'un lemme n'existe pas déjàGravatar herbelin2001-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2142 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵Gravatar herbelin2001-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
* Amélioration mise en page Print ML Module et Print ML ModuleGravatar herbelin2001-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Recordobj et conséquencesGravatar herbelin2001-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2122 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrthographeGravatar herbelin2001-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵Gravatar herbelin2001-10-12
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-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 constructeursGravatar barras2001-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilite WindozGravatar herbelin2001-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le fichier .vo etait ecrit dans un mauvais repertoire si ce dernier etait ↵Gravatar herbelin2001-09-26
| | | | | | trouve dans le path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaires pour make docGravatar herbelin2001-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation des options Set Printing and coGravatar herbelin2001-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place globalisation optionnelle pour Infix/DistfixGravatar herbelin2001-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre Not_foundGravatar herbelin2001-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug affichage Infix/DistfixGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2036 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
* On ignore les répertoires qui ne correspondent pas à des identsGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection hd d'une liste videGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2002 85f007b7-540e-0410-9357-904b9bb8a0f7
* make install dans coq_makefile et repertoire associe user-contrib ajoute au ↵Gravatar filliatr2001-09-19
| | | | | | load path au demarrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵Gravatar herbelin2001-09-19
| | | | | | le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de noms contenant la section pour Fact et RemarkGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option et d'une fonction compile pour fabriquer les .voGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du message d'erreur si une coercion mettant en jeu des locaux ↵Gravatar herbelin2001-09-18
| | | | | | n'est pas déclarée locale (le discharge fonctionnera bien silencieusement et c'est compatible V6.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug discharge d'une déclaration de coercion pour une constante non définie ↵Gravatar herbelin2001-09-18
| | | | | | dans la section courante git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1979 85f007b7-540e-0410-9357-904b9bb8a0f7
* Blindage de Show IntroGravatar letouzey2001-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Transformation de Remark/Fact en constantes non visibles sans qualificationGravatar herbelin2001-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵Gravatar herbelin2001-09-10
| | | | | | éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1946 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-23 19:37:22 +0000