aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Update compatibility file for some of bug #4392Gravatar Jason Gross2015-11-03
* Fix bug #4397: refreshing types in abstract_generalize.Gravatar Matthieu Sozeau2015-11-02
* Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
* Refresh rigid universes as well, and in 8.4 compatibility mode,Gravatar Matthieu Sozeau2015-11-02
* Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Gravatar Maxime Dénès2015-11-02
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* Made that the syntax [id]:tac also applies to the shelve, which is after all ...Gravatar Hugo Herbelin2015-11-02
* STM: fix undo into a branch containing side effectsGravatar Enrico Tassi2015-11-02
* STM: never reopen a branch containing side effectsGravatar Enrico Tassi2015-11-02
* Command.declare_definition: grab the fix_exn early (follows 77cf18e)Gravatar Enrico Tassi2015-10-30
* Manually expand red_tactic so that notations do not break reduction tactics. ...Gravatar Guillaume Melquiond2015-10-30
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* Fix typo.Gravatar Guillaume Melquiond2015-10-30
* Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* Collect subproof universes in handle_side_effects.Gravatar Matthieu Sozeau2015-10-29
* Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Gravatar Guillaume Melquiond2015-10-29
* Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)Gravatar Guillaume Melquiond2015-10-29
* Fixing another instance of bug #3267 in eauto, this time in theGravatar Hugo Herbelin2015-10-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 15:06:04 +0000