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