index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
STM: make the slave start from the most recent known state
Enrico Tassi
2014-03-18
*
STM: make -async-proofs on work from coqc too
Enrico Tassi
2014-03-18
*
fix compilation with ocaml < 4
Enrico Tassi
2014-03-13
*
STM: perspective (tell the scheduler what the user sees)
Enrico Tassi
2014-03-13
*
STM: move out a couple of submodules
Enrico Tassi
2014-03-13
*
Stm: smarter delegation policy
Enrico Tassi
2014-03-12
*
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-11
*
Using Hashmaps by default in constant and inductive maps. This changes fold and
Pierre-Marie Pédrot
2014-03-07
*
Lets coqtop use a slash
Virgile Prevosto
2014-03-06
*
Using HMaps in Safe_env.environments, hopefully improving performances.
Pierre-Marie Pédrot
2014-03-05
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
STM: fix Show Script
Enrico Tassi
2014-03-04
*
STM: when finish a task hcons universe constraints
Enrico Tassi
2014-03-04
*
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
*
Migrate back g_obligations in toplevel
Pierre Letouzey
2014-03-02
*
Useless check when loading notations through import.
Pierre-Marie Pédrot
2014-03-01
*
Removing a fishy use of pervasive equality in Ltac backtrace printing.
Pierre-Marie Pédrot
2014-03-01
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
STM: better debug messages
Enrico Tassi
2014-02-26
*
STM: do not print goals on Undo
Enrico Tassi
2014-02-26
*
CoqIDE: print message of "Fail" command
Enrico Tassi
2014-02-26
*
STM: better messages when checking/finishing tasks
Enrico Tassi
2014-02-26
*
vi2vo: new flag -schedule-vi2vo
Enrico Tassi
2014-02-26
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
STM: backup/restore remote counters
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
Fixing printing of only_parsing notations.
Pierre-Marie Pédrot
2014-02-25
*
Simpl_behaviour becomes Reductionops.ReductionBehaviour
Pierre Boutillier
2014-02-24
*
Dead Code elimination
Pierre Boutillier
2014-02-24
*
Timeout and Set Default Timeout fixed (closes: #3229)
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
*
Removing the [Require "file"] syntax.
Pierre-Marie Pédrot
2014-02-02
*
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
*
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
2014-01-30
*
STM: tell the user if the master is recomputing states validated by workers
Enrico Tassi
2014-01-30
*
Fixing backtrace handling here and there.
Pierre-Marie Pédrot
2014-01-30
*
-schedule-vi-checking ported to spawn
Enrico Tassi
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
*
-schedule-vi-checking generates better script
Enrico Tassi
2014-01-14
*
STM: fix -async-proofs lazy
Enrico Tassi
2014-01-14
*
Make Require verbose
Pierre Boutillier
2014-01-13
*
STM: fix very simple demo
Enrico Tassi
2014-01-13
[next]