aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
2011-12-17Added ability to take the type of applied metas into account whenherbelin
2011-12-12Proof using ...gareuselesinge
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Updating Cases.v test.herbelin
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:34:47 +0000