aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
2017-04-04Bad correction in previous commitJulien Forest
2017-04-04Solving first problem in bug #4306. TO DO : solve the let in problemJulien Forest
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-24"Standardizing" the name LocalPatten into LocalRawPattern.Hugo Herbelin
2017-03-23Improving the API of constrexpr_ops.mli.Hugo Herbelin
2017-03-23Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#495: funind: Ignore missing info for current functionMaxime Dénès
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
2017-03-22funind: Ignore missing info for current functionTej Chajed
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Funind API using EConstr.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Elim API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-12-12Extend Fast_typeops to be a replacement for TypeopsGaetan Gilbert
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-25That Function is unable to create a Fixpoint equation is a user problem,Yves Bertot
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-22Merge remote-tracking branch 'github/pr/283' into trunkMaxime Dénès
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Matej Kosik
2016-08-29CLEANUP: taking advantage of "_ % _" operator to express function composition...Matej Kosik
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 16:45:21 +0000