aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Finish fix in command where we still lost information on what was a typeGravatar msozeau2008-03-24
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Correct bug introduced in r10589, where we lost information thatGravatar msozeau2008-03-21
* some references to IntMap forgotten in last commitGravatar letouzey2008-03-19
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* * Small change in the make_eq_decidability call : the functions does not (yet)Gravatar vsiles2008-03-18
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* fix the 'decreasing on Xth' messageGravatar letouzey2008-03-13
* * Catching a Not_found exception when trying to use Scheme Equality Gravatar vsiles2008-03-12
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* New instance returns the (future) identifier of the instance.Gravatar msozeau2008-02-26
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09