aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/merge.ml
Commit message (Expand)AuthorAge
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| * 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
* | 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
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics 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
|/
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* 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: minor readability improvementsGravatar 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
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/ /
* | Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* | Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
| * Add corresponding field in `VernacInductive`.Gravatar Arnaud Spiwack2015-06-24
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 03:41:57 +0000