aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).Gravatar herbelin2010-07-18
* Finish adding out-of-the-box support for camlp4Gravatar letouzey2010-07-09
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* A new command Compute foo, shortcut for Eval vm_compute in fooGravatar letouzey2010-06-04
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Missing warning flush in a lexer message + update of CHANGESGravatar herbelin2010-05-12
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Removed obsolete v7->v8 translation code (function check_same_type isGravatar herbelin2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
* Improving error messages in the presence of utf-8 charactersGravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* Fixes in rewrite and a Elimination/Case to Scheme:Gravatar msozeau2010-03-06
* Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)Gravatar letouzey2010-03-04
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* g_decl_mode: 'by' is now a keywordGravatar letouzey2010-01-12
* * Segmenttree: New. A very simple implementation of segment trees.Gravatar regisgia2010-01-08
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...Gravatar letouzey2010-01-06
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* Fixing precedence while printing patterns in Ltac (was modified in r12607)Gravatar herbelin2009-12-29
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* * Rewrite [classify_unicode] using standard unicode tables.Gravatar regisgia2009-12-20
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
* Deactivating printing of {| |} for records when option Printing All is set.Gravatar herbelin2009-12-13
* Fixing bug in printing option as of remember and generalizeGravatar herbelin2009-12-13
* Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...Gravatar letouzey2009-12-08
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 13:06:05 +0000