aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Backtrack on activating scopes with type casts (was r15978).Gravatar herbelin2012-12-04
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* Evarconv: Fix #2936 + commentsGravatar pboutill2012-11-28
* Fixed bug #2930: folded let-in's were hiding a violation to the occurGravatar herbelin2012-11-25
* Fixing test-suite: Scope.vGravatar ppedrot2012-11-21
* Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)Gravatar herbelin2012-11-18
* Update output/Search.out after hint-related extra defs in PeanoGravatar letouzey2012-11-17
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
* test-suite: fix grep rule for output testsGravatar pboutill2012-09-04
* test-suite uses coqtop instead of coqtop.byteGravatar pboutill2012-09-04
* In the output tests, ignore dynlink messagesGravatar letouzey2012-08-24
* test-suite: Local Tactic Notation is now legal since r15731Gravatar letouzey2012-08-23
* No more coqtop.opt, produce directly a coqtop binaryGravatar letouzey2012-08-23
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
* Updating headers.Gravatar herbelin2012-08-08
* Fixing #2836 (materialize_evar might refine as a side effect theGravatar herbelin2012-07-29
* Fixing bug #2835 (the rationale for printing notations was notGravatar herbelin2012-07-21
* Improving management of notations with binders (see #2708 where aGravatar herbelin2012-07-21
* Restore test file induct.v where the "in |- *" is mandatoryGravatar letouzey2012-07-10
* Continuing r15459: it helps testing occur-check early in someGravatar herbelin2012-07-06
* Minor fixes in the test-suite after my recent commitsGravatar letouzey2012-07-06
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Fixing bug #2809 (anomaly when printing a module with notations due toGravatar herbelin2012-06-20
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
* Constrextern is allow to use partially applied notationsGravatar pboutill2012-06-14
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
* Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.Gravatar ppedrot2012-06-12
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
* Implicit arguments of Definition are taken from the type when given by the user.Gravatar pboutill2012-04-27
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* Bug 2733 : { } implicits and FixpointsGravatar pboutill2012-04-17
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Repair two testsGravatar letouzey2012-04-12
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* Relax uniform inheritance conditionGravatar gareuselesinge2012-04-05
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
* evarconv: MaybeFlex/MaybeFlex case infers more Canonical StructuresGravatar gareuselesinge2012-03-22
* Fixing bug #2724 (using notations with binders in cases patternsGravatar herbelin2012-03-20
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02