aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-02-14Obsolète (cf Coqlib)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1376 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Test syntaxe avec motifs numériquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1375 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-13Absolute URL for DTDs introducedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1374 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-13Bug nommage Stdlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1373 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-13export a function that is needed in pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1372 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-13Make sure the initial state used in a protected loop is the state chose exactlybertot
at the time the protected loop was started. This makes it possible to have modifications of commands specific to the protected loop remembered throughout the session. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1371 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-12Bug nombres en chiffres décimaux dans les Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1370 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-12Theoreme opaquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1369 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-10All errors were not well reported before. In particular syntax errors werebertot
not correctly encapsulated in an acknowledge message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1368 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 01:57:56 +0000