aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2014-03-26test for apply + TC resolutionEnrico Tassi
2014-02-28Pos.compare_cont takes the comparison as first argumentPierre Boutillier
2014-01-06Add a test suite file for Ltac's "+" tactical.Arnaud Spiwack
2013-12-06Remove duplicate test-suite file.Arnaud Spiwack
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-09-03Fixing some tests from the test-suite.ppedrot
2013-09-02* test-suite/success/Unicode_utf8:regisgia
2013-07-17More dynamic argument scopesletouzey
2013-07-10Continuing r16621 on injection intro-patterns:herbelin
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-10Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...msozeau
2013-06-02Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anherbelin
2013-05-14Fixing a regression in unification introduced in r16205 (error raisedherbelin
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
2013-05-08Share more information between constructors and arity of an inductiveherbelin
2013-05-08Moved isolated test params_ind.v to Inductive.v.herbelin
2013-05-05Hack to solve a "Bad recursive type" anomaly.herbelin
2013-03-21Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.herbelin
2013-03-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
2013-01-29Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).herbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
2013-01-18Unset Asymmetric Patternspboutill
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
2012-11-28Evarconv: Fix #2936 + commentspboutill
2012-11-21Fixing test-suite: Scope.vppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
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-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 #2809 (anomaly when printing a module with notations due toherbelin
2012-06-18Proof using: nested sections bugfixgareuselesinge
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
2012-04-12Repair two testsletouzey
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-19Fix bugs related to Program integration.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 00:54:56 +0000