aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
2001-02-14Bug affichageherbelin
2001-02-14MAJherbelin
2001-02-14mise a jourfilliatr
2001-02-14Stdlib -> Coqlib, Stock disparaitherbelin
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
2001-02-14prise en compte des défs locales dans les arguments des inductifs; meilleure...herbelin
2001-02-14Restructurationherbelin
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
2001-02-14Obsolète (cf Coqlib)herbelin
2001-02-14Test syntaxe avec motifs numériquesherbelin
2001-02-13Absolute URL for DTDs introducedsacerdot
2001-02-13Bug nommage Stdlibherbelin
2001-02-13export a function that is needed in pcoq.bertot
2001-02-13Make sure the initial state used in a protected loop is the state chose exactlybertot
2001-02-12Bug nombres en chiffres décimaux dans les Casesherbelin
2001-02-12Theoreme opaquesmohring
2001-02-10All errors were not well reported before. In particular syntax errors werebertot
2001-02-09Two pairs of parentheses were missing.bertot
2001-02-09option -m (utilisation memoire)filliatr
2001-02-09Bug point final dans la syntaxe theorem_bodyherbelin
2001-02-09MAJherbelin
2001-02-09exported several functions that are used in the graphical interface pcoq.bertot
2001-02-09changed the design to have command groups executed in a protected mannerbertot
2001-02-09exported a few functions that are used in graphical interface pcoq.bertot
2001-02-09Several pairs of different functions actually had the same name, sobertot
2001-02-08modif de la syntax: assoc a droite pour Ringmayero
2001-02-08Simplificationsherbelin
2001-02-08Scratch par defaut si rien n'est specifier dans Add LoadPathherbelin
2001-02-08Suppression warning no .coqrcherbelin
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans certains...filliatr
2001-02-08modifs mineuresfilliatr
2001-02-08exporting traverse_to and mutate: they are used in pcoq.bertot
2001-02-08export a function that can be used to retrieve the context correspondingbertot
2001-02-07Meilleure approche du conflit path/freeze/library_root en séquentialisant la...herbelin
2001-02-07code mortherbelin
2001-02-07Ajout du Match Contextdelahaye
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
2001-02-07Modif pour les patterns de sous-termesdelahaye
2001-02-07Probleme synchronisation roots / inputstateherbelin
2001-02-07Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirherbelin
2001-02-07Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirherbelin
2001-02-07Message d'erreur absolute_referenceherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-02-07Chgt signature de type_of_existentialherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-02-06mise en place extractionfilliatr
2001-02-06mise a jourfilliatr
2001-02-06Correction pour les Unfold/Fold dans Cbvdelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 02:57:37 +0000