| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-02-04 | The constructor tactic now returns several successes. | Pierre-Marie Pédrot | |
| 2014-02-03 | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot | |
| 2014-02-03 | Allocation-friendly mapping functions in Nametab. | Pierre-Marie Pédrot | |
| 2014-02-03 | Allocation friendly map-handling functions in Dag. | Pierre-Marie Pédrot | |
| 2014-02-02 | Fixing backtrace reporting. | Pierre-Marie Pédrot | |
| 2014-02-02 | Fixing bug #3226. | Pierre-Marie Pédrot | |
| 2014-02-02 | Removing the [Require "file"] syntax. | Pierre-Marie Pédrot | |
| 2014-01-31 | In Ltac's exact tactic: avoid checking the type of the term twice. | Arnaud Spiwack | |
| Following a remark by Jason Gross and Daniel Grayson. | |||
| 2014-01-31 | Typos in comment. | Arnaud Spiwack | |
| 2014-01-30 | Coqmktop without Sys.command, changes in ./configure -*byteflags options | Pierre Letouzey | |
| NB: Please re-run ./configure after pulling this commit For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore, but rather CUnix.sys_command, which is based on Unix.create_process. This way, we do not need to bother with the underlying shell (/bin/sh or cmd.exe) and the way arguments are to be quoted :-). Btw, many cleanups of coqmktop. Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option" that collect as a string several sub-options to be given by coqmktop to ocamlc. For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to parse all these sub-options. To ease that, I've made the following changes to the ./configure options: * The -coqrunbyteflags and its blank-separated argument isn't accepted anymore, and is replaced by a new option -vmbyteflags which expects a comma-separated argument. For instance: ./configure -vmbyteflags "-dllib,-lcoqrun" Btw, on this example, the double-quotes aren't mandatory anymore :-) * The -coqtoolsbyteflags isn't accepted anymore. To the best of my knowledge, nobody ever used it directly (it was internally triggered as a byproduct of the -custom option). The only interest I can think of for this option was to cancel the default use of ocamlc custom-linking on Win32 and MacOS. For that, ./configure now provides a -no-custom option. | |||
| 2014-01-30 | Relaunch all Unix.waitpid when they ended with EINTR | Pierre Letouzey | |
| Moreover, cleanup of System.connect (used by the "external" tactic). | |||
| 2014-01-30 | CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned | Pierre Letouzey | |
| 2014-01-30 | Mltop: explicitly qualify calls to CUnix | Pierre Letouzey | |
| 2014-01-30 | CString: avoid redefining is_sub | Pierre Letouzey | |
| 2014-01-30 | Remove useless Xml_utils | Pierre Letouzey | |
| 2014-01-30 | Get rid of two utility files, obsolete now that configure is a .ml | Pierre Letouzey | |
| 2014-01-30 | clib.mllib: remove duplicated Flags entry | Pierre Letouzey | |
| 2014-01-30 | G_xml: remove some duplication in error fonctions | Pierre Letouzey | |
| 2014-01-30 | G_xml: protect against some possible Not_found | Pierre Letouzey | |
| 2014-01-30 | Load implemented in CoqIDE/STM (closes: #3223) | Enrico Tassi | |
| 2014-01-30 | STM + CoqIDE: stop_worker message and UI | Enrico Tassi | |
| 2014-01-30 | Work around for bug in threads + blocking io streamlined | Enrico Tassi | |
| 2014-01-30 | STM: worker sends back to master the last valid state | Enrico Tassi | |
| So that the master process does not require to compute it. Still not all valid states are sent back. | |||
| 2014-01-30 | STM: tell the user if the master is recomputing states validated by workers | Enrico Tassi | |
| When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly. | |||
| 2014-01-30 | Fixing backtrace handling here and there. | Pierre-Marie Pédrot | |
| 2014-01-29 | Using Map.smartmap whenever deemed useful. | Pierre-Marie Pédrot | |
| 2014-01-29 | Adding a smartmap[i] operator to maps. | Pierre-Marie Pédrot | |
| 2014-01-28 | Fixing dependent inversion. Some exceptions were not caught by the tactic | Pierre-Marie Pédrot | |
| monad. | |||
| 2014-01-27 | Abstracting away coercion indexes in Classops. | Pierre-Marie Pédrot | |
| 2014-01-26 | Coercions: avoid imperative data structure | Enrico Tassi | |
| 2014-01-26 | -schedule-vi-checking ported to spawn | Enrico Tassi | |
| 2014-01-26 | CoqIDE: command line for extra coqtop "flags" | Enrico Tassi | |
| Like the socket for the OCaml debugger | |||
| 2014-01-26 | break > 80 cols line | Enrico Tassi | |
| 2014-01-26 | STM: ported to spawn | Enrico Tassi | |
| 2014-01-26 | CoqIDE: ported to spawn | Enrico Tassi | |
| 2014-01-26 | Spawn: managed processes | Enrico Tassi | |
| The Spawn and Spawned modules factor the operation of spawning a process. Both synchronous and asynchronous channels are supported. Both threaded and glib like main loop models are supported. Still, not all combinations are truly tested not equipped with a decent API: only async + glib and sync + thread are, since these are the models we use for coqide<->coqtop and coqtop<->worker respectively. | |||
| 2014-01-26 | configure.ml fixed wrt Win32 + byte-only + coqide | Enrico Tassi | |
| 2014-01-25 | Adding a test for bug #3023. | Pierre-Marie Pédrot | |
| 2014-01-25 | More in CHANGES. | Pierre-Marie Pédrot | |
| 2014-01-24 | [Coercion]s use [Sortclass], not [Prop] (in docs) | Jason Gross | |
| Reported By: J. Ian Johnson | |||
| 2014-01-24 | The configure script now outputs the parameters it was fed with in | Pierre-Marie Pédrot | |
| config/coq_config.ml | |||
| 2014-01-20 | bug correction in proving principles of function | jforest | |
| 2014-01-19 | Using full paths in coqdep -dumpgraph. | Pierre-Marie Pédrot | |
| 2014-01-19 | Fixing coqdep graph printing. The transitive reduction algorithm was bugged. | Pierre-Marie Pédrot | |
| 2014-01-19 | Adding a default object to generic argument registering mechanism. | Pierre-Marie Pédrot | |
| 2014-01-19 | Fixing an interpretation bug with tactics in notations. For some obscure | Pierre-Marie Pédrot | |
| reason, Ltac interpretation does not allow tactics of the following shape : let x := bla in TacGeneric tac. Hence we force genargs to be tactics and build the resulting hole tactic from scratch. | |||
| 2014-01-19 | Fixing checker compilation, which was broken by the following commit: | Pierre-Marie Pédrot | |
| 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369 | |||
| 2014-01-18 | Relaxing the sort elimination check to allow for let-bindings in arities. | Maxime Dénès | |
| I restored this in the kernel, and added it to the checker. There is one last source of non-uniformity, which is the Sort case in the checker (was not present in the kernel). I don't know what this case covers, so it should be reviewed. | |||
| 2014-01-18 | Makefiles use $(foo), not $foo, for variables | Jason Gross | |
| Also, we need :=, so that it's evaluated immediately, rather than becoming a self-recursive variable. This fixes the "Undefined variable 'C'" error that make keeps spewing. | |||
| 2014-01-18 | Fixup make clean and .merlin | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |