aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
|
* FinFun.v: results about injective/surjective/bijective fonctions over finite ↵Gravatar Pierre Letouzey2014-02-07
| | | | | | domains + Some extra results about NoDup, Fin.t, ...
* Tactic extensions do not need to be classified by the STM, asGravatar Pierre-Marie Pédrot2014-02-05
| | | | they never produce a VernacExtend entry.
* The constructor tactic now returns several successes.Gravatar Pierre-Marie Pédrot2014-02-04
|
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Allocation friendly map-handling functions in Dag.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Fixing backtrace reporting.Gravatar Pierre-Marie Pédrot2014-02-02
|
* Fixing bug #3226.Gravatar Pierre-Marie Pédrot2014-02-02
|
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
|
* In Ltac's exact tactic: avoid checking the type of the term twice.Gravatar Arnaud Spiwack2014-01-31
| | | | Following a remark by Jason Gross and Daniel Grayson.
* Typos in comment.Gravatar Arnaud Spiwack2014-01-31
|
* Coqmktop without Sys.command, changes in ./configure -*byteflags optionsGravatar Pierre Letouzey2014-01-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Relaunch all Unix.waitpid when they ended with EINTRGravatar Pierre Letouzey2014-01-30
| | | | Moreover, cleanup of System.connect (used by the "external" tactic).
* CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleanedGravatar Pierre Letouzey2014-01-30
|
* Mltop: explicitly qualify calls to CUnixGravatar Pierre Letouzey2014-01-30
|
* CString: avoid redefining is_subGravatar Pierre Letouzey2014-01-30
|
* Remove useless Xml_utilsGravatar Pierre Letouzey2014-01-30
|
* Get rid of two utility files, obsolete now that configure is a .mlGravatar Pierre Letouzey2014-01-30
|
* clib.mllib: remove duplicated Flags entryGravatar Pierre Letouzey2014-01-30
|
* G_xml: remove some duplication in error fonctionsGravatar Pierre Letouzey2014-01-30
|
* G_xml: protect against some possible Not_foundGravatar Pierre Letouzey2014-01-30
|
* Load implemented in CoqIDE/STM (closes: #3223)Gravatar Enrico Tassi2014-01-30
|
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
|
* Work around for bug in threads + blocking io streamlinedGravatar Enrico Tassi2014-01-30
|
* STM: worker sends back to master the last valid stateGravatar Enrico Tassi2014-01-30
| | | | | So that the master process does not require to compute it. Still not all valid states are sent back.
* STM: tell the user if the master is recomputing states validated by workersGravatar Enrico Tassi2014-01-30
| | | | | | When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
* Fixing backtrace handling here and there.Gravatar Pierre-Marie Pédrot2014-01-30
|
* Using Map.smartmap whenever deemed useful.Gravatar Pierre-Marie Pédrot2014-01-29
|
* Adding a smartmap[i] operator to maps.Gravatar Pierre-Marie Pédrot2014-01-29
|
* Fixing dependent inversion. Some exceptions were not caught by the tacticGravatar Pierre-Marie Pédrot2014-01-28
| | | | monad.
* Abstracting away coercion indexes in Classops.Gravatar Pierre-Marie Pédrot2014-01-27
|
* Coercions: avoid imperative data structureGravatar Enrico Tassi2014-01-26
|
* -schedule-vi-checking ported to spawnGravatar Enrico Tassi2014-01-26
|
* CoqIDE: command line for extra coqtop "flags"Gravatar Enrico Tassi2014-01-26
| | | | Like the socket for the OCaml debugger
* break > 80 cols lineGravatar Enrico Tassi2014-01-26
|
* STM: ported to spawnGravatar Enrico Tassi2014-01-26
|
* CoqIDE: ported to spawnGravatar Enrico Tassi2014-01-26
|
* Spawn: managed processesGravatar Enrico Tassi2014-01-26
| | | | | | | | | 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.
* configure.ml fixed wrt Win32 + byte-only + coqideGravatar Enrico Tassi2014-01-26
|
* Adding a test for bug #3023.Gravatar Pierre-Marie Pédrot2014-01-25
|
* More in CHANGES.Gravatar Pierre-Marie Pédrot2014-01-25
|
* [Coercion]s use [Sortclass], not [Prop] (in docs)Gravatar Jason Gross2014-01-24
| | | | Reported By: J. Ian Johnson
* The configure script now outputs the parameters it was fed with inGravatar Pierre-Marie Pédrot2014-01-24
| | | | config/coq_config.ml
* bug correction in proving principles of functionGravatar jforest2014-01-20
|
* Using full paths in coqdep -dumpgraph.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Fixing coqdep graph printing. The transitive reduction algorithm was bugged.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Fixing an interpretation bug with tactics in notations. For some obscureGravatar Pierre-Marie Pédrot2014-01-19
| | | | | | 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.
* Fixing checker compilation, which was broken by the following commit:Gravatar Pierre-Marie Pédrot2014-01-19
| | | | 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 02:29:29 +0000