aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Fix bug #2245, incorrect handling of Context in sections inside moduleGravatar msozeau2010-04-27
* Added a new exception for already declared Schemes, Gravatar vsiles2010-04-27
* 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
* missing space in error messageGravatar vsiles2010-04-20
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
* Small improvements around coqdoc (including fix for bug #2288)Gravatar herbelin2010-03-30
* Improving error messages in the presence of utf-8 charactersGravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Fixed bug #2260 (check of resolution of all evars in the declarationGravatar herbelin2010-03-24
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
* No delta-reduction in libtypes anymoreGravatar puech2010-03-11
* Filter out "_subproof" objects from search resultsGravatar puech2010-03-11
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
* Fixes in rewrite and a Elimination/Case to Scheme:Gravatar msozeau2010-03-06
* Minor fixes.Gravatar msozeau2010-03-05
* Delineating a API for Coq inside toplevel/vernac.mlGravatar vgross2010-02-12
* 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
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Fix bug in last commit, missing a substitution call.Gravatar msozeau2010-01-02
* Fix handling of instance declarations in presence of let-ins (bugGravatar msozeau2010-01-01
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* 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
* Fix for notation scope & inductive typesGravatar vsiles2009-11-25
* Now "Include Self <expr>" handles partially applied functors, cf for example ...Gravatar soubiran2009-11-18
* Allow interactive proofs in module typesGravatar letouzey2009-11-18
* 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
* Fix [Instance: forall ..., C args := t] declarations to behave asGravatar msozeau2009-11-15
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* 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
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
* Fixed "Scheme Equality" when another instance of the scheme on theGravatar herbelin2009-11-08
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Hopefully improved layout of fix guardness error message.Gravatar herbelin2009-10-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 16:49:31 +0000