aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppvernac.ml
AgeCommit message (Expand)Author
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29Extend become a mli-only file in intf/letouzey
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2012-03-30Added a command "Unfocused" which returns an error when the proof isaspiwack
2012-03-30Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclletouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-23Remove undocumented command "Delete foo"letouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-21Ppvernac: nicer printing of proof delimiters { ... }letouzey
2012-03-02Noise for nothingpboutill
2012-02-14Arguments supports extra notation scopesgareuselesinge
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