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
*
CoqIDE ported to the revides protocol
gareuselesinge
2013-09-30
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Made the filename of compiled files explicit, i.e. add a ./ prefix
ppedrot
2013-09-19
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
STM pretty printer should never fail
gareuselesinge
2013-09-13
*
fix STM feeback on running jobs
gareuselesinge
2013-09-13
*
Unplugging Autoinstance. The code is still here if someone wishes
ppedrot
2013-09-12
*
CoqIDE: show number of proofs being checked in background
gareuselesinge
2013-09-12
*
Unknown commands starting a proof were not setting the proof mode.
gareuselesinge
2013-09-12
*
Remove outdated comment
gareuselesinge
2013-09-12
*
VernacList handling was lost in STM merge
gareuselesinge
2013-09-12
*
Temporary fix of emacs mode for ProofGeneral
letouzey
2013-09-10
*
Moving Searchstack to CStack, and normalizing names a bit.
ppedrot
2013-09-06
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
summary for ML modules made correct
gareuselesinge
2013-08-30
*
Make the jopin-document button wait for slaves to terminate
gareuselesinge
2013-08-30
*
When PG is used as interface behave as before STM
gareuselesinge
2013-08-30
*
ind_tables: properly handling side effects
gareuselesinge
2013-08-30
*
Stm: if slave process dies badly go back to local lazy evaluation
gareuselesinge
2013-08-30
*
-coq-slaves: close_on_exec + correct argument passing
gareuselesinge
2013-08-30
*
Fixing bug #3083.
ppedrot
2013-08-28
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Less "Coq" strings everywhere
letouzey
2013-08-22
*
Fix STM: Module Import may change the parser
gareuselesinge
2013-08-20
*
Universe counters on slaves are in sync with master
gareuselesinge
2013-08-20
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Himsg : strict 80-column indentation
letouzey
2013-08-20
*
Safe_typing code refactoring
letouzey
2013-08-20
*
Modulification and removing of structural equality in Stateid.
ppedrot
2013-08-19
*
Modulification and removing of structural equality in VCS.
ppedrot
2013-08-19
*
Fixing potentially misused Errors.push.
ppedrot
2013-08-12
*
Mutual proofs cannot be delegated
gareuselesinge
2013-08-11
*
Small typos
ppedrot
2013-08-10
*
Lemmas ending with Defined cannot be delegated to slaves
gareuselesinge
2013-08-10
*
Fix batch compilation of scripts with Admitted proofs (in a section)
gareuselesinge
2013-08-09
*
fix batch compilation of scripts containing Admitted
gareuselesinge
2013-08-09
*
stm: (initial) support for -coq-slaves
gareuselesinge
2013-08-08
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
Vernac classification streamlined (handles VERNAC EXTEND)
gareuselesinge
2013-08-08
*
Simple machinery to detect EXTEND that interpret during parsing
gareuselesinge
2013-08-08
*
Support Proof General
gareuselesinge
2013-08-08
*
Coqide ported to STM
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Added more flags choice in desambiguating printer. The code is
ppedrot
2013-08-06
*
Tentative fix for bug #2961. When we have to print two terms that
ppedrot
2013-08-05
*
Fixing #2846: Uncaught exception Reduction.NotArity.
ppedrot
2013-08-04
[next]