aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* 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
* Ajout recarg_lengthGravatar herbelin2003-11-18
* Suppression StronglyClassical, StronglyConstructive devient plus concretement...Gravatar herbelin2003-11-08
* Message inductive largeGravatar herbelin2003-10-28
* Set devient predicatif par defautGravatar herbelin2003-10-28
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
* Correction bug 328Gravatar coq2003-09-23
* message d'erreur de garde des cofixGravatar barras2003-09-22
* bug fix: term reduced in bad envGravatar barras2003-09-18
* Mise en place possibilité de définitions locales dans les paramètres des i...Gravatar herbelin2003-09-06
* Ajout de l'opti des fermeture (mais debranche pour l'instant)Gravatar barras2003-08-06
* Improved reduction machine with closure: should use less memoryGravatar barras2003-08-05
* Comparaison de Cases module mind_equivGravatar coq2003-06-30
* *** empty log message ***Gravatar courant2003-06-27
* Simplification case_infoGravatar herbelin2003-06-10