| Commit message (Expand) | Author | Age |
* | Fixed a hole in glob_tactic that allowed some Ltac code to refer to | herbelin | 2009-09-26 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |
* | Timeout message was not always displayed | barras | 2009-03-04 |
* | Correction de bugs: | herbelin | 2008-08-05 |
* | Évolutions diverses et variées. | herbelin | 2008-08-04 |
* | Autour du parsing: | herbelin | 2008-07-15 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
* | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
* | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin | 2007-09-30 |
* | Contrôle de la compatibilité de apply via une information dans les | herbelin | 2007-05-28 |
* | Documentation de "Set Printing Universes", "Print Universes" (anciennement | herbelin | 2006-10-28 |
* | improve the amount of information given by the Ltac tactic debugger | bertot | 2006-08-28 |
* | Amélioration des messages d'erreurs de tacred; unfold considère maintenant le | herbelin | 2006-02-07 |
* | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin | 2006-01-21 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ... | herbelin | 2005-12-17 |
* | Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ... | herbelin | 2005-12-17 |
* | Abstraction vis à vis du type loc pour compatibilité ocaml 3.08 | herbelin | 2004-07-16 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Adaptation a la v7 du message d'erreur Match_failure | herbelin | 2004-03-16 |
* | search window | coq | 2004-02-04 |
* | Affichage Assert_failure en ocaml 3.07 | herbelin | 2003-10-28 |
* | Ajout d'un message à FailTac | herbelin | 2003-03-31 |
* | Debugger plus informatif | delahaye | 2003-02-13 |
* | msg Failtac; echec -batch s'il reste des preuves | filliatr | 2003-01-17 |
* | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
* | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | resolution du pb d'efficacite du a Sign.add_named_decl | barras | 2002-04-04 |
* | Bug d'affichage des erreurs localisées dans un fichier suite à | herbelin | 2002-03-27 |
* | Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce | ddr | 2002-02-20 |