aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
|/
* Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Gravatar Maxime Dénès2017-11-24
|\
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/
* Merge PR #6058: Remove redundant env argument to Reduction.ccnvGravatar Maxime Dénès2017-11-15
|\
* | [ci] [coq] Complete 4.06.0 support.Gravatar Emilio Jesus Gallego Arias2017-11-13
* | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* | [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* | [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| * Remove redundant env argument to Reduction.ccnvGravatar Gaëtan Gilbert2017-11-02
|/
* A missing newline after a comment.Gravatar Hugo Herbelin2017-10-24
* Merge PR #1155: Use type nonrec in some functor arguments.Gravatar Maxime Dénès2017-10-20
|\
* | [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
| * Use type nonrec in some functor arguments.Gravatar Gaëtan Gilbert2017-10-16
|/
* Merge PR #1103: Take Suggest Proof Using outside the kernel.Gravatar Maxime Dénès2017-10-13
|\
| * Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
* | [flambda] [native] Pass `-Oclassic` to the native compiler.Gravatar Emilio Jesus Gallego Arias2017-10-10
|/
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
* | [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
| * Remove unused Failure catchGravatar Gaëtan Gilbert2017-09-29
| * Remove some duplication between Typeops and Nativenorm.Gravatar Gaëtan Gilbert2017-09-29
* | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
| * Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* | Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ | |/ |/|
* | Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #931: Parametrize module bodyGravatar Maxime Dénès2017-09-07
|\ \ \
| | * | Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
| |/ / |/| |
* | | Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\ \ \
| | * | Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
| | * | Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* | | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \ \ | |_|/ / |/| | |
| | * | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| |/ / |/| |
| * | Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
* | | Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Gravatar Hugo Herbelin2017-08-12
|/ /
* | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | * kernel: bugfix in filter_stack_domain.Gravatar Matthieu Sozeau2017-07-26
| |/
* | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* | Avoiding a variable shadowing in the kernel.Gravatar Pierre-Marie Pédrot2017-07-26
* | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* | Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* | Remove a horrendous hack in Declare to retrieve exported side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* | More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* | Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
* | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25