aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Expand)AuthorAge
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* primproj: fix bug 5245, hnf on proj with simpl never flag.Gravatar Matthieu Sozeau2017-08-25
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| * Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* 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
* Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Eliminating parts of the right-hand side compatibility layerGravatar 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
* Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cbv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping 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
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | 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
|/
* 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
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* 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
* | Monotonizing the Evarutil module.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-11-22 16:47:45 +0000