aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Added a new option -emacs-U changing emacs prompt delimiters byGravatar courtieu2006-09-29
* Corrections mineuresGravatar notin2006-09-25
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Compatibilité hyp=var dans Tactic Notation + nettoyageGravatar herbelin2006-09-15
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Indentation + svnpropGravatar notin2006-09-12
* Retour à un warning en cas de (co-)fixpoint pas totalement mutuelGravatar herbelin2006-09-09
* Finalement, interdiction des points fixes non totalement mutuellementGravatar herbelin2006-09-06
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
* Extension et réorganisation de l'interprétation des (co-)points fixesGravatar herbelin2006-09-01
* Indentation + typoGravatar notin2006-09-01
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
* Morceau de code mortGravatar herbelin2006-08-24
* Modifications dans les scripts de configuration (coqtop et coqide affichent m...Gravatar notin2006-07-28
* Correction du bug #1116 Gravatar jforest2006-07-20
* Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...Gravatar herbelin2006-07-05
* Ajout d'une option -with-geoproof à la configuration et à l'exécutionGravatar notin2006-06-09
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Réparation coqtop.mlGravatar notin2006-06-07
* Changement de l'option -where: on vérifie si la variable d'environnement COQ...Gravatar notin2006-06-07
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-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
* 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