aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
2011-10-25Fixing "destruct" test.herbelin
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-08-04moins de reification inutile, noatations standardspottier
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18add names of theorems in outputjnarboux
2011-06-16Tests de nsatz avec la geometriepottier
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-13Another bug of Scheme Induction (generated names dep/nodep were swapped).herbelin
2011-06-13Fixing an anomaly in Scheme Induction.herbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
2011-05-26Mini-test for etaherbelin
2011-05-26Partial fix for accepting bound variables with same name as implicitherbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-05-17Add simple test of bullet behaviour.aspiwack
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
2011-04-28Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedherbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 09:57:50 +0000