aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Remove code that was already commented out.Gravatar Maxime Dénès2015-10-12
* Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
* Fix Definition id := Eval <redexpr> in by passing the right universeGravatar Matthieu Sozeau2015-10-12
* Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...Gravatar Matthieu Sozeau2015-10-12
* Gather VM tags in Cbytecodes.Gravatar Maxime Dénès2015-10-12
* Adding test for bug #4366.Gravatar Pierre-Marie Pédrot2015-10-11
* Fixing bug #4366: Conversion tactics recheck uselessly convertibility.Gravatar Pierre-Marie Pédrot2015-10-11
* Fixing test-suiteGravatar Hugo Herbelin2015-10-11
* Documenting matching under binders.Gravatar Hugo Herbelin2015-10-11
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
* Fixing obviously untested fold_glob_constr and iter_glob_constr.Gravatar Hugo Herbelin2015-10-11
* Constr_matching: renaming misleading name stk into ctx.Gravatar Hugo Herbelin2015-10-11
* Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Gravatar Guillaume Melquiond2015-10-10
* Complete handling of primitive projections in VM.Gravatar Maxime Dénès2015-10-09
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Minor typo in universe polymorphism doc.Gravatar Maxime Dénès2015-10-09
* Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
* Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
* Fix Next Obligation to not raise an anomaly in case of mutualGravatar Matthieu Sozeau2015-10-09
* Fix inference of return clause raising a type error.Gravatar Matthieu Sozeau2015-10-09
* STM: Work around an occasional crash in dot (debug output)Gravatar Alec Faithfull2015-10-09
* TQueue: Allow some tasks to be saved when clearing a TQueueGravatar Alec Faithfull2015-10-09
* TQueue: Expose the length of TQueuesGravatar Alec Faithfull2015-10-09
* STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
* STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
* Remove misleading warning (Close #4365)Gravatar Enrico Tassi2015-10-09
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Allowing empty bound universe variables.Gravatar Pierre-Marie Pédrot2015-10-08
* Univs: fix bug #4161.Gravatar Matthieu Sozeau2015-10-08
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* f_equal fix continued: do a refresh_universes as before.Gravatar Matthieu Sozeau2015-10-08
* aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* term_typing: strengthen discharging codeGravatar Enrico Tassi2015-10-08
* CThread: blocking read + threads now worksGravatar Enrico Tassi2015-10-08
* Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
* STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
* Future: make not-here/not-ready messages customizableGravatar Enrico Tassi2015-10-08
* STM: fix backtrace handlingGravatar Enrico Tassi2015-10-08
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
* Fix bug #4069: f_equal regression.Gravatar Matthieu Sozeau2015-10-07
* Univs: fix FingerTree contrib.Gravatar Matthieu Sozeau2015-10-07
* Test for record syntax parsing.Gravatar Pierre-Marie Pédrot2015-10-07
* Record fields accept an optional final semicolon separator.Gravatar Pierre-Marie Pédrot2015-10-07
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Fixing emacs output in debugging mode.Gravatar Pierre Courtieu2015-10-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 08:10:28 +0000