aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-07-21Fixing semantics of HSet.inter and HSet.diff.Pierre-Marie Pédrot
2014-07-21More straightforward definition of Universes.add_list_map.Pierre-Marie Pédrot
2014-07-21Cleanup substitution inside universe instances, only done through subst_fn now,Matthieu Sozeau
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2014-07-21Correct eauto which was not dealing properly with polymorphic constants.Matthieu Sozeau
2014-07-21Cleanup code for constant equality in kernel conversion.Matthieu Sozeau
2014-07-21Missing space in pretty-printerPierre-Marie Pédrot
2014-07-21Documenting the changes of Locate semantics.Pierre-Marie Pédrot
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate co...Pierre-Marie Pédrot
2014-07-21Documenting the need of the "DECLARE PLUGIN" statement.Pierre-Marie Pédrot
2014-07-21Documenting the change of semantics of the "constructor" tactic.Pierre-Marie Pédrot
2014-07-21Adding a test-suite for bug #3422.Pierre-Marie Pédrot
2014-07-20Use kernel conversion on terms that contain universe variables during unifica...Matthieu Sozeau
2014-07-17Fix coercion code to disallow using cumulativity in the domain of products, w...Matthieu Sozeau
2014-07-17Completing c236b51348d2 by fixing EqdepFactsv actually committing theHugo Herbelin
2014-07-16Adding a test-suite for bug #3416.Pierre-Marie Pédrot
2014-07-16Fixing universe substitution in mutual fixpoints.Pierre-Marie Pédrot
2014-07-16STM: check-vi-task fixedEnrico Tassi
2014-07-16STM: Goal printing got wrong in a merge, fixedEnrico Tassi
2014-07-16- Fix bug introduced in obligations which wouldn't consider all evars that areMatthieu Sozeau
2014-07-15Added a (constructive) proof of Weak Konig's lemma for decidable trees.Hugo Herbelin
2014-07-15Some basics facts about eq_dep.Hugo Herbelin
2014-07-15Using the generic timeout function in the boostrapped file.Pierre-Marie Pédrot
2014-07-14Don't set global variables from a hidden file. (!)Matthieu Sozeau
2014-07-14Add interface function to replace new_Type ()Matthieu Sozeau
2014-07-14Redo PMP's patch to rewriting to make it purely functional using state passing.Matthieu Sozeau
2014-07-14smartlocate: look for the head symbol for realEnrico Tassi
2014-07-14Adding a delay to tclTIME.Pierre-Marie Pédrot
2014-07-13Mentioning the incompatibility due to fixing bug #2996 (see #3418).Hugo Herbelin
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-11Fix Funind test-suite file after patch by Pierre.Matthieu Sozeau
2014-07-11Properly add a Set lower bound on any polymorphic inductive in Type withMatthieu Sozeau
2014-07-11An outdated comment + comment layout.Arnaud Spiwack
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
2014-07-11STM: flag to turn off branch reopeningEnrico Tassi
2014-07-11STM: add optionally takes the id of the new tipEnrico Tassi
2014-07-11STM: export the observe function (useful for pide)Enrico Tassi
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-07-11Export type_of_global_ref (useful for external users of glob files)Enrico Tassi
2014-07-11make the standard logging facility stm awareEnrico Tassi
2014-07-10MSetRBT: unfortunate typo in compare_height (fix #3413)Pierre Letouzey
2014-07-10Better handling of the universe context in case of Admitted proof obligations.Matthieu Sozeau
2014-07-10Overlooked to remove a change in kernel/closure that made reducing underMatthieu Sozeau
2014-07-10option to always delegate futures to workersEnrico Tassi
2014-07-10CoqIDE: on win32 the old interrputer code (SIGINT) is still neededEnrico Tassi
2014-07-10more APIs in TQueue and CThreadEnrico Tassi
2014-07-10check_for_interrupt: better (but slower) in threading modeEnrico Tassi
2014-07-10Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:57:32 +0000