aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
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
2010-07-18Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).herbelin
2010-07-09Finish adding out-of-the-box support for camlp4letouzey
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-08Using vernac parsing for Functionjforest
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-04A new command Compute foo, shortcut for Eval vm_compute in fooletouzey
2010-06-03Added command "Locate Ltac qid".herbelin
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2010-05-12Missing warning flush in a lexer message + update of CHANGESherbelin
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-29Removed obsolete v7->v8 translation code (function check_same_type isherbelin
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
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-30Improving error messages in the presence of utf-8 charactersherbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
2010-03-04Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)letouzey
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 03:36:21 +0000