Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 |
|\ | |||
* | | Porting the ssrmatching plugin to the new EConstr API. | Enrico Tassi | 2017-02-14 |
* | | Quick hack to fix interpretation of patterns in Ltac. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Removing most nf_enter in tactics. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Fix a mishandled exception in Omega. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | 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 compatibility layers from Tacticals | Pierre-Marie Pédrot | 2017-02-14 |
* | | Omega API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Micromega API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Funind API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Removing compatibility layers related to printing. | 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 |
* | | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Setoid_ring API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Cc API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Quote API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 |
* | | Rewrite API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Hints API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Inv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Contradiction API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Equality API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Elim API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Hipattern 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 |
* | | Cleaning up opening of the EConstr module in pretyping folder. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Unification API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Pretyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Cases API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Tacred API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Constr_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Patternops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Typing API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Evarconv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Evarsolve API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | Retyping 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 PR#393: Replace Typeops with Fast_typeops | Maxime Dénès | 2017-02-08 |
| |\ | |||
| * | | Revert "Extraction: avoid deprecated functions of module String" | Pierre Letouzey | 2017-02-07 |