aboutsummaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
AgeCommit message (Expand)Author
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-20Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicherbelin
2012-03-02Noise for nothingpboutill
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-08-23Clarifying that only identifiers are advertised to be turned into keywordsherbelin
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-10-17About "unsupported" unicode characters in notations.herbelin
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2009-11-25Fix for notation scope & inductive typesvsiles
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-29Remove legacy export_* functionsglondu
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-14- Addition of "Reserved Infix" continued.herbelin
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-11Add support for "Infix ... := constr" instead of just "Infix ... := ref".herbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-14Fixing #1960 (xml bug with external on goal variable) and #1961herbelin
2008-10-26- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)herbelin
2008-10-22Affichage des notations récursives:herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-08-05Correction de bugs:herbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:07:52 +0000