aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
...
| * | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| |\ \ \ | |/ / / |/| | |
| * | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| * | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| |\ \ \
* | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
* | | | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
* | | | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
* | | | | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
| |/ / / |/| | |
| | * | Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |/ / |/| |
* | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
* | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ | | |/ | |/|
| * | Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| |\ \
| * | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | * | funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| |/ /
* | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | * Merge branch 'master'.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 various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | * Funind API using EConstr.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
| | * Reductionops now return EConstrs.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
| | * Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | * Tacred 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
| | * Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | * Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
| |/ |/|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
* | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| * | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ /
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: taking advantage of "_ % _" operator to express function composition...Gravatar Matej Kosik2016-08-29
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:32:57 +0000