Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Extend definition of inductives to include subtyping info | Amin Timany | 2017-06-16 | |
* | | Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613 | Maxime Dénès | 2017-06-14 | |
|\ \ | ||||
* \ \ | Merge PR#448: Do not recompute twice the whnf of terms in conversion. | Maxime Dénès | 2017-06-14 | |
|\ \ \ | ||||
| | | * | Remove some useless code in Term_typing | Gaëtan Gilbert | 2017-06-13 | |
| |_|/ |/| | | ||||
* | | | Merge PR#714: Print feature Proof-of-Concept (episode 2) | Maxime Dénès | 2017-06-13 | |
|\ \ \ | ||||
* | | | | Remove (useless) aliases from the API. | Matej Košík | 2017-06-10 | |
| | | * | [kernel] Improve proof using message, fixes bugzilla #3613 | Emilio Jesus Gallego Arias | 2017-06-07 | |
* | | | | Put all plugins behind an "API". | Matej Kosik | 2017-06-07 | |
| |_|/ |/| | | ||||
* | | | Merge PR#728: A few typos. | Maxime Dénès | 2017-06-06 | |
|\ \ \ | ||||
| | * | | Added support for a side effect on constants in reduction functions. | Thomas Sibut-Pinote | 2017-06-04 | |
| * | | | A few typos. | Hugo Herbelin | 2017-06-04 | |
| |/ / | ||||
* / / | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | 2017-06-02 | |
|/ / | ||||
* | | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | 2017-05-31 | |
* | | Merge PR#555: Missing optimization when Kernel Term Sharing is disabled. | Maxime Dénès | 2017-05-29 | |
|\ \ | ||||
* | | | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | 2017-05-27 | |
* | | | 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 | |
| | | | | * | | Missing optimization when Kernel Term Sharing is disabled. | Pierre-Marie Pédrot | 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 | |
| |\ \ \ \ |