aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-01-02Fix bug in last commit, missing a substitution call.msozeau
2010-01-01Fix handling of instance declarations in presence of let-ins (bugmsozeau
2009-12-30Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).herbelin
2009-12-30Fixing bug #2156 (non positive occurrence error message displayed "Rel"'s).herbelin
2009-12-30Fixing bug #2193: computation of dependencies in the "match" returnherbelin
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-12-29Renouncing to have the option "Automatic Introduction" on by default.herbelin
2009-12-29Improving descend_in_conjunctions (using a combinators instead of a tactic)herbelin
2009-12-29Fixing precedence while printing patterns in Ltac (was modified in r12607)herbelin
2009-12-28Safer, though ad hoc, approach to re-interpretation of the argument ofherbelin
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-23Moved a bit further the code for pattern interpretation in match goalherbelin
2009-12-22Attached evar source to the evar_info and add location to tclWITHHOLES errorsherbelin
2009-12-21Patches and instructions to enable Input Method support in CoqIDE.vgross
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-21In "progress", extending the set of evars w/o solving an existing one isherbelin
2009-12-20* Rewrite [classify_unicode] using standard unicode tables.regisgia
2009-12-19Backtrack on making exact hints for lemmas starting with productsmsozeau
2009-12-19Made the interpretation levels rlevel/glevel/tlevel truly phantomherbelin
2009-12-18RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndletouzey
2009-12-18Const_omega: look for S in Init only (avoid future clash with S of Numbers)letouzey
2009-12-17ZOdiv: fully use generic properties from ZDivTrunc.vletouzey
2009-12-17Reverse order of arguments in min_case_strong for better uniformity (and comp...letouzey
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. B...letouzey
2009-12-16correction de la nouvelle option pour functional inductionjforest
2009-12-16adding an option functional_induction_rewrite_dependent to make functional in...jforest
2009-12-16Division in Numbers: more properties proved (still W.I.P.)letouzey
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
2009-12-15file integrated into the archive by mistakeletouzey
2009-12-15Description of the new features of the module system (part two).soubiran
2009-12-15Description of the new features of the module system (first part).soubiran
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-12-13Completion of r12580 (better rendering of dependent rewrite and inversion).herbelin
2009-12-13Deactivating printing of {| |} for records when option Printing All is set.herbelin
2009-12-13Fixing bug in printing option as of remember and generalizeherbelin
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
2009-12-12Fixed incorrect computation of possible guard in presence of `{ ... } contexts.herbelin
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-12-12Improved the rendering of "dependent rewrite" and hence of "inversion"herbelin
2009-12-11Deport the backtracking code out of the idevgross
2009-12-10NZDomain: investigation of the shape of NZ domain, more results about ofnat:n...letouzey
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...letouzey
2009-12-08Fix the build of coq via ocamlbuildletouzey
2009-12-08integrate MSetToFiniteSet into the compilation (and fix it)letouzey
2009-12-08Sos.ml: no more warningsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:07:00 +0000