| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-02-24 | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier | |
| 2014-02-24 | Fix grammatical mistake in error message (bug #3238) | xclerc | |
| 2014-02-21 | More sharing in Logic, together with some code cleaning. | Pierre-Marie Pédrot | |
| 2014-02-20 | Optimization in kernel/vars.ml: directly allocate a fixed-size block in the | Pierre-Marie Pédrot | |
| subst1 case. | |||
| 2014-02-17 | CoqIDE: when coqtop misbehaves kill it properly (no zombie) | Enrico Tassi | |
| 2014-02-17 | [nanoPG]: emacs like copy/paste | Enrico Tassi | |
| 2014-02-16 | Removing non-marshallable data from the Agram constructor. Instead of | Pierre-Marie Pédrot | |
| containing opaque grammar objects, it now contains a string representing the entry. In order to recover the entry from the string, the former must have been created with [Pcoq.create_generic_entry] or similar. This is guaranteed for entries generated by ARGUMENT EXTEND, and must be done by hand otherwise. Some plugins were fixed accordingly. | |||
| 2014-02-14 | fast correction of bug #3234 | Julien Forest | |
| 2014-02-12 | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi | |
| The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes. | |||
| 2014-02-11 | Made Pre_env.lazy_val opaque. | Pierre-Marie Pédrot | |
| 2014-02-10 | Timeout and Set Default Timeout fixed (closes: #3229) | Enrico Tassi | |
| 2014-02-10 | STM: fix valid_id coming from Qed errors | Enrico Tassi | |
| 2014-02-10 | STM: when a worker is canceled mark the proof as broken | Enrico Tassi | |
| 2014-02-10 | STM: be conservative w.r.t. proofs containing global side effects | Enrico Tassi | |
| 2014-02-10 | fake_ide: ported to spawn | Enrico Tassi | |
| 2014-02-10 | Tentative fixup for the previous commit. It seems I have broken something | Pierre-Marie Pédrot | |
| nasty relating memory management triggering random segfaults. But this seemed really unlikely... | |||
| 2014-02-09 | Small optimizations in Closure: | Pierre-Marie Pédrot | |
| 1. Only apply last Zupdates 2. Better smartmap with state. | |||
| 2014-02-08 | Less dependencies in Omega. | Pierre-Marie Pédrot | |
| 2014-02-07 | FinFun.v: results about injective/surjective/bijective fonctions over finite ↵ | Pierre Letouzey | |
| domains + Some extra results about NoDup, Fin.t, ... | |||
| 2014-02-05 | Tactic extensions do not need to be classified by the STM, as | Pierre-Marie Pédrot | |
| they never produce a VernacExtend entry. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |