aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-10-26Coq_makefile handles .mlpack filespboutill
2011-10-26Coqdep handles .mlpackpboutill
2011-10-26Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)letouzey
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
2011-10-26Environ.set_universes is dead codeletouzey
2011-10-26Mod_subst: some simplifications, some more significant names to functions, etcletouzey
2011-10-26Auto: avoid storing clausenv (and hence env, evar_map, universes) in voletouzey
2011-10-26Makefile install rule fixpboutill
2011-10-26Coq_makefile includes coqtop -config without file generationpboutill
2011-10-26 Coq_makefile: libraries in bytecode are now installed toopboutill
2011-10-26Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).herbelin
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
2011-10-25Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).herbelin
2011-10-25Regression tests for bugs #2613 and #2616.herbelin
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-25Coq_makefile: a more complete commentary about global variablespboutill
2011-10-25Coq_makefile does not install/compile explicitely cmo and cmxs? that are in a...pboutill
2011-10-25coqdep defines a makefile variable name_MLLIB_DEPENDENCIES to store dependenc...pboutill
2011-10-25Fixing use of type constraint for refining the "return" clause of "match".herbelin
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
2011-10-25Fixing "destruct" test.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 10:04:02 +0000