aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-10-11in heads.ml, at least turn the Not_found of #2608 into assert falseletouzey
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-10-11Unification in the return clause of match was not supported in solve_evars.herbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-10Hash-consing of mutual_inductive_body (and Univ.constraints)letouzey
2011-10-10Avoid some re-allocation during hash-cons of dir_pathletouzey
2011-10-10Hash-cons the statically allocated Rels (1 to 16) to themselvesletouzey
2011-10-10Hashtbl_alt : typo in a commentletouzey
2011-10-10Hash-cons of constr : avoid some useless allocationsletouzey
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 12:28:28 +0000