aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Fixing a regression wrt 8.2 when using an "ident" several times in a notationGravatar herbelin2010-11-04
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* Cleaning the use of parentheses around evd and evdref (cosmetic commit).Gravatar herbelin2010-10-31
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Partial review of removed dead code (r13460)Gravatar herbelin2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
* Bugfix: A notation for a constructor where some arguments are _Gravatar pboutill2010-09-10
* Fixed a bug introduced (r13316/r13329) in the printing of notationsGravatar herbelin2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Constrintern: Moved section about binders before section about notationGravatar herbelin2010-07-22
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Fixed wrong spelling in a warning.Gravatar herbelin2010-06-08
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Fix bug 2307Gravatar pboutill2010-05-20
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* 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
* Fixed some printing bugs.Gravatar herbelin2010-04-18
* Optimized need for delimiters when disjoint scopes for strings andGravatar herbelin2010-04-10
* Partially fixed bug #2231 (an inductive parameter name was internallyGravatar herbelin2010-04-10
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Fix implicit_application for let-bound variables in the class context.Gravatar msozeau2010-01-28
* Backport fixes in Instance declarations to Program Instance.Gravatar msozeau2010-01-28
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Allowed handling of partly-applied record constructors. (Fix for bug #2196.)Gravatar gmelquio2010-01-06
* 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
* 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
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 16:15:47 +0000