aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-30Remove Obj.magic from safe typinggareuselesinge
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-25Replacing lists by sets in clear tactic.ppedrot
2013-08-23Fix computation of discharged hyps for inductive types forgetting the conclus...msozeau
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
2013-08-20Partial revert of r16711letouzey
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Declareops + Modops : more clever substitutionsletouzey
2013-08-20Mod_typing : code cleanupletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-20Attempt to restore hash-consing of opaque termsletouzey
2013-08-19Cleanup code in term_typinggareuselesinge
2013-08-19abstract+Defined: create opaque sub proofs (as pre-ParalITP)gareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-04Fixing #2846: Uncaught exception Reduction.NotArity.ppedrot
2013-08-04Removing useless casts between arrays and lists.ppedrot
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-07-17Modops.destr_functor without useless envletouzey
2013-07-17Safe_typing: minor factorisationletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-07-06Fixing a bug in the native compiler, introduced by r16363, leading to undefinedmdenes
2013-05-30comments in mlipboutill
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
2013-05-12Removing Gmap from Extraction pluginppedrot
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-04-15Minor simplifications in Declaremods and Safe_typingletouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-04-03Removing two Pervasives.compare from Term.ppedrot
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-04-02Minor cleanup concerning Mod_subst.MBImapletouzey
2013-03-28Safe_typing+Libary: use some arrays instead of lists in vo structuresletouzey
2013-03-28Safe_library : a record type for compiled_library instead of large tupleletouzey
2013-03-25Native compiler: hash-consing of generated code and values.mdenes
2013-03-25Native compiler: Inlined constants are now compiled, fixing a bug reported bymdenes
2013-03-25 Comments in mlipboutill
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:23:59 +0000