aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/find_subterm.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Revert "Fixing #1225: we now skip the canonically built binding contexts of"Gravatar Hugo Herbelin2015-11-10
* | Fixing #1225: we now skip the canonically built binding contexts ofGravatar Hugo Herbelin2015-11-10
|/
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 19:55:59 +0000