aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
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
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-12g_decl_mode: 'by' is now a keywordletouzey
2010-01-08* Segmenttree: New. A very simple implementation of segment trees.regisgia
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-06"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...letouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-12-29Fixing precedence while printing patterns in Ltac (was modified in r12607)herbelin
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-20* Rewrite [classify_unicode] using standard unicode tables.regisgia
2009-12-19Made the interpretation levels rlevel/glevel/tlevel truly phantomherbelin
2009-12-13Deactivating printing of {| |} for records when option Printing All is set.herbelin
2009-12-13Fixing bug in printing option as of remember and generalizeherbelin
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...letouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 13:54:25 +0000