aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
* Library: when compiling multiple files, reset the opaque tablesGravatar Enrico Tassi2014-02-26
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
* STM: modules do not prevent proofs from being ASyncGravatar Enrico Tassi2014-01-05
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Patch for supporting [From Xxx Require Yyy Zzz.]Gravatar Gregory Malecha2013-12-12
* Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
* Better implementation of summary unfreezing.Gravatar Pierre-Marie Pédrot2013-11-24
* Using hashes in Summary, like the previous commit did with Dyn.Gravatar Pierre-Marie Pédrot2013-11-22
* Using hashes instead of strings in dynamic tags. In case of collision, anGravatar Pierre-Marie Pédrot2013-11-22
* Partial application hunt.Gravatar ppedrot2013-11-07
* Partial application in Globnames.Gravatar ppedrot2013-11-06
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Native compiler: library compilation errors are now non fatal.Gravatar mdenes2013-10-28
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* CList.prefix_of and CList.drop_prefix with a parametric equalityGravatar letouzey2013-10-23
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Summary: if an unfreeze function fails, print an error messageGravatar gareuselesinge2013-10-18
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Minimal implementation of `Shallow marshalling of LibGravatar gareuselesinge2013-09-12
* summary for ML modules made correctGravatar gareuselesinge2013-08-30
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* recdef: restore old semantics (pre STM)Gravatar gareuselesinge2013-08-30
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* abstract+Defined: create opaque sub proofs (as pre-ParalITP)Gravatar gareuselesinge2013-08-19
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* Simple machinery to detect EXTEND that interpret during parsingGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* Modops.destr_functor without useless envGravatar letouzey2013-07-17
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* More dynamic argument scopesGravatar letouzey2013-07-17
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* Cosmetic changeGravatar gareuselesinge2013-05-09