aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2010-05-04 - Fixing bug #2308 about Lemma ... withvsiles
2010-04-30Fail: a way to check that a command is refused without blocking a scriptletouzey
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Two forgotten $Id$ in last commitletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-27Fix bug #2245, incorrect handling of Context in sections inside modulemsozeau
2010-04-27Added a new exception for already declared Schemes, vsiles
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
2010-04-20missing space in error messagevsiles
2010-04-09Granting wish #2249 (checking existing lemma name also when in a section).herbelin
2010-03-30Small improvements around coqdoc (including fix for bug #2288)herbelin
2010-03-30Improving error messages in the presence of utf-8 charactersherbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-24Fixed bug #2260 (check of resolution of all evars in the declarationherbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-11No delta-reduction in libtypes anymorepuech
2010-03-11Filter out "_subproof" objects from search resultspuech
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
2010-03-05Minor fixes.msozeau
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 01:52:21 +0000