aboutsummaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
AgeCommit message (Expand)Author
2013-01-27Fixed bug #2967 (some missing check on ill-formed recursive notation strings).herbelin
2012-12-14Modulification of identifierppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-06still some more dead code removalletouzey
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-18Cleaning interface of Util.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-04Replacing some str with strbrkppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:11:30 +0000