index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
library
/
summary.mli
Age
Commit message (
Expand
)
Author
2021-01-22
Properly implement local references in Summary.
Pierre-Marie Pédrot
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-12-09
Simplify the implementation of Summary by specifying the type of ML-MODULES.
Pierre-Marie Pédrot
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-23
Fixing typos - Part 2
JPR
2018-12-13
Move shallow state logic to the function preparing state for workers
Maxime Dénès
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-05-30
[api] Remove deprecated objects in engine / interp / library
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-09
[summary] Adapt STM to the new Summary API.
Emilio Jesus Gallego Arias
2017-12-09
[summary] Allow typed projections from global state + rework of internals.
Emilio Jesus Gallego Arias
2017-07-20
Documenting the purity / marshallability invariant of persistent states.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-09-05
Summary: simpler API for process-local storage
Enrico Tassi
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-12-04
Specializing the Dyn module to each usecase.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-17
Summary: more surgery functions
Enrico Tassi
2014-01-05
STM: modules do not prevent proofs from being ASync
Enrico Tassi
2013-08-30
summary for ML modules made correct
gareuselesinge
2013-08-08
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-05-06
States: frozen states can hold closures
gareuselesinge
2013-05-06
Summary: support selective freeze
gareuselesinge
2013-04-22
code simplifications concerning Summary
letouzey
2012-08-08
Updating headers.
herbelin
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-06-22
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2009-08-13
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-02-03
Allow to turn contrib/subtac into a (nat)dynlink'able plugin
letouzey
2004-07-16
Nouvelle en-tête
herbelin
2003-10-07
Correction du bug 335 et Export/Require Export dans un module
coq
2003-02-24
False dependencies in summary
coq
2002-08-02
Modules dans COQ\!\!\!\!
coq
2001-03-15
entetes
filliatr
2000-12-12
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-11-24
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
1999-09-10
modules System, Lib et States
filliatr
1999-09-03
modules Libobject et Summary (partiel)
filliatr