aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
...
* 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
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...Gravatar barras2009-03-19
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* From v8.2 to trunk:Gravatar herbelin2009-02-06
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fix for syntax changes in test-suite scripts.Gravatar msozeau2008-12-16
* About "apply in":Gravatar herbelin2008-12-09
* improved simplGravatar barras2008-12-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 07:45:08 +0000