aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Catch a Not_found exception in the Combined Scheme mechanism to hide an uglyGravatar vsiles2008-06-24
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix bug #1889, correct globalization in class declarations.Gravatar msozeau2008-06-21
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* 2-3 petites modifs pour la compilation sous Windows...Gravatar notin2008-06-06
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* Fix globalization bug in class_tactics and refactorize instanceGravatar msozeau2008-05-19
* - Fix bug related to indices of fixpoints.Gravatar msozeau2008-05-13
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-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
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Integration of theories/Ints into theories/Numbers, part 3: fixing forgotten ...Gravatar letouzey2008-05-07
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* 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
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Fix bug #1844, generalize implementation to handle and combination ofGravatar msozeau2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Added frozen state after each command.Gravatar courtieu2008-04-23
* Bug squashing day !Gravatar msozeau2008-04-17
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Check that no evars remain in instance types earlier at InstanceGravatar msozeau2008-04-11
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02