aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
2008-11-07Slight change of the semantics of user-given casts: they don't reallymsozeau
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-11-05Petit bug dans le commit précédent.aspiwack
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-10-29Remove calls to Dynlink.add_{interfaces,available_units} altogetherglondu
2008-10-28Native "Declare ML Module" when possibleglondu
2008-10-2811511 continued (bug in set.out + incohérence dans "Theorem with"herbelin
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-10-26- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)herbelin
2008-10-24Raise informative errors instead of Failures or anomalies in case a metamsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22Fix bugs #1975 and #1976.msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-10-08Fix bug #1959 (remember: never use a partial functions mindlessly).msozeau
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-09-15Fix bug #1943 and restrict the inference optimisation of Program tomsozeau
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-09-14In manual implicit arguments mode, do not enrich implicitsmsozeau
2008-09-14Fix bug #1936: uncaught exception due to undefinable exceptions.msozeau
2008-09-14Fix bug #1940: uncaught exception when searching for a type class.msozeau
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
2008-09-07Add the ability to declare [Hint Extern]'s with no pattern.msozeau
2008-09-07Fixes in typeclasses resolution. Avoid reducing instances types beforemsozeau
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-08-21Various fixes w.r.t typeclasses and subtac: resolve tcs properly insidemsozeau
2008-08-07eviter redondance du message d'erreur (Error while reading / File)barras
2008-08-05Correction de bugs:herbelin
2008-08-04Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parherbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-28Fixes in generalize_eqs/dependent induction to allow the user to specifymsozeau
2008-07-26- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecherbelin
2008-07-25Fixed bug #1904 (instances of evars were no longer substituted sinceherbelin
2008-07-24Fix bug #1913, checking for unresolved evars which aren't obligations.msozeau
2008-07-24Suite commit 11236notin
2008-07-23Stop glob messages to be printed by default on stdout letouzey
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-21Suite commit 11236notin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-07-18Affichage intempestif d'information de globalisation + numéro de version dan...notin
2008-07-17fixed indentation of subgoals for Show Scriptbarras
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-15Autour du parsing:herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:25:23 +0000