aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-04-26Pcoq.ml4: fix a typo in a comment to please ocamldocletouzey
2011-04-26G_vernac can be parsed without grammar.cmaletouzey
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Made warning about ending comments in string less intrusive so as to supportherbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-23- Remove useless grammar rulemsozeau
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-05Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationherbelin
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-25Fix compilation with camlp5 (Closes: #2487)glondu
2011-01-11Add "Print Sorted Universes"glondu
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
2010-12-25Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsglondu
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-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-09Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.herbelin
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
2010-11-18adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6letouzey
2010-11-16Support for camlp5 6.02.0 (Closes: #2432)glondu
2010-10-17About "unsupported" unicode characters in notations.herbelin
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
2010-10-08Export the "bullet" grammar entryglondu
2010-10-06Remove Explain* vernacsglondu
2010-10-06Remove VernacGoglondu
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Making display of various informations about constants more modular:herbelin
2010-10-03Fixed a little printing bug with "About" on an undefined constant.herbelin
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-02Improved printing of Unfoldable constants in hints databases (usedherbelin
2010-07-30r13359 continued: removed native treatment for λ (lambda) and Π (Pi)herbelin
2010-07-29Rather quick hack to make basic unicode notations available byherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 02:04:26 +0000