aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* fixed minor pbs with test casesGravatar barras2010-03-12
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* ajout test de fied_simplify_eq inGravatar barras2010-02-10
* New version of 12650 that was broken (supporting again records whenGravatar herbelin2010-01-12
* revert commit 12650 for the moment, since it breaks MSetAVLGravatar letouzey2010-01-12
* Temporary fix to compensate the loss of descent on dependentGravatar herbelin2010-01-12
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* Renouncing to have the option "Automatic Introduction" on by default.Gravatar herbelin2009-12-29
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
* Fix test-suite scripts: [Generalizable Variables] and small Gravatar msozeau2009-11-13
* Test for bug #2168, forgotten in r12496.Gravatar herbelin2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Attempt to capture on time unification errors for "with" bindings.Gravatar herbelin2009-10-30
* Revision 12439 continued, printing part (notations to names behaveGravatar herbelin2009-10-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
* Adapted test unfold.v after eq gets its argument maximally insertedGravatar herbelin2009-10-26
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Fixed a bug in the interaction between dEqThen and inject_at_positionsGravatar herbelin2009-09-27
* Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.Gravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Add the option to automatically introduce variables declared before theGravatar msozeau2009-09-22
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-10 09:12:59 +0000