Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR#537: Efficient side-effect abstraction | Maxime Dénès | 2017-04-11 |
|\ | |||
* \ | 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 |
| | |_|/ | |/| | | |||
* | | | | 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 |
| |/ / / | |||
| * | | | 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 |
| | |_|/ / | |/| | | |