aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Porting the ssrmatching plugin to the new EConstr API.Gravatar Enrico Tassi2017-02-14
* | Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Fix a mishandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-02-14
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
* | Omega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Micromega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Setoid_ring API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Patternops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
| |\
| * | Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07