aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-07-10Fix a oversight in 5bf9e67b .Arnaud Spiwack
2014-07-09Revert patch making the oracle be used for the transparent state in evarconv,Matthieu Sozeau
2014-07-09Locate: also display some information about module aliasingPierre Letouzey
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-07-09Fixing the previous patch to keep transparent states in sync.Pierre-Marie Pédrot
2014-07-09Recovering transparent state from kernel oracles in constant time.Pierre-Marie Pédrot
2014-07-08Fixing bug #3270. Patch by Robbert Krebbers.Pierre-Marie Pédrot
2014-07-08Exporting Proof.split in proofview.Pierre-Marie Pédrot
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-07-07Updating README wrt coq-club and ftp.Hugo Herbelin
2014-07-07Fix g_coqast for explicit applications.Matthieu Sozeau
2014-07-07Coq_makefile: fix cmx compilation when there are both ml and mllibPierre Boutillier
2014-07-07In flex-flex cases, the undefinedness of an evar can not be preseved after co...Matthieu Sozeau
2014-07-07Missing check of evar instantiation, resulting in missing constraints (bug fr...Matthieu Sozeau
2014-07-07In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...Matthieu Sozeau
2014-07-05Using IStream coiterator to explicit the captured state of tactic matching re...Pierre-Marie Pédrot
2014-07-03Cleanup code related to the constraint solving, which sits now outside theMatthieu Sozeau
2014-07-03Properly compute the transitive closure of the system of constraintsMatthieu Sozeau
2014-07-03Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Matthieu Sozeau
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Matthieu Sozeau
2014-07-03Fix Coq_makefile in presence of mlpackPierre Boutillier
2014-07-03coqdoc is minimaly -Q awarePierre Boutillier
2014-07-03Adding a coiterator to IStream.Pierre-Marie Pédrot
2014-07-03More efficient implementation of Ltac match, by inlining a stream map.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:26:24 +0000