Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | * | | | | | | | | Preliminary work before extending support for binders in notations | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Make pattern variables of "match" substitutable in notations. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Supporting recursive notations reversing the left-to-right order. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Allowing variables used in recursive notation to occur several times in pattern. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Allows recursive patterns for binders to be associative on the left. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Fixing/improving notations with recursive patterns. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | A bit of miscellaneous code documentation around notations. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Notations: documenting structure collecting variables occurring in notation. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Renaming binders into binderlists in egramcoq.ml. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Introducing an intermediary type "constr_prod_entry_key" for grammar producti... | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Canonically add an encoding in glob_constr of "as" operator for cases_pattern. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Minor clarifying of name variables in constrintern.ml. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Using name given by user to name a 'pat, if any. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Rephrasing ETBinderList with a self-documenting and invariant-carrying argument. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Notations: Do not consider a non-occurring variable as a binder-only variable. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | More precise explanation when a notation is not reversible for printing. | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Adding support for re-folding notation referring to isolated "forall '(x,y), t". | Hugo Herbelin | 2018-02-20 | |
| | | | * | | | | | | | | Again one more step in fixing #5762 ("where" clause). | Hugo Herbelin | 2018-02-20 | |
| |_|_|/ / / / / / / / |/| | | | | | | | | | | ||||
| | | | * | | | | | | | ci: add elpi | Enrico Tassi | 2018-02-19 | |
| | | | * | | | | | | | record: restore API declare_projections (removed in e414c07e1) | Enrico Tassi | 2018-02-19 | |
| | | | * | | | | | | | pretyping: restore API understand_judgment_tcc (now understand_tcc_ty) | Enrico Tassi | 2018-02-19 | |
| |_|_|/ / / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #6728: Extrude monomorphic universe contexts from with Definition co... | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6761: Remove unused argument in Record.declare_structure | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t` | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6753: [toplevel] Make toplevel state into a record. | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | | | Fix #6529: nf_evar_info and check the env evars' not just the concl | Matthieu Sozeau | 2018-02-19 | |
* | | | | | | | | | | | | | | Merge PR #6230: Better Cemitcodes API + compact relocation representation | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6759: detype_case predicate is not optional | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6772: Cleanup inferCumulativity | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6648: [tactics] make apply_type safe | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ... | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds. | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6571: Fix ci-all target | Maxime Dénès | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | | | | | | | | | | | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle | 2018-02-17 | |
| | | | | * | | | | | | | | | | | | | | | | | apply_type: add option "typecheck" passed down to refine | Enrico Tassi | 2018-02-16 | |
| |_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | | | Cleaner treatment of parameters in inferCumulativity | Gaëtan Gilbert | 2018-02-16 | |
| | | | | * | | | | | | | | | | | | | | | | Fix reduction flags in inferCumulativity | Gaëtan Gilbert | 2018-02-16 | |
| |_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | | Adding a test for the construction that was broken in Coccinelle. | Pierre-Marie Pédrot | 2018-02-16 | |
| | | | | | | | | | * | | | | | | | | | | Extrude monomorphic universe contexts from with Definition constraints. | Pierre-Marie Pédrot | 2018-02-16 | |
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | Adding a test for variance subtyping in the module system. | Pierre-Marie Pédrot | 2018-02-15 | |
| | | | | | | | | | * | | | | | | | | | Adding a sanity check on inductive variance subtyping. | Pierre-Marie Pédrot | 2018-02-15 | |
| |_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | | [toplevel] Make toplevel state into a record. | Emilio Jesus Gallego Arias | 2018-02-15 | |
| | | | | | | * | | | | | | | | | | | [ide] Localize a IDE-specific flag. | Emilio Jesus Gallego Arias | 2018-02-15 | |
| |_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarter | Maxime Dénès | 2018-02-15 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | | | | | disable tests: vio2vo is broken in Windows | Ralf Jung | 2018-02-15 | |
| * | | | | | | | | | | | | | | | | | also test vio2vo | Ralf Jung | 2018-02-15 | |
| * | | | | | | | | | | | | | | | | | test "make quick2vo" | Ralf Jung | 2018-02-15 | |
| * | | | | | | | | | | | | | | | | | new quick2vo target: like vio2vo, but smarter | Ralf Jung | 2018-02-15 | |
| | |_|_|/ / / / / / / / / / / / / | |/| | | | | | | | | | | | | | | |