aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
2011-10-10Fixing buggy abberant code for Evarutil.expand_evarherbelin
2011-10-10Little code simplification of instantiate_evar in evd.mlherbelin
2011-10-10Added information about evar origin in pretty-printing evd for debugherbelin
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
2011-10-10Proper fix for complement/flip instances.msozeau
2011-10-09mainbiblio.bib : get rid of merge marker from failed mergeletouzey
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
2011-10-08Rely on kernel to know if a name is already used so as to be consistent with it.herbelin
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ...msozeau
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-10-07ocamlbuild: remove -dllpath from coqrunbyteflagsglondu
2011-10-07ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.glondu
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-10-05When a pattern match, don't use the first matching term but anherbelin
2011-10-05Removing vernacular code mistakenly committed.herbelin
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
2011-10-05Force dependency of Reference-Manual.pdf over Reference-Manual.dviherbelin
2011-10-05Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...letouzey
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-10-02Hash-consing of constr could share moreletouzey
2011-10-01Updating some links in the FAQherbelin
2011-10-01Moving never-used comments from Zhints.v to dev/doc so as not toherbelin
2011-10-01Fixing critical part of bug #2504. Not all inductive types in Type areherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 11:17:35 +0000