aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-02-22Try to fix the behavior of clenv_missing used when declaring hintsletouzey
2011-02-21Some fixes of the test-suite scriptsletouzey
2011-02-21Fix test-suite script.msozeau
2011-02-08Correct handling of existential variables when multiple differentmsozeau
2011-01-11Add "Print Sorted Universes"glondu
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
2010-12-23Remove the two-argument variant of "decide equality"glondu
2010-12-19Fixing bug #2454: inversion predicate strategy for inferring the typeherbelin
2010-12-04Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:37:28 +0000