aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* exported several functions that are used in the graphical interface pcoq.Gravatar bertot2001-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1363 85f007b7-540e-0410-9357-904b9bb8a0f7
* changed the design to have command groups executed in a protected mannerGravatar bertot2001-02-09
| | | | | | | rather than one command at a time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1362 85f007b7-540e-0410-9357-904b9bb8a0f7
* exported a few functions that are used in graphical interface pcoq.Gravatar bertot2001-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several pairs of different functions actually had the same name, soGravatar bertot2001-02-09
| | | | | | | that the older function could not be exported. New names have been introduced. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1360 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif de la syntax: assoc a droite pour RingGravatar mayero2001-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1359 85f007b7-540e-0410-9357-904b9bb8a0f7
* SimplificationsGravatar herbelin2001-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Scratch par defaut si rien n'est specifier dans Add LoadPathGravatar herbelin2001-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression warning no .coqrcGravatar herbelin2001-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1356 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification du make depend; fonctions de stat. util. memoire dans ↵Gravatar filliatr2001-02-08
| | | | | | certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
* modifs mineuresGravatar filliatr2001-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1354 85f007b7-540e-0410-9357-904b9bb8a0f7
* exporting traverse_to and mutate: they are used in pcoq.Gravatar bertot2001-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1353 85f007b7-540e-0410-9357-904b9bb8a0f7
* export a function that can be used to retrieve the context correspondingGravatar bertot2001-02-08
| | | | | | | to the current goal. This is needed for pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure approche du conflit path/freeze/library_root en séquentialisant ↵Gravatar herbelin2001-02-07
| | | | | | la partie asynchrone (path) de la partie synchrone (roots) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1351 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1350 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du Match ContextGravatar delahaye2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation du pretty-print pour les tactiquesGravatar delahaye2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modif pour les patterns de sous-termesGravatar delahaye2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Probleme synchronisation roots / inputstateGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1344 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message d'erreur absolute_referenceGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1343 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1342 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgt signature de type_of_existentialGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1341 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place extractionGravatar filliatr2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1339 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour les Unfold/Fold dans CbvGravatar delahaye2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1337 85f007b7-540e-0410-9357-904b9bb8a0f7
* EqDecideGravatar filliatr2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un exempleGravatar delahaye2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1335 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une commande pour afficher chaque coercion à la demandeGravatar herbelin2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1333 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une commande pour afficher chaque coercion à la ↵Gravatar herbelin2001-02-06
| | | | | | demandeparsing/g_basevernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension coerce_to_varGravatar herbelin2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration de classops; évolution en une version mieux intégrée au ↵Gravatar herbelin2001-02-05
| | | | | | reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration de classops; évolution en une version mieux intégrée au ↵Gravatar herbelin2001-02-05
| | | | | | reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleur traitement des noms explicites dans la Nametab; Différentation du ↵Gravatar herbelin2001-02-05
| | | | | | traitement des sections et des modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration de classops; évolution en une version mieux intégrée au ↵Gravatar herbelin2001-02-05
| | | | | | reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour Time pour ne pas etre oblige de mettre deux pointsGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1326 85f007b7-540e-0410-9357-904b9bb8a0f7
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
* D'autres exemplesGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'Apply dans TautoGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une heuristique pour les types dependantsGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du test de TautoGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message d'erreur plus explicite pour TautoGravatar delahaye2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1320 85f007b7-540e-0410-9357-904b9bb8a0f7
* rétablissement patch ClaudioGravatar filliatr2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1319 85f007b7-540e-0410-9357-904b9bb8a0f7
* rétablissement nouveau TautoGravatar filliatr2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1318 85f007b7-540e-0410-9357-904b9bb8a0f7
* Résolution d'un bug de simplificationGravatar delahaye2001-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1317 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2001-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1316 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2001-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des credits version V6.3Gravatar mohring2001-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1314 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 05:11:01 +0000