aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2012-10-17Fix test-suite output/* in benchpboutill
2012-09-04test-suite: fix grep rule for output testspboutill
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
2012-08-24In the output tests, ignore dynlink messagesletouzey
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
2012-07-21Fixing bug #2835 (the rationale for printing notations was notherbelin
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
2012-07-10Restore test file induct.v where the "in |- *" is mandatoryletouzey
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
2012-07-06Minor fixes in the test-suite after my recent commitsletouzey
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-06-20Fixing bug #2809 (anomaly when printing a module with notations due toherbelin
2012-06-18Proof using: nested sections bugfixgareuselesinge
2012-06-14Constrextern is allow to use partially applied notationspboutill
2012-06-12Fixing test-suite after last storm in Pp.pboutill
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-04-27Implicit arguments of Definition are taken from the type when given by the user.pboutill
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2012-04-17Bug 2733 : { } implicits and Fixpointspboutill
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-12Repair two testsletouzey
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-04-05Relax uniform inheritance conditiongareuselesinge
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
2012-03-23Fix the test-suite by removing any Reset in the scriptsletouzey
2012-03-22evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structuresgareuselesinge
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-03-02Noise for nothingpboutill
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-02-14Arguments supports extra notation scopesgareuselesinge
2012-01-31Fix consequence of pp bugfix in testsuitepboutill
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2012-01-20Notations with binders: Accepting using notations for functional termsherbelin
2012-01-16Parameters in pattern first step.pboutill
2012-01-14Add distclean back to test-suite/Makefileglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:24:04 +0000