aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.ml
AgeCommit message (Expand)Author
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-02-12fix last commit about modules (subst_cl_typ may raise Not_found)letouzey
2011-02-11An automatic substitution of scope at functor applicationletouzey
2011-02-11Annotations at functor applications:letouzey
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-09-24Partial review of removed dead code (r13460)herbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-06-08Fixed wrong spelling in a warning.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2009-11-02list, length, app are migrated from List to Datatypesletouzey
2009-10-26Local/Global revision 12418 continuedherbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-30Fix a small notation/scope bug:vsiles
2009-02-06pushed evar reduction in kernelbarras
2008-10-22Affichage des notations récursives:herbelin
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-05-07Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757herbelin
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-05-10Prise en compte réversibilité des notations de la forme "Notation Nil := @n...herbelin
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2007-01-10Suite commit restructuration discharge (application du type deherbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-10-23Add a flush for a warning.courtieu
2006-10-06Annulation de l'essai de changement de sémantique du %scope (révision 9208).herbelin
2006-10-05Essai de changement de sémantique du %scope : herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:11:39 +0000