aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print PathGravatar herbelin2000-09-10
* Nametab.init - bug correctedGravatar coq2000-08-21
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...Gravatar filliatr2000-06-21
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Amélioration capture des erreursGravatar herbelin2000-05-31
* Bugs d'index d'inductiveGravatar herbelin2000-05-22
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Adaptation pour nouveaux inductifs (cf Inductive)Gravatar herbelin2000-05-18
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* suppression de Fw pour les implicitesGravatar herbelin2000-05-03
* construct_reference prend en compte aussi les variables du contextGravatar filliatr2000-05-02
* portage Omega (code seulement)Gravatar filliatr2000-04-28
* discharge des axiomesGravatar filliatr2000-04-21
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* NettoyageGravatar herbelin2000-03-21
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* BroutillesGravatar herbelin2000-01-20
* Correction pbs liés aux evarGravatar herbelin2000-01-07
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* sauvegarde de la valeur de module_nameGravatar filliatr1999-12-14
* mise a jour de refiner.ml (reports de modifs de la V6.3)Gravatar barras1999-12-13
* - méthode load sur les HintsGravatar filliatr1999-12-13
* modulesGravatar filliatr1999-12-12
* bug: enregistrement de vartab au lieu de csttabGravatar filliatr1999-12-10
* - erreurs PretypeGravatar filliatr1999-12-10
* debug resetGravatar filliatr1999-12-10
* debug discharge et inductifsGravatar filliatr1999-12-10
* - constantes avec recettesGravatar filliatr1999-12-09
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
* correction bug construct_referenceGravatar filliatr1999-12-07
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* add_leaf -> application methode cacheGravatar filliatr1999-12-05
* bug make_strength repareGravatar filliatr1999-12-03
* module Discharge (ne fait rien pour l'instant)Gravatar filliatr1999-12-03
* - global_reference traite des variablesGravatar filliatr1999-12-03
* Modifs suite à intégration de class.mlGravatar herbelin1999-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-01 05:44:46 +0000