Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Merge PR#201: Transparent abstract | Maxime Dénès | 2017-05-11 | |
| |\ | ||||
| * | | Remove unused [open] statements | Gaetan Gilbert | 2017-04-27 | |
| * | | Remove some unused values and types | Gaetan Gilbert | 2017-04-27 | |
| | * | Add transparent_abstract tactic | Jason Gross | 2017-04-25 | |
| |/ | ||||
* | | [location] [ast] Port module AST to CAst | 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 | |
|/ | ||||
* | Merge branch 'master' into econstr | Pierre-Marie Pédrot | 2017-04-07 | |
|\ | ||||
* | | Fix a normalization hotspot in computation of constr keys. | Pierre-Marie Pédrot | 2017-04-06 | |
* | | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | 2017-04-01 | |
* | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 | |
| * | Fast path for implicit tactic solving. | Pierre-Marie Pédrot | 2017-03-23 | |
|/ | ||||
* | Ltac as a plugin. | Pierre-Marie Pédrot | 2017-02-17 |