aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Gravatar Pierre-Marie Pédrot2015-11-19
* Allow program hooks to see the refined universe_context at the end of aGravatar Matthieu Sozeau2015-11-19
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Fixing fix c71aa6b to primitive projections.Gravatar Hugo Herbelin2015-11-18
* Fix a bug preventing the generation of graphs when doing multipleGravatar Matthieu Sozeau2015-11-18
* Improve error message.Gravatar Maxime Dénès2015-11-18
* MacOS package script: do not fail if link to /Applications already exists.Gravatar Maxime Dénès2015-11-18
* Slightly documenting code for building primitive projections.Gravatar Hugo Herbelin2015-11-18
* Fixing logical bugs in the presence of let-ins in computiong primitiveGravatar Hugo Herbelin2015-11-18
* More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
* Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* Being more precise and faithful about the origin of the file reportingGravatar Hugo Herbelin2015-11-16
* Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Gravatar Matthieu Sozeau2015-11-13
* MacOS package script: do not fail if directory _dmg already exists.Gravatar Maxime Dénès2015-11-13
* Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Gravatar Pierre-Marie Pédrot2015-11-12
* Fixed test-suite file for bug #3998.Gravatar Matthieu Sozeau2015-11-12
* Update CHANGESGravatar Jason Gross2015-11-12
* Script building MacOS package.Gravatar Maxime Dénès2015-11-12
* Now closed.Gravatar Matthieu Sozeau2015-11-11
* Ensure that conversion is called on terms of the same type inGravatar Matthieu Sozeau2015-11-11
* Fix bug #3998: when using typeclass resolution for conversion, allowGravatar Matthieu Sozeau2015-11-11
* Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
* Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
* Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
* Dead code from the commit having introduced primitive projections (a4043608).Gravatar Hugo Herbelin2015-11-10
* Typo.Gravatar Hugo Herbelin2015-11-10
* Fixing a bug in reporting ill-formed constructor.Gravatar Hugo Herbelin2015-11-10
* Test for bug #4404.Gravatar Pierre-Marie Pédrot2015-11-10
* Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Gravatar Pierre-Marie Pédrot2015-11-10
* Pushing the backtrace in conversion anomalies.Gravatar Pierre-Marie Pédrot2015-11-09
* Fixing output test Existentials.v after eec77191b.Gravatar Hugo Herbelin2015-11-07
* Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Gravatar Hugo Herbelin2015-11-07
* Tests for syntax "Show id" and [id]:tac (shelved or not).Gravatar Hugo Herbelin2015-11-07
* Fixing documention of Add Printing Coercion.Gravatar Hugo Herbelin2015-11-07
* Fixed #4407.Gravatar Pierre Courtieu2015-11-06
* Fixing #4406 coqdep: No recursive search of ml (-I).Gravatar Pierre Courtieu2015-11-06
* Fixing complexity file f_equal.v.Gravatar Hugo Herbelin2015-11-06
* More on how to compile doc.Gravatar Hugo Herbelin2015-11-06
* Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
* Add test-suite file for #4273.Gravatar Matthieu Sozeau2015-11-05
* Fix bug #4273Gravatar Matthieu Sozeau2015-11-05
* Update version numbers and magic numbers for 8.5beta3 release.Gravatar Maxime Dénès2015-11-05
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
* Univs: missing checks in evarsolve with candidates and missing aGravatar Matthieu Sozeau2015-11-04
* Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* Univs: compatibility with 8.4.Gravatar Matthieu Sozeau2015-11-04
* Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
* Test file for #4397.Gravatar Maxime Dénès2015-11-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:55:12 +0000