aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2011-11-18Added hint support in the API. You can now query a goal to see the tactics th...ppedrot
2011-11-18Toplevel loop is a bit more robust: it catches bad API queries.ppedrot
2011-11-18Making status info better in CoqIDE: path and name of current lemmappedrot
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. Answer...ppedrot
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in C...ppedrot
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-14Bug 2637: patches to make slightly easier to write programs that use coq code...pboutill
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-11-07Fixed xml-light handling of whitespace not compliant with XML standard: it st...ppedrot
2011-11-06Also sprach CoqIDE (in XML)ppedrot
2011-11-06Fixed nasty bug when empty PCData, confusion no string vs. empty stringppedrot
2011-11-06More XML marshalling functionsppedrot
2011-11-06Partialliy added XML marshalling to ide_intfppedrot
2011-11-06Added XML manipulation tools to compilation chainppedrot
2011-11-06Added XML manipulation basics (modified from xml-light)ppedrot
2011-11-05Added missing printing debug functions in IDE interfaceppedrot
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-29Added checksums to glob files and warned about possibly missingherbelin
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-10-01Fixing critical part of bug #2504. Not all inductive types in Type areherbelin
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-09-05Coqide: new backtracking code, based on the Backtrack commandletouzey
2011-09-05Ide_intf: slight reorganisation of the IDE apiletouzey
2011-09-05Lib.node: merge OpenedModtype and OpenedModule, same for Closed...letouzey
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-08-30Quick improvement of some error messages related to module applicationherbelin
2011-08-23Clarifying that only identifiers are advertised to be turned into keywordsherbelin
2011-08-18Misc improvements concerning "Show Match" and its coqide equivalentletouzey
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-08-10Improving error message about coinductive guard (old "cases" is now "match")herbelin
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
2011-08-09Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...aspiwack
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
2011-08-03Fix nf_evars_undefined use in pr_constraintsmsozeau
2011-07-29Class: generic equality on constr replaced by destructorspuech
2011-07-28Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)letouzey
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-06-30Keep obligation source information in Programmsozeau
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-20Add compatibility option "-compat 8.3".herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 19:32:48 +0000