aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-11-03Cleaning a little bit the files talking about descriptions: avoidingherbelin
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-29Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).herbelin
2011-10-29Fixed broken globalization of identifiers containing utf8 lettersherbelin
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-27Remove avoidable use of GDynamicglondu
2011-10-26Deactivating second-order pattern-matching in evarconv for 8.4.herbelin
2011-10-26Fix configuration box bug in recursive callpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:02:42 +0000