aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2010-12-03Fixing bug using explictly declared implicit arguments in inductive arities.herbelin
2010-12-02Fixing a bug introduced in r12304 (move of interpretation ofherbelin
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
2010-10-07test-suite: fix success/unification.vglondu
2010-10-05test-suite: fix success/Typeclasses.vglondu
2010-10-05test-suite: fix success/AdvancedCanonicalStructure.vglondu
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
2010-09-11Improving a few error messages in Ltac interpretationherbelin
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-12Fix compilation and test-suite of nsatzglondu
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-04Grobner.v removedpottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-17Moved Case3.v from ideal features to success (it works since 8.2).herbelin
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
2010-04-07Commit 12906 continued (forgotten file).herbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-03-12fixed minor pbs with test casesbarras
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-02-10ajout test de fied_simplify_eq inbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:34:33 +0000