aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-10-25Continuing r1492 (useless changes were inadvertantly committed)herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-25Still more unification in typing.mlherbelin
2011-10-25Icons in CoqIdE preference panelpboutill
2011-10-25Configuration window of CoqIdE looks more like other Gtk one.pboutill
2011-10-24Heads: avoid potentially uncaught Not_found via an assert falseletouzey
2011-10-24Mod_subst: Attempt to fix #2608letouzey
2011-10-24More unification in type_of and addition of e_type_of to get the newherbelin
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
2011-10-24Fixing failing printer when the type of a binder name with implicitherbelin
2011-10-22Fail if some conv pbs remain after consider_remaining_unif_problems.herbelin
2011-10-22Now consider remaining conversion problems in solve_remaining_evars.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 19:40:06 +0000