aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Expand)AuthorAge
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Correction bug #1477 sur ordre des variables partagées par les or-patterns.Gravatar herbelin2007-04-13
* Intégration de la modification suggérée par Michal Moskal (cf msg sur Coq ...Gravatar notin2007-04-02
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
* Ajout combinateurs option_fold_left et name_fold_mapGravatar herbelin2006-10-09
* Added a new option -emacs-U changing emacs prompt delimiters byGravatar courtieu2006-09-29
* Déplacement surround dans util.ml et parenthésage des déclarationsGravatar herbelin2006-09-23
* added congruence improvementGravatar corbinea2006-09-19
* Ajout array_distinctGravatar herbelin2006-09-12
* Code mortGravatar herbelin2006-09-05
* Force évaluation 'naturelle' de list_map2_i et list_map3 de gauche à droiteGravatar herbelin2006-09-01
* Petite optimisation récursive-terminale en passantGravatar herbelin2006-08-28
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
* Ajout array_fold_map2Ã'Gravatar herbelin2006-05-28
* r8931@thot: notin | 2006-04-28 16:19:38 +0200Gravatar notin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Modification of emacs output: Pp.warning and al now output warningGravatar courtieu2006-04-27
* Modification of emacs output: Pp.warning and al now output warningGravatar courtieu2006-04-27
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Ajout array_fold_map', list_fold_map' et list_remove_firstGravatar herbelin2006-03-29
* DocumentationGravatar herbelin2006-03-18
* Ajout pluralGravatar herbelin2006-02-07
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Déplacement de pr_arg et pr_opt de Ppconstr vers UtilGravatar herbelin2006-01-21
* Modification pour que l'ordre des éléments respecte l'ordre dans lequel ils...Gravatar herbelin2006-01-03
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* bug de coqide sous windows (bad file descriptor)Gravatar barras2005-11-23
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* pas besoin de List.length pour savoir si une liste est videGravatar letouzey2005-08-19
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* New environment variable COQREMOTEBROWSER to set the command used by CoqGravatar sacerdot2005-05-26
* Déplacement de fonctionnalités unix et browser de ide vers libGravatar herbelin2005-05-19
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Implementation of a new backtracking system, that allow to go backGravatar coq2005-04-20
* Bug synchronisation fonction connectGravatar herbelin2005-02-04
* Ajout d'un processus de communication entre Coq et un outil externeGravatar herbelin2005-02-04
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21