aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-02-09Two pairs of parentheses were missing.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1367 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09option -m (utilisation memoire)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1366 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09Bug point final dans la syntaxe theorem_bodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1365 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1364 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09exported several functions that are used in the graphical interface pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1363 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09changed the design to have command groups executed in a protected mannerbertot
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
2001-02-09exported a few functions that are used in graphical interface pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1361 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09Several pairs of different functions actually had the same name, sobertot
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
2001-02-08modif de la syntax: assoc a droite pour Ringmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1359 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08Simplificationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1358 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08Scratch par defaut si rien n'est specifier dans Add LoadPathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1357 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08Suppression warning no .coqrcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1356 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans ↵filliatr
certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08modifs mineuresfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1354 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08exporting traverse_to and mutate: they are used in pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1353 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08export a function that can be used to retrieve the context correspondingbertot
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
2001-02-07Meilleure approche du conflit path/freeze/library_root en séquentialisant ↵herbelin
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
2001-02-07code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1350 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Ajout du Match Contextdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1349 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1348 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Modif pour les patterns de sous-termesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1347 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Probleme synchronisation roots / inputstateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1346 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1345 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1344 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Message d'erreur absolute_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1343 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1342 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Chgt signature de type_of_existentialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1341 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06mise en place extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1339 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1338 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06Correction pour les Unfold/Fold dans Cbvdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1337 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06EqDecidefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1336 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06Ajout d'un exempledelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1335 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1334 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06Ajout d'une commande pour afficher chaque coercion à la demandeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1333 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06Ajout d'une commande pour afficher chaque coercion à la ↵herbelin
demandeparsing/g_basevernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1332 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Extension coerce_to_varherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1331 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au ↵herbelin
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
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au ↵herbelin
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
2001-02-05Meilleur traitement des noms explicites dans la Nametab; Différentation du ↵herbelin
traitement des sections et des modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1328 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au ↵herbelin
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
2001-02-05Correction pour Time pour ne pas etre oblige de mettre deux pointsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1326 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05D'autres exemplesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1324 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Pas d'Apply dans Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1323 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Ajout d'une heuristique pour les types dependantsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1322 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Ajout du test de Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1321 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Message d'erreur plus explicite pour Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1320 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05rétablissement patch Claudiofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1319 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05rétablissement nouveau Tautofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1318 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-27 00:28:49 +0000