aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.ml
Commit message (Expand)AuthorAge
...
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\
* \ Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \
| | * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| |/ |/|
| * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \
* | | 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
* | | Evar-normalizing functions now act on EConstrs.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 some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Elim API using EConstr.Gravatar 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
* | | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Typing 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
| * | Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
|/ /
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
* | 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: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
| |/ |/|
| * 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
|/
* 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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
* | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
* | 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
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* | | More conversion functions in the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
* | | Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 05:38:40 +0000