aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-10-10Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Guillaume Melquiond
2015-10-09Complete handling of primitive projections in VM.Maxime Dénès
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Minor typo in universe polymorphism doc.Maxime Dénès
2015-10-09Refine fix for handling of the universe contexts of hints, depending onMatthieu Sozeau
2015-10-09Fix CFGV contrib: handling of global hints introducing global universes.Matthieu Sozeau
2015-10-09Fix Next Obligation to not raise an anomaly in case of mutualMatthieu Sozeau
2015-10-09Fix inference of return clause raising a type error.Matthieu Sozeau
2015-10-09STM: Work around an occasional crash in dot (debug output)Alec Faithfull
2015-10-09TQueue: Allow some tasks to be saved when clearing a TQueueAlec Faithfull
2015-10-09TQueue: Expose the length of TQueuesAlec Faithfull
2015-10-09STM: Added functions for saving and restoring the internal stateAlec Faithfull
2015-10-09STM: Pass exception information to unreachable_state_hook functionsAlec Faithfull
2015-10-09Remove misleading warning (Close #4365)Enrico Tassi
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-08Allowing empty bound universe variables.Pierre-Marie Pédrot
2015-10-08Univs: fix bug #4161.Matthieu Sozeau
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08f_equal fix continued: do a refresh_universes as before.Matthieu Sozeau
2015-10-08aux_file: export API to ease writing of a Proof Using annotator.Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-08term_typing: strengthen discharging codeEnrico Tassi
2015-10-08CThread: blocking read + threads now worksEnrico Tassi
2015-10-08Spawn: use each socket exclusively for writing or readingEnrico Tassi
2015-10-08STM: for PIDE based UIs, edit_at requires no Reach.known_stateEnrico Tassi
2015-10-08Future: make not-here/not-ready messages customizableEnrico Tassi
2015-10-08STM: fix backtrace handlingEnrico Tassi
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
2015-10-07Test for record syntax parsing.Pierre-Marie Pédrot
2015-10-07Record fields accept an optional final semicolon separator.Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-06Fixing emacs output in debugging mode.Pierre Courtieu
2015-10-06Univs (pretyping): call vm_compute/native_compute with the currentMatthieu Sozeau
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-10-05Univs: fix bug #4288, Print Sorted generated backward < constraints.Matthieu Sozeau
2015-10-05Univs: fix printing bug #3797.Matthieu Sozeau
2015-10-05Update the .mailmap file.Guillaume Melquiond
2015-10-05Univs: fix handling of evar_map in identity coercion construction.Matthieu Sozeau
2015-10-04Fix typo. (Fix bug #4355)Guillaume Melquiond
2015-10-02Mark the Coq.Compat files for documentation. (Fix bug #4353)Guillaume Melquiond
2015-10-02Updating versions history with data from Gérard.Hugo Herbelin
2015-10-02Fixing error messages about Hint.Hugo Herbelin
2015-10-02Improving reference manual in that auto uses simple apply rather than apply.Hugo Herbelin
2015-10-02Update the history of versions with recent versions.Hugo Herbelin
2015-10-02Univs: Change intf of push_named_def to return the computed universeMatthieu Sozeau
2015-10-02Univs: refined handling of assumptionsMatthieu Sozeau
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 16:08:11 +0000