aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-28Native compiler: library compilation errors are now non fatal.mdenes
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23CList.prefix_of and CList.drop_prefix with a parametric equalityletouzey
2013-10-22Removing some generic equalities.ppedrot
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-18Summary: if an unfreeze function fails, print an error messagegareuselesinge
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-12Minimal implementation of `Shallow marshalling of Libgareuselesinge
2013-08-30summary for ML modules made correctgareuselesinge
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-30recdef: restore old semantics (pre STM)gareuselesinge
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-19abstract+Defined: create opaque sub proofs (as pre-ParalITP)gareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-04Removing useless casts between arrays and lists.ppedrot
2013-07-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
2013-07-17Modops.destr_functor without useless envletouzey
2013-07-17Lib.contents () instead of Lib.contents_after Noneletouzey
2013-07-17More dynamic argument scopesletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-09Cosmetic changegareuselesinge
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-05-06Summary: support selective freezegareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-23Fix issues with "Reset Initial" in scripts given to coqtop -lletouzey
2013-04-23coqtop -compile: avoid with_heavy_rollback when non-interactiveletouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-04-22Declaremods: some more minor cleanupletouzey
2013-04-15Minor simplifications in Declaremods and Safe_typingletouzey
2013-04-15Declaremods: drop some useless stuff (slight gain in vo size)letouzey
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-28Safe_typing+Libary: use some arrays instead of lists in vo structuresletouzey
2013-03-26Synchronizing loadpath with the backtrack mechanism.ppedrot
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-21Removing mandatory suffixes for library files.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 02:37:51 +0000