aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
2008-06-03Fix setoid_rewrite documentation examples.msozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
2008-05-22Strategy commands are now exportedbarras
2008-05-21refined the conversion oraclebarras
2008-05-19Fix globalization bug in class_tactics and refactorize instancemsozeau
2008-05-13- Fix bug related to indices of fixpoints.msozeau
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-10Correction bug #1842 + correction bug initialisation introduit dansherbelin
2008-05-10- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desherbelin
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
2008-05-07Integration of theories/Ints into theories/Numbers, part 3: fixing forgotten ...letouzey
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-05-05More emacs-friendly error messages.glondu
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-27Quelques bricoles autour de l'unification:herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-24Fix bug #1844, generalize implementation to handle and combination ofmsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-23Added frozen state after each command.courtieu
2008-04-17Bug squashing day !msozeau
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-11Check that no evars remain in instance types earlier at Instancemsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-27Various fixes on typeclasses:msozeau
2008-03-24Finish fix in command where we still lost information on what was a typemsozeau
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
2008-03-21Correct bug introduced in r10589, where we lost information thatmsozeau
2008-03-19some references to IntMap forgotten in last commitletouzey
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-03-18* Small change in the make_eq_decidability call : the functions does not (yet)vsiles
2008-03-17* Factorizing code : context_chop was used in several files (even as chop_con...vsiles
2008-03-15Do a second pass on the treatment of user-given implicit arguments. Nowmsozeau
2008-03-13fix the 'decreasing on Xth' messageletouzey
2008-03-12* Catching a Not_found exception when trying to use Scheme Equality vsiles
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau