aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppvernac.ml
AgeCommit message (Expand)Author
2012-01-23Removed a seemingly unused argument in Require of modules, introduced 10 year...ppedrot
2012-01-23Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.ppedrot
2012-01-20Fix printing of classesmsozeau
2012-01-17Fixed the pretty-printing of the Program plugin.ppedrot
2012-01-17Some fix in beautify pretty-printerpboutill
2012-01-10Fix printing of instances, generalized arguments.msozeau
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-12Proof using ...gareuselesinge
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-16Fixing beautification of "thm_token" (missing space) + improvements.herbelin
2011-09-15Names.make_mbid and co : convert from/to identifier (avoid some String.copy)letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-08-30Quick improvement of some error messages related to module applicationherbelin
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-02-11Annotations at functor applications:letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-11Add "Print Sorted Universes"glondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-10-06Remove Explain* vernacsglondu
2010-10-06Remove VernacGoglondu
2010-10-03Added multiple implicit arguments rules per name.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-03Added command "Locate Ltac qid".herbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-30Fail: a way to check that a command is refused without blocking a scriptletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-26Misc small fixes : warning, dep cycles, ocamlbuild...letouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey