aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* 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
* Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\
| * \ Merge commit 'a799600' into v8.6Gravatar Maxime Dénès2016-10-25
| |\ \
| | * | That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| * | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| |/ /
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | * [pp] Use more convenient pp API in ssrmatchingGravatar Emilio Jesus Gallego Arias2016-10-18
| | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Ncring_initial: avoid a notation overridingGravatar Pierre Letouzey2016-09-29
| * Extraction: ignore some useless stuff about universesGravatar Pierre Letouzey2016-09-29
| * Ring_theory: avoid overriding a few notationsGravatar Pierre Letouzey2016-09-28
| * Adding interface files to Nsatz ML files.Gravatar Pierre-Marie Pédrot2016-09-28
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 15:08:03 +0000