aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* 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
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Deactivation of (intrusive) printing of abbreviations from non-imported modules.Gravatar herbelin2009-11-09
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* Misc fixes.Gravatar msozeau2009-11-06
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
* Revision 12439 continued, printing part (notations to names behaveGravatar herbelin2009-10-29
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
* Fixed a bug when reporting unexisting reference to an inductiveGravatar herbelin2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 10:12:40 +0000