aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* Modification of emacs output: No more show script at the end of a proof.Gravatar 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
* Modification of "Show Intros": it now shows letins too.Gravatar courtieu2006-04-11
* Finalement, scopes utiles pour option 'where' (cf bug #1132)Gravatar herbelin2006-04-07
* Suppression du test Proof with <tac>Gravatar notin2006-04-05
* - correction du bug #1055Gravatar notin2006-03-27
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Correction du bug 808: il est maintenant interdit de déclarer une assomption...Gravatar coq2006-03-02
* Bug correction in saving proofs: If a hook opens a proof but does not close i...Gravatar bertot2006-02-13
* Messages nth brancheGravatar herbelin2006-02-07
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* warning seulement si mode verboseGravatar herbelin2006-02-06
* Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas laGravatar herbelin2006-01-30
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* *** empty log message ***Gravatar coq2006-01-16
* Correction dans vernac_exact_proof -- jmnGravatar coq2006-01-16
* Correction du bug #1055Gravatar coq2006-01-13
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Prise en compte de notations numérales définies au niveau utilisateur+ lég...Gravatar herbelin2006-01-08
* Réorganisation; suppression code mort; documentationGravatar herbelin2006-01-07
* Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...Gravatar herbelin2006-01-04
* Mini-restructurationGravatar herbelin2005-12-30
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
* 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 de stratégie vis à vis du positionnement du module Top en mode b...Gravatar herbelin2005-12-24
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Correction printer des Tactic NotationGravatar herbelin2005-12-23
* option '-top dir' now works also in batch mode (2ème)Gravatar herbelin2005-12-22
* option '-top dir' now works also in batch mode; it is even necessary to ensur...Gravatar herbelin2005-12-22
* Double bug de interp_modifiers anciennement caché par un troisième que les ...Gravatar herbelin2005-12-22
* Divers; restructuration des points d'entrée de ConstrinternGravatar herbelin2005-12-21
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...Gravatar herbelin2005-12-20
* Suppression de la mise en boite automatique si format utilisateurGravatar herbelin2005-12-19
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
* Changement des named_contextGravatar gregoire2005-12-02
* bug de coqide sous windows (bad file descriptor)Gravatar barras2005-11-23
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* - debugging og "Show Intros": no line breaking + fresh idsGravatar coq2005-11-08
* Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04
* Types inductifs parametriquesGravatar mohring2005-11-02