aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Amélioration de la colorisation, du backtrack et des messages de CoqIDEGravatar herbelin2008-05-10
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
* Still Ints-->Numbers transition: fix the previous commit about a typoGravatar letouzey2008-05-09
* Still Ints-->Numbers transition: fix a typo preventing the compilation of BigQGravatar letouzey2008-05-08
* Autre oubli de la révision 10904Gravatar herbelin2008-05-08
* remove mention of an obsolete limitation of Add MorphismGravatar letouzey2008-05-08
* Oups, my new version of NMake_gen.ml was relying on a 3.10 feature:Gravatar letouzey2008-05-08
* Suite 10904 (fichiers oubliés)Gravatar herbelin2008-05-08
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Integration of theories/Ints into theories/Numbers, again : better generation...Gravatar letouzey2008-05-08
* Integration of theories/Ints into theories/Numbers, part 3: auto-generation o...Gravatar letouzey2008-05-08
* Integration of theories/Ints into theories/Numbers, part 3: fixing forgotten ...Gravatar letouzey2008-05-07
* Integration of theories/Ints into theories/Numbers, part 2: removing theories...Gravatar letouzey2008-05-07
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
* fixed bug with aliasesGravatar barras2008-05-07
* export Extract_env.mono_environment in the mli Gravatar letouzey2008-05-07
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* checker deals with polymorphic constants and module aliasesGravatar barras2008-05-06
* [ring] constructor for power was missing in the docGravatar barras2008-05-06
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Backtrack commit 10887 (priorité des notations pour les signatures deGravatar notin2008-05-05
* It seems more natural to put those operators at same level as "->"...Gravatar glondu2008-05-05
* Minor updates in the documentation of notations.Gravatar glondu2008-05-05
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* More emacs-friendly error messages.Gravatar glondu2008-05-05
* Factorize code for internalization of binders to fix bug #1846. AlsoGravatar msozeau2008-05-04
* Quelques éléments de réflexionGravatar herbelin2008-05-03
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
* Calcul plus robuste du numéro de révision (ne marche en positionnantGravatar herbelin2008-04-29
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* Suppression de la partie ML de la contrib correctness. Les fichiersGravatar herbelin2008-04-29
* Correction d'un bug dans coq_makefile: génération des règles implicites en...Gravatar notin2008-04-29
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
* reparation bug de compil introduit au precedent commitGravatar jforest2008-04-28
* menage dans funind + deplaceemnt de recdef dans funindGravatar jforest2008-04-28
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Suite commit 10861Gravatar herbelin2008-04-28
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27