| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-02-24 | IStream: a concat_map primitive. | Arnaud Spiwack | |
| 2014-02-24 | IStream: change type of thunk, spare allocations. | Arnaud Spiwack | |
| Two changes: - 'a Lazy.t becomes unit -> 'a - 'a t becomes 'a u (the view type) This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial. | |||
| 2014-02-24 | IStream: remove a useless Obj.magic. | Arnaud Spiwack | |
| Lazy.lazy_from_val does almost the same thing as this Obj.magic. It makes some extra dynamic check, but it's frankly unlikely that it could be observed. | |||
| 2014-02-24 | A view type for IStream. | Arnaud Spiwack | |
| View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations) | |||
| 2014-02-24 | Ensuring that the module Stack is opaque inside Reductionops. | Pierre-Marie Pédrot | |
| 2014-02-24 | make coqide-binaries does not build coqtop anymore | Pierre Boutillier | |
| 2014-02-24 | fixup complement Fin | Pierre Boutillier | |
| 2014-02-24 | cbn understands Arguments | Pierre Boutillier | |
| (excepts list of args that must be constructors | |||
| 2014-02-24 | Simpl_behaviour becomes Reductionops.ReductionBehaviour | Pierre Boutillier | |
| syntax mentionning simpl remains | |||
| 2014-02-24 | Dead Code elimination | Pierre Boutillier | |
| 2014-02-24 | Create Debug Unification option | Pierre Boutillier | |
| to dump states that Evarconv.eq_appr_x tries to unify. | |||
| 2014-02-24 | Fix coqide build under MacOS | Pierre Boutillier | |
| 2014-02-24 | No more translation array <-> list in Reductionops.Stack | Pierre Boutillier | |
| 2014-02-24 | Reductionops.Stack.strip* are ready to deal with Shift | Pierre Boutillier | |
| 2014-02-24 | Reductionops.Stack.app_node is secret | Pierre Boutillier | |
| 2014-02-24 | app_node, stack, state printers | Pierre Boutillier | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |