aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Cleanup API and comments of 908dcd613Gravatar Enrico Tassi2015-10-29
* Accept option -compat 8.5. (Fix bug #4393)Gravatar Guillaume Melquiond2015-10-29
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Printing of @{} instances for polymorphic references in Print and About.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* lib_stack: API to reorder the libstackGravatar Enrico Tassi2015-10-28
* Fix test suite after Matthieu's ed7af646f2e486b.Gravatar Maxime Dénès2015-10-28
* Fix bug in native compiler with universe polymorphism.Gravatar Maxime Dénès2015-10-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 15:42:26 +0000