Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | | | 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 | |
| |\ \ \ \ | ||||
| * \ \ \ \ | Merge PR#482: [toplevel] Remove unusable option -notop | Maxime Dénès | 2017-03-22 | |
| |\ \ \ \ \ | ||||
| | | | * | | | Add a few comments in term_typing.ml. | Maxime Dénès | 2017-03-21 | |
| | | | * | | | Do not typecheck twice the type of opaque constants. | Maxime Dénès | 2017-03-21 | |
| | | |/ / / | ||||
| * | | | | | Merge PR#134: Enable `-safe-string` | Maxime Dénès | 2017-03-21 | |
| |\ \ \ \ \ | ||||
| | | | * | | | In the Kami project, that causes a stack overflow in one of the example files | Paul Steckler | 2017-03-20 | |
| | * | | | | | [misc] Remove warnings about String.set | Emilio Jesus Gallego Arias | 2017-03-20 | |
| | * | | | | | [safe-string] Enable -safe-string ! | Emilio Jesus Gallego Arias | 2017-03-14 | |
| | * | | | | | [safe_string] library/nameops | Emilio Jesus Gallego Arias | 2017-03-14 | |
| | * | | | | | [safe_string] kernel/cemitcodes | Emilio Jesus Gallego Arias | 2017-03-14 | |
| | | * | | | | [toplevel] Remove unusable option -notop | Emilio Jesus Gallego Arias | 2017-03-14 | |
| | * | | | | | [safe-string] kernel/nativevalues | Emilio Jesus Gallego Arias | 2017-03-14 | |
| | * | | | | | [safe_string] kernel/term_typing | Emilio Jesus Gallego Arias | 2017-03-14 | |
| | |/ / / / | ||||
| * / / / / | [future] Remove unused parameter greedy. | Emilio Jesus Gallego Arias | 2017-03-14 | |
| |/ / / / | ||||
| | | | * | Do not recompute twice the whnf of terms in conversion. | Pierre-Marie Pédrot | 2017-02-27 | |
| | | |/ | | |/| | ||||
| * | | | Merge PR#189: Remove tabulation support from pretty-printing. | Maxime Dénès | 2017-02-20 | |
| |\ \ \ | ||||
| | | | * | Optimizing array mapping in the kernel. | Pierre-Marie Pédrot | 2017-02-19 | |
| | | |/ | ||||
* | | | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 | |
|\| | | | ||||
* | | | | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot | 2017-02-14 | |
| * | | | Merge PR#393: Replace Typeops with Fast_typeops | Maxime Dénès | 2017-02-08 | |
| |\ \ \ | ||||
| * \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-02-01 | |
| |\ \ \ \ | | | |_|/ | | |/| | | ||||
| | * | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2017-02-01 | |
| | |\ \ \ | ||||
| | | | * | | Remove useless comments | Gaetan Gilbert | 2017-01-28 | |
| | | * | | | [native comp] Improve error message on linking error. | Emilio Jesus Gallego Arias | 2017-01-26 | |
| | * | | | | Do not add redundant side effects in tactic code. | Pierre-Marie Pédrot | 2017-01-20 | |
| * | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-01-19 | |
| |\| | | | | ||||
| | * | | | | Mapping named_context_val preserves sharing when possible. | Pierre-Marie Pédrot | 2017-01-17 | |
| | | * | | | Handle application of a primitive projection to a not yet evaluated cofixpoin... | Guillaume Melquiond | 2016-12-26 | |
| | * | | | | Handle application of a primitive projection to a not yet evaluated cofixpoin... | Guillaume Melquiond | 2016-12-23 | |
| * | | | | | Fixing injection in the presence of let-in in constructors. | Hugo Herbelin | 2016-12-22 | |
| | | | * | | Replace Typeops by Fast_typeops | Gaetan Gilbert | 2016-12-12 | |
| | | | * | | Extend Fast_typeops to be a replacement for Typeops | Gaetan Gilbert | 2016-12-12 | |
| | |_|/ / | |/| | | | ||||
| * | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-12-07 | |
| |\| | | |