aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* 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
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Misc fixes.Gravatar msozeau2009-11-06
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Module type expressions of the form (Fsig X) with Definition foo := bar are n...Gravatar soubiran2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 11:14:14 +0000