aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun.ml
Commit message (Expand)AuthorAge
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-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] Make location optional in Loc.locatedGravatar 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
* [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
* Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\
* \ 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
| * | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
| | * Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |/
* | Definining EConstr-based contexts.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
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | 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
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | More conversion functions in the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\ \
| * | Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
| * | Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* | | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
|/ /
* | Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 03:18:56 +0000