aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * 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
* | | CLEANUP: removing unnecessary variable bindingGravatar Matej Kosik2016-08-24
| * | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* / CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
|/
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 20:54:51 +0000