index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
CoqIDE: fixed detection of edits in the locked zone
gareuselesinge
2013-08-20
*
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
*
Declareops + Modops : more clever substitutions
letouzey
2013-08-20
*
Himsg : strict 80-column indentation
letouzey
2013-08-20
*
Mod_typing : code cleanup
letouzey
2013-08-20
*
Safe_typing code refactoring
letouzey
2013-08-20
*
Attempt to restore hash-consing of opaque terms
letouzey
2013-08-20
*
Repair coqcheck : constant_body constraints are also future
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
*
Cleanup code in term_typing
gareuselesinge
2013-08-19
*
abstract+Defined: create opaque sub proofs (as pre-ParalITP)
gareuselesinge
2013-08-19
*
Tooltips can be augmented with custom widgets, still not clickable
gareuselesinge
2013-08-19
*
Setting tooltip font monospace.
ppedrot
2013-08-12
*
Fixing potentially misused Errors.push.
ppedrot
2013-08-12
*
Automatic backtracking if locked zone is edited
gareuselesinge
2013-08-11
*
Mutual proofs cannot be delegated
gareuselesinge
2013-08-11
*
Printing any backtrace in debug mode, not only anomalies.
ppedrot
2013-08-10
*
Small typos
ppedrot
2013-08-10
*
Lemmas ending with Defined cannot be delegated to slaves
gareuselesinge
2013-08-10
*
Adding the processed tag to comments in CoqIDE.
ppedrot
2013-08-09
*
Fix batch compilation of scripts with Admitted proofs (in a section)
gareuselesinge
2013-08-09
*
checker validation fixed w.r.t. Futures
gareuselesinge
2013-08-09
*
checker validation made a bit more verbose
gareuselesinge
2013-08-09
*
fix batch compilation of scripts containing Admitted
gareuselesinge
2013-08-09
*
state_id data type
gareuselesinge
2013-08-09
*
Gtk check_buttons do have a label
gareuselesinge
2013-08-08
*
calling interp by hand is forbidden
gareuselesinge
2013-08-08
*
Add a (very minimal) Proof General mode to CoqIDE
gareuselesinge
2013-08-08
*
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
*
Test for Paral-ITP
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
*
Fix testsuite so that it works with STM
gareuselesinge
2013-08-08
*
Manual fixed w.r.t. STM
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Side effect free implementation of admit (Isabelle's oracle)
gareuselesinge
2013-08-08
*
Vcs data structure (Git inspired builder for Dag)
gareuselesinge
2013-08-08
*
Dag data structure
gareuselesinge
2013-08-08
*
Searchable stack data structure
gareuselesinge
2013-08-08
*
Future library to represent pure computations
gareuselesinge
2013-08-08
*
Fixing a warning in CoqIDE compilation.
ppedrot
2013-08-08
*
Small fix in IStream interface.
ppedrot
2013-08-08
*
Removing association lists in Constrintern.
ppedrot
2013-08-07
[prev]
[next]