aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
2011-11-18Fix parsing of :>> and backtrack correctly on the cache of hints for local co...msozeau
2011-11-18Return of the tactic hints features in CoqIDE.ppedrot
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-18Added a printing function to handle single evarsppedrot
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in C...ppedrot
2011-11-18Coqide -debug only printed Coqtop information.pboutill
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-18Fix for subclasses implementation, allowing to register generalized classes s...msozeau
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-17Merge fix for bug #2604.msozeau
2011-11-17Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-17Was missing a potential application of subtypingmsozeau
2011-11-16Adding postprocessing to remove "commutative cuts" expansions inherbelin
2011-11-16Changed the way find_dependencies_signature is working so that itherbelin
2011-11-16De Bruijn indices bug in pattern matching compilation in the presenceherbelin
2011-11-16Old generalization bug in pattern-matching: names were considered theherbelin
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
2011-11-16Old typing bug in pattern-matching compilation (apparently w/oherbelin
2011-11-16Specialization of tomatch in pattern-matching compilation was done tooherbelin
2011-11-16A bit of documentation around cases.ml + ML modules uselessly openherbelin
2011-11-16Completed list of theories targetsherbelin
2011-11-16Suppression fichier Case8.v redondantherbelin
2011-11-16Fixing beautification of "thm_token" (missing space) + improvements.herbelin
2011-11-16Fixing association of wrong "as"-pattern name when expandingherbelin
2011-11-16Fixing dependencies lifting bug in pattern-matching compilationherbelin
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-09Fixed ocamlbuild compilation (Tom Prince)ppedrot
2011-11-08Refined second_order_matching so that a constraint on whichherbelin
2011-11-08optimization: memoization for is_open_canonical_projectiongareuselesinge
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-11-07Fixed xml-light handling of whitespace not compliant with XML standard: it st...ppedrot
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
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-06Added XML dependencies into Makefileppedrot
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-04Auto: removal of ?use_core_db obsolete now that we have nocoreletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 13:22:32 +0000