aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Merge PR#646: Revised behavior on ill-formed identifiersGravatar Maxime Dénès2017-05-23
|\
* \ Merge PR#518: Faster universe unificationGravatar Maxime Dénès2017-05-23
|\ \
| | * Revised behavior on ill-formed identifiers.Gravatar Hugo Herbelin2017-05-20
| |/ |/|
* | Merge PR#572: Replacing costly merges in UGraph.Gravatar Maxime Dénès2017-05-11
|\ \
* \ \ Merge PR#602: Fix more warningsGravatar Maxime Dénès2017-05-03
|\ \ \
* \ \ \ Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \ \
| | * | | Remove dead code in native compiler.Gravatar Maxime Dénès2017-05-02
| |/ / / |/| | |
* | | | Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\ \ \ \
* | | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | | | | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \ \ \ \
| | * | | | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | * | | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | * | | | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | * | | | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
| |/ / / / |/| | | |
| | | | * Fast path when checking equality of universe levels in UState.Gravatar Pierre-Marie Pédrot2017-04-27
| |_|_|/ |/| | |
* | | | COMMENT: Pre_env.envGravatar Matej Kosik2017-04-20
* | | | correcting a typo in a commentGravatar Matej Kosik2017-04-20
* | | | correcting comments in the "Context" moduleGravatar Matej Kosik2017-04-20
* | | | simplifying "Environ.push_named" functionGravatar Matej Kosik2017-04-20
* | | | refactoring "Names.DirPath.is_empty" functionGravatar Matej Kosik2017-04-20
* | | | refactoring "Names.DirPath.compare" functionGravatar Matej Kosik2017-04-20
* | | | refactoring "Names.DirPath.equal" functionGravatar Matej Kosik2017-04-20
| | | * Replacing costly merges in UGraph.Gravatar Pierre-Marie Pédrot2017-04-18
| |_|/ |/| |
* | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \ \
* \ \ \ Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \ \
| * | | | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | | | | Merge PR#549: Fast path in weak head reduction of applied atoms.Gravatar Maxime Dénès2017-04-11
|\ \ \ \ \
| | | | | * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
| |_|_|_|/ |/| | | |
* | | | | Merge PR#537: Efficient side-effect abstractionGravatar Maxime Dénès2017-04-11
|\ \ \ \ \
| | | | | * Documenting how the recursive indices of a fixpoint are computed.Gravatar Hugo Herbelin2017-04-09
| | | | |/ | | | |/|
| | * / | Fast path in weak head reduction of applied atoms.Gravatar Pierre-Marie Pédrot2017-04-08
| | |/ /
* | | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \ \ \ | | |/ / | |/| |
| * | | Merge PR#519: Faster side effectsGravatar Maxime Dénès2017-04-07
| |\ \ \
| | * | | Inline the only use of hcons_j in Term_typing.Gravatar Pierre-Marie Pédrot2017-04-07
| | * | | Documenting the fact terms are only hashconsed outside of a section.Gravatar Pierre-Marie Pédrot2017-04-06
| * | | | Merge PR#434: Optimizing array mapping in the kernel.Gravatar Maxime Dénès2017-04-05
| |\ \ \ \
| | | | * | Fix substitution of abstracted lemmas.Gravatar Pierre-Marie Pédrot2017-04-04
| | |_|/ / | |/| | |
| | | | * Fix bug #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
* | | | | Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
| | | * | More efficient check in validity of side-effects.Gravatar Pierre-Marie Pédrot2017-03-27
| | | * | Adding the size of the opaquetab in its representation.Gravatar Pierre-Marie Pédrot2017-03-27
| | | * | Fix hashconsing of terms in the kernel.Gravatar Pierre-Marie Pédrot2017-03-27
| | |/ / | |/| |
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| | |
| * | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
| |\ \ \ | | | |/ | | |/|
| | * | Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
| | * | Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
| | * | Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
| * | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\| |
| * | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
| |\ \ \