aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...Gravatar letouzey2008-12-17
* Take advantage of natdynlink when available: almost all contribs become loada...Gravatar letouzey2008-12-16
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* About "apply in":Gravatar herbelin2008-12-09
* Correct handling of defined methods (let-ins) in instance declarations.Gravatar msozeau2008-12-04
* Inductive parameters: nicer doc examples and error messageGravatar letouzey2008-11-28
* - Synchronized subst_object with load_object (load_and_subst_objects)Gravatar herbelin2008-11-23
* Minor improvement to commit 11619Gravatar herbelin2008-11-23
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* Tentative d'amélioration de la robustesse des Makefile générés parGravatar notin2008-11-13
* Fix mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Petit bug dans le commit précédent.Gravatar aspiwack2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Remove calls to Dynlink.add_{interfaces,available_units} altogetherGravatar glondu2008-10-29
* Native "Declare ML Module" when possibleGravatar glondu2008-10-28
* 11511 continued (bug in set.out + incohérence dans "Theorem with"Gravatar herbelin2008-10-28
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* - MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)Gravatar herbelin2008-10-26
* Raise informative errors instead of Failures or anomalies in case a metaGravatar msozeau2008-10-24
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Fix bugs #1975 and #1976.Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Fix bug #1959 (remember: never use a partial functions mindlessly).Gravatar msozeau2008-10-08
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
* Fix bug #1936: uncaught exception due to undefinable exceptions.Gravatar msozeau2008-09-14
* Fix bug #1940: uncaught exception when searching for a type class.Gravatar msozeau2008-09-14
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Various fixes w.r.t typeclasses and subtac: resolve tcs properly insideGravatar msozeau2008-08-21
* eviter redondance du message d'erreur (Error while reading / File)Gravatar barras2008-08-07
* Correction de bugs:Gravatar herbelin2008-08-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 01:35:14 +0000