aboutsummaryrefslogtreecommitdiff
path: root/library/summary.mli
AgeCommit message (Expand)Author
2021-01-22Properly implement local references in Summary.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-09Simplify the implementation of Summary by specifying the type of ML-MODULES.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 2JPR
2018-12-13Move shallow state logic to the function preparing state for workersMaxime 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 / libraryEmilio Jesus Gallego Arias
2018-02-27Update 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-20Documenting the purity / marshallability invariant of persistent states.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-09-05Summary: simpler API for process-local storageEnrico Tassi
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-04Specializing the Dyn module to each usecase.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-17Summary: more surgery functionsEnrico Tassi
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2013-08-30summary for ML modules made correctgareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-05-06Summary: support selective freezegareuselesinge
2013-04-22code simplifications concerning Summaryletouzey
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-02-03Allow to turn contrib/subtac into a (nat)dynlink'able pluginletouzey
2004-07-16Nouvelle en-têteherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-02-24False dependencies in summarycoq
2002-08-02Modules dans COQ\!\!\!\!coq
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
1999-09-10modules System, Lib et Statesfilliatr
1999-09-03modules Libobject et Summary (partiel)filliatr