aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)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 2)letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-03-12Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentletouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:12:29 +0000