aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2010-01-02Fix bug in last commit, missing a substitution call.msozeau
2010-01-01Fix handling of instance declarations in presence of let-ins (bugmsozeau
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-12-12Fixed incorrect computation of possible guard in presence of `{ ... } contexts.herbelin
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...letouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-25Fix for notation scope & inductive typesvsiles
2009-11-18Now "Include Self <expr>" handles partially applied functors, cf for example ...soubiran
2009-11-18Allow interactive proofs in module typesletouzey
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
2009-11-15Fix [Instance: forall ..., C args := t] declarations to behave asmsozeau
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-09Quick fix for restoring a left-to-right rewriting lemma compatibleherbelin
2009-11-08Fixed "Scheme Equality" when another instance of the scheme on theherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-10-29Hopefully improved layout of fix guardness error message.herbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-10-27Documentation of the Local and Global modifiers.herbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-10-16note for later : when the tag table is shared, never, ever create twovgross
2009-10-13MSets: a new generation of FSetsletouzey
2009-10-09Fix bug #2162 and a name clashing bug in generalized binders.msozeau
2009-10-05Correctly do backtracking during type class resolution even if only newmsozeau
2009-10-05Revert "kills the old backtracking framework and replaces it with"vgross
2009-10-04Changed the way to support compatibility with previous versions.herbelin
2009-10-04Removal of trailing spaces.serpyc
2009-10-03Added option "Unset Dependent Propositions Elimination" to protectherbelin
2009-09-29Add support for Local Declare ML Moduleglondu
2009-09-29Remove legacy export_* functionsglondu
2009-09-29kills the old backtracking framework and replaces it withvgross
2009-09-26Fixed a hole in glob_tactic that allowed some Ltac code to refer toherbelin
2009-09-22Add the option to automatically introduce variables declared before themsozeau
2009-09-17Replace call to where_in_path by find_file_in_path in "Locate File"glondu
2009-09-17Replace unprotected call to where_in_path by find_file_in_pathglondu
2009-09-17Remove useless Liboject.export_function fieldglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:33:56 +0000