aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* 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
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
* | Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
* | | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | * Univs/Program/Function: Fix bug #4725Gravatar Matthieu Sozeau2016-05-26
* | | Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Revert "Fixing printing of Function."Gravatar Hugo Herbelin2016-04-27
* | | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
* | | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
* | | Fixing printing of Function.Gravatar Hugo Herbelin2016-04-27
* | | Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 14:45:23 +0000