aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evardefine.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Actually exporting delayed universes in the EConstr implementation.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
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics 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
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 02:36:14 +0000