| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-01-17 | Follow-up of bugfix for #3204: local definitions were not handled properly. | Pierre-Marie Pédrot | |
| 2014-01-17 | Fixing bug #1758: Print Hint output can be misleading if variable shadows ↵ | Pierre-Marie Pédrot | |
| hypothesis. | |||
| 2014-01-17 | Update .mailmap with recent contributors. | Arnaud Spiwack | |
| I should have updated everyone who committed since the migration to git (giving me a canonical email). I've search git shortlog -s to ensure the best I could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed. | |||
| 2014-01-16 | Fixing bugs #1039: Hypotheses don't respect Barendregt convention | Pierre-Marie Pédrot | |
| and #3204: Failure of hygiene condition. It was sufficient to tweak a flag in the constr externalization... | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |