aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
* Prevent States.intern_state and System.extern_intern from looking up files in...Gravatar Guillaume Melquiond2015-09-29
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Update headers.Gravatar Maxime Dénès2015-01-12
* Summary: more surgery functionsGravatar Enrico Tassi2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* recdef: restore old semantics (pre STM)Gravatar gareuselesinge2013-08-30
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* coqtop -compile: avoid with_heavy_rollback when non-interactiveGravatar letouzey2013-04-23
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Protection against anomaly when loading a state with bad magic number.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* moved magic numbers to configure (share coq/coqchk)Gravatar barras2008-07-24
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Un peu de delta-réduction...Gravatar herbelin2006-08-31
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* - erreurs PretypeGravatar filliatr1999-12-10
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* with_heavy_rollback deplace dans StatesGravatar filliatr1999-09-29
* modules System, Lib et StatesGravatar filliatr1999-09-10