aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Suppression code inactif et commentaire apparemment incorrect (pour éviter c...Gravatar herbelin2005-09-09
* Simplification message d'anomalieGravatar herbelin2005-09-08
* argument inutilisé de zip: toujours l'identitéGravatar letouzey2005-08-22
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ...Gravatar herbelin2005-07-21
* reactivation de l optim des fermeturesGravatar barras2005-07-13
* backtrack modif de knh...Gravatar barras2005-07-13
* *** empty log message ***Gravatar barras2005-07-13
* test du tag de reductionGravatar barras2005-07-12
* Correction bug #983Gravatar herbelin2005-06-28
* Bug fix for a bug reported by Roland: the function that detects the constantsGravatar sacerdot2005-05-23
* Bug affichage graphe universGravatar herbelin2005-05-05
* Code v7 obsoleteGravatar herbelin2005-05-05
* MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...Gravatar herbelin2005-05-05
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Added map_named_contextGravatar herbelin2005-02-18
* Moved Indmap and ConstrMap from Libnames to Names for use in CookingGravatar herbelin2005-02-18
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
* Uniformisation de destApplication en destApp; simplification decompose_appGravatar herbelin2005-02-12
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* 1. added code to handle the inclusion of inductive types and constructors inGravatar sacerdot2005-01-17
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* [ Waiting for a keyword to control expansion during functor application ]Gravatar sacerdot2005-01-05
* HUGE COMMITGravatar sacerdot2005-01-03
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* CommentaireGravatar herbelin2004-12-06
* *** empty log message ***Gravatar gregoire2004-11-29
* Code mortGravatar herbelin2004-11-22
* compatibility with POWERPCGravatar gregoire2004-11-22
* bug module with ... + vmGravatar barras2004-11-17
* bug module M:=N avec vmGravatar barras2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)Gravatar barras2004-10-20
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* Fusion comparaison Const/Var; export is_opaqueGravatar herbelin2004-06-02
* Un bug résiduel (mais pas bien méchant) du noyauGravatar herbelin2004-05-27
* Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...Gravatar herbelin2004-03-28
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* Inductive Types : seuls les petits types sont unitairesGravatar mohring2003-12-19
* bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)Gravatar barras2003-12-16
* *** empty log message ***Gravatar barras2003-11-27
* modif lexer: ident peut commencer par _Gravatar barras2003-11-25
* CC: added injection theoryGravatar corbinea2003-11-25