aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Documentation of the Local and Global modifiers.Gravatar herbelin2009-10-27
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
* Revert "kills the old backtracking framework and replaces it with"Gravatar vgross2009-10-05
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Added option "Unset Dependent Propositions Elimination" to protectGravatar herbelin2009-10-03
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
* Remove legacy export_* functionsGravatar glondu2009-09-29
* kills the old backtracking framework and replaces it withGravatar vgross2009-09-29
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Add the option to automatically introduce variables declared before theGravatar msozeau2009-09-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 11:30:45 +0000