aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Term: Refactoring of hashconsingGravatar puech2011-07-29
* Oversight in revision 14292.Gravatar pboutill2011-07-27
* Partial revert of r14292Gravatar pboutill2011-07-26
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
* Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.Gravatar courtieu2011-07-05
* Revert "Check if recursive calls are guarded before printing "Proof completed"."Gravatar pboutill2011-06-10
* Check if recursive calls are guarded before printing "Proof completed".Gravatar herbelin2011-05-26
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
* Restore display of notation when printing an inductive such as sigGravatar letouzey2011-05-21
* Break circular dependency Proof_global -> Vernacexpr -> Proof_global.Gravatar aspiwack2011-05-17
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* New option [Set Bullet Behavior] allows to select the behaviour of bullets.Gravatar aspiwack2011-05-13
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Pcoq.ml4: fix a typo in a comment to please ocamldocGravatar letouzey2011-04-26
* G_vernac can be parsed without grammar.cmaGravatar letouzey2011-04-26
* Fixing bug in printing let-in binders in fix/cofixGravatar herbelin2011-04-24
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Made warning about ending comments in string less intrusive so as to supportGravatar herbelin2011-04-08
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
* Add 'Existing Instances' declaration to declare multiple instances at once.Gravatar letouzey2011-04-06
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* - Remove useless grammar ruleGravatar msozeau2011-03-23
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationGravatar herbelin2011-03-05
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* Annotations at functor applications:Gravatar letouzey2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Fix compilation with camlp5 (Closes: #2487)Gravatar glondu2011-01-25
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
* Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsGravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.Gravatar herbelin2010-12-09
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
* adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6Gravatar letouzey2010-11-18
* Support for camlp5 6.02.0 (Closes: #2432)Gravatar glondu2010-11-16
* About "unsupported" unicode characters in notations.Gravatar herbelin2010-10-17
* Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingGravatar herbelin2010-10-11
* Export the "bullet" grammar entryGravatar glondu2010-10-08
* Remove Explain* vernacsGravatar glondu2010-10-06
* Remove VernacGoGravatar glondu2010-10-06
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03