aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constr_matching.mli
Commit message (Expand)AuthorAge
* Do not compute constr matching context if not used.Gravatar Pierre-Marie Pédrot2018-04-10
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
* Remove up-to-conversion matching functions.Gravatar Pierre-Marie Pédrot2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 20:01:26 +0000