aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 14:10:56 +0000