aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2010-06-03Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4letouzey
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
2010-06-01restore handling of lexer errorsletouzey
2010-05-31CoqIDE goes multiprocessvgross
2010-05-31More indirection.vgross
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2010-05-31Modifying startup sequencevgross
2010-05-29New pass on inductive schemesherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:54:08 +0000