aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-10-22Use also second-order unification if first-order fails at the time of conside...herbelin
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
2011-10-22Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...herbelin
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
2011-10-20More descriptive error messages in checkerglondu
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
2011-10-18Fix bug #2227msozeau
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
2011-10-17Revert "New evar_map printer ppevmfull which can typically be installed for"herbelin
2011-10-17Partly reverting r14539 about fully expanding "let-in"s and not justherbelin
2011-10-17New evar_map printer ppevmfull which can typically be installed forherbelin
2011-10-17Patch by Dan Grayson to ensure that "Add LoadPath ... as ..." closesherbelin
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...msozeau
2011-10-15dev/base_include: display a nice message at the end of the loadletouzey
2011-10-15debugging.txt: no more typing of #use "include" if using .ocamlinitletouzey
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
2011-10-12Temporary revert commit 14550 since it breaks a few contribsletouzey
2011-10-12Patch to support (a priori) all versions of make 3.xx >= 3.81herbelin
2011-10-12test-suite: non-regression test for bug #2603letouzey
2011-10-11Added test for bug #2615herbelin
2011-10-11Safe_typing: adding a inductive block adds many labels (fix #2603)letouzey
2011-10-11Names : check of labels, cleanup, nicer debug display of kn and constantletouzey
2011-10-11Mod_subst: an unused functionletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 05:50:51 +0000