aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
* Petite correction sur un message d'erreur renvoyé au sous typage.Gravatar soubiran2007-01-30
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Correction du bug #1315:Gravatar notin2007-01-22
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
* Correction bug #1302Gravatar herbelin2007-01-17
* Correction du bug #1273 (problème avec les paramètres non récursivement un...Gravatar notin2006-12-12
* cosmetiqueGravatar barras2006-12-12
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* bug condition de gardeGravatar barras2006-12-08
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
* dependencesGravatar barras2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Ajout fold_rel_declaration et fold_named_declarationGravatar herbelin2006-10-27
* Correction de 2 bugs critiques du polymorphisme d'universGravatar herbelin2006-10-27
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
* Protection raise en début de séquence (en attendant que le code caché trou...Gravatar herbelin2006-10-12
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* Correction du bug #1181Gravatar jforest2006-09-14
* Indentation + typoGravatar notin2006-09-01
* Ajout iter_rel_context/iter_named_contextGravatar herbelin2006-09-01
* Appel à caml_modify pour Ocaml 3.07Gravatar notin2006-09-01
* Export de closedn pour EvarutilGravatar herbelin2006-08-28
* correction bug vm_computeGravatar bgregoir2006-08-25
* Modifications dans les scripts de configuration (coqtop et coqide affichent m...Gravatar notin2006-07-28
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Correction bug du polymorphisme de sort des inductifs (cas où les variables ...Gravatar herbelin2006-06-22
* Oh le joli bug dans le kernel:Gravatar letouzey2006-06-05
* retour au comportement antérieur pour une application de foncteur: Gravatar letouzey2006-05-30
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* Ajout substl_named_decl pour mode MapleGravatar herbelin2006-05-23
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Correction trou de typage des éliminations d'inductifs introduit dans commit...Gravatar herbelin2006-05-13
* correction bugs de condition de garde (fix + cofix)Gravatar barras2006-05-12
* correction bugs dans Cbv (beta n-aire)Gravatar barras2006-05-10
* subst. explicites avec vecteursGravatar barras2006-05-09
* amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)Gravatar barras2006-05-05
* fixed bug #804: removed useless reduction in fix guard checkingGravatar barras2006-05-03
* bug #1096: whd_stack on one arg of conversion had side-effect on the other argGravatar barras2006-05-03
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22