Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | 2017-05-24 |
|\ | |||
| * | Remove unused [open] statements | Gaetan Gilbert | 2017-04-27 |
| * | Remove unused constructors | 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 |
* | | [location] [ast] Port module AST to CAst | Emilio Jesus Gallego Arias | 2017-04-25 |
* | | [location] [ast] Switch Constrexpr AST to an extensible node type. | Emilio Jesus Gallego Arias | 2017-04-25 |
* | | [location] Make location optional in Loc.located | Emilio Jesus Gallego Arias | 2017-04-25 |
* | | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | 2017-04-25 |
* | | [location] Switch glob_constr to Loc.located | Emilio Jesus Gallego Arias | 2017-04-24 |
* | | [location] Use Loc.located for constr_expr. | Emilio Jesus Gallego Arias | 2017-04-24 |
|/ | |||
* | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 |
|\ | |||
* | | [camlpX] Remove camlp4 compat layer. | Emilio Jesus Gallego Arias | 2017-04-07 |
| * | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-04-04 |
| |\ | |/ |/| | |||
| * | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
| |\ | |||
* | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | Hugo Herbelin | 2017-03-24 |
| |/ |/| | |||
* | | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | Maxime Dénès | 2017-03-14 |
|\ \ | |||
* | | | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot | 2017-02-17 |
| * | | [cleanup] Change Id.t option to Name.t in TacFun | Tej Chajed | 2017-02-16 |
|/ / | |||
| * | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 |
| |\ | |/ |/| | |||
| * | Porting the ssrmatching plugin to the new EConstr API. | Enrico Tassi | 2017-02-14 |
| * | Definining EConstr-based contexts. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | 2017-02-14 |
| * | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Goal API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Unification API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Tacred API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Evarconv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Reductionops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | Termops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-01-19 |
|\ \ | |||
| * | | ssrmatching: fix iter_constr_LR iterator wrt Proj | Enrico Tassi | 2016-12-07 |
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-12-07 |
|\| | | |||
| * | | ssrmatching: handle primite projections (fix: #5247) | Enrico Tassi | 2016-12-05 |
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 |
|\| | | |/ |/| | |||
| * | Merge commit 'e6edb33' into v8.6 | Maxime Dénès | 2016-11-07 |
| |\ | |||
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-29 |
|\| | | |||
| * | | Merge remote-tracking branch 'github/pr/319' into v8.6 | Maxime Dénès | 2016-10-28 |
| |\ \ | |||
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-24 |
|\| | | | |||
| * | | | ssrmatching: fix interpretation of rpattern | Enrico Tassi | 2016-10-24 |
| | | * | Renamings to avoid confusion deprecating old names | Matthieu Sozeau | 2016-10-22 |
| | |/ | |/| | |||
| | * | [pp] Use more convenient pp API in ssrmatching | Emilio Jesus Gallego Arias | 2016-10-18 |
| | * | [pp] Add tagging function to all low-level printing calls. | Emilio Jesus Gallego Arias | 2016-10-18 |
| |/ | |||
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-23 |
|\| | |||
* | | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot | 2016-09-21 |