aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
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
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Declaremods: a few syntactic improvementsletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Mod_subst: misc reformulationsletouzey
2013-02-24Reduced the noise level when dynlinking in bytecode mode or whenmdenes
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 07:15:25 +0000