aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedGravatar herbelin2011-04-28
* Fixed notation printing bug when curly brackets are involved (requestsGravatar herbelin2011-04-28
* Fixing output of Notations2.v test messed up in r14060Gravatar herbelin2011-04-27
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vGravatar herbelin2011-04-08
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
* Did that adding a rule for printing applications as "f(x)" works.Gravatar herbelin2011-03-31
* Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)Gravatar letouzey2011-03-16
* Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionGravatar letouzey2011-03-16
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* Starting being more explicit on the reasons why module subtyping fails.Gravatar herbelin2011-03-05
* Improved define_evar_as_lambda which was creating an unrelated new evarGravatar herbelin2011-03-05
* Try to fix the behavior of clenv_missing used when declaring hintsGravatar letouzey2011-02-22
* Some fixes of the test-suite scriptsGravatar letouzey2011-02-21
* Fix test-suite script.Gravatar msozeau2011-02-21
* MacOS compatibilityGravatar pboutill2011-02-10
* Correct handling of existential variables when multiple differentGravatar msozeau2011-02-08
* test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)Gravatar glondu2011-01-27
* Add a test for sorting all universes of stdlibGravatar glondu2011-01-25
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Fixing an uncaught exception bug with use of vmcastGravatar herbelin2011-01-07
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
* Fixing bug using explictly declared implicit arguments in inductive arities.Gravatar herbelin2010-12-03
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* Fix missing -coqlib argument to coqdep in test-suiteGravatar glondu2010-10-16
* Adding test-case for bug #2362, which uses HO unification duringGravatar msozeau2010-10-12
* Fix bug #2393: allow let-ins inside telescopes (only fails when there'sGravatar msozeau2010-10-12
* Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingGravatar herbelin2010-10-11
* test-suite: fix success/unification.vGravatar glondu2010-10-07
* test-suite: fix output/Existentials.outGravatar glondu2010-10-06
* test-suite: fix success/Typeclasses.vGravatar glondu2010-10-05
* test-suite: fix success/AdvancedCanonicalStructure.vGravatar glondu2010-10-05
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
* test-suite: use unified diff output and use expected output as referenceGravatar glondu2010-10-05
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
* Test for non-regression of the display bug fixed in r13486.Gravatar herbelin2010-10-03
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Making display of various informations about constants more modular:Gravatar herbelin2010-10-03
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
* Fixed test of bug #2360 (use of Fail to check a regular error insteadGravatar herbelin2010-09-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 05:55:01 +0000