aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-02-04The constructor tactic now returns several successes.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2014-02-03Allocation friendly map-handling functions in Dag.Pierre-Marie Pédrot
2014-02-02Fixing backtrace reporting.Pierre-Marie Pédrot
2014-02-02Fixing bug #3226.Pierre-Marie Pédrot
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-31In Ltac's exact tactic: avoid checking the type of the term twice.Arnaud Spiwack
2014-01-31Typos in comment.Arnaud Spiwack
2014-01-30Coqmktop without Sys.command, changes in ./configure -*byteflags optionsPierre Letouzey
2014-01-30Relaunch all Unix.waitpid when they ended with EINTRPierre Letouzey
2014-01-30CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleanedPierre Letouzey
2014-01-30Mltop: explicitly qualify calls to CUnixPierre Letouzey
2014-01-30CString: avoid redefining is_subPierre Letouzey
2014-01-30Remove useless Xml_utilsPierre Letouzey
2014-01-30Get rid of two utility files, obsolete now that configure is a .mlPierre Letouzey
2014-01-30clib.mllib: remove duplicated Flags entryPierre Letouzey
2014-01-30G_xml: remove some duplication in error fonctionsPierre Letouzey
2014-01-30G_xml: protect against some possible Not_foundPierre Letouzey
2014-01-30Load implemented in CoqIDE/STM (closes: #3223)Enrico Tassi
2014-01-30STM + CoqIDE: stop_worker message and UIEnrico Tassi
2014-01-30Work around for bug in threads + blocking io streamlinedEnrico Tassi
2014-01-30STM: worker sends back to master the last valid stateEnrico Tassi
2014-01-30STM: tell the user if the master is recomputing states validated by workersEnrico Tassi
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2014-01-29Adding a smartmap[i] operator to maps.Pierre-Marie Pédrot
2014-01-28Fixing dependent inversion. Some exceptions were not caught by the tacticPierre-Marie Pédrot
2014-01-27Abstracting away coercion indexes in Classops.Pierre-Marie Pédrot
2014-01-26Coercions: avoid imperative data structureEnrico Tassi
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-26CoqIDE: command line for extra coqtop "flags"Enrico Tassi
2014-01-26break > 80 cols lineEnrico Tassi
2014-01-26STM: ported to spawnEnrico Tassi
2014-01-26CoqIDE: ported to spawnEnrico Tassi
2014-01-26Spawn: managed processesEnrico Tassi
2014-01-26configure.ml fixed wrt Win32 + byte-only + coqideEnrico Tassi
2014-01-25Adding a test for bug #3023.Pierre-Marie Pédrot
2014-01-25More in CHANGES.Pierre-Marie Pédrot
2014-01-24[Coercion]s use [Sortclass], not [Prop] (in docs)Jason Gross
2014-01-24The configure script now outputs the parameters it was fed with inPierre-Marie Pédrot
2014-01-20bug correction in proving principles of functionjforest
2014-01-19Using full paths in coqdep -dumpgraph.Pierre-Marie Pédrot
2014-01-19Fixing coqdep graph printing. The transitive reduction algorithm was bugged.Pierre-Marie Pédrot
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2014-01-19Fixing an interpretation bug with tactics in notations. For some obscurePierre-Marie Pédrot
2014-01-19Fixing checker compilation, which was broken by the following commit:Pierre-Marie Pédrot
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
2014-01-18Makefiles use $(foo), not $foo, for variablesJason Gross
2014-01-18Fixup make clean and .merlinPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 02:18:27 +0000