aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
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
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-24CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-08-24CLEANUP: removing unnecessary variable bindingMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-08-11CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16Fixing printing of Function.Hugo Herbelin
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-26Univs/Program/Function: Fix bug #4725Matthieu Sozeau
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27Fixing printing of Function.Hugo Herbelin
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:32:14 +0000