aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/find_subterm.ml
Commit message (Expand)AuthorAge
* 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 PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | 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
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\
| * Reverting dbdff037 which does not seem to prevent to have #3638 fixedGravatar Hugo Herbelin2016-06-09
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Continuing fixing nested but convertible occurrences in find_subtermGravatar Hugo Herbelin2014-11-19
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Dead code + typo.Gravatar Hugo Herbelin2014-10-26
* 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
* Do not try to match on a subterm that is not closed in find_subterm.Gravatar Matthieu Sozeau2014-09-18
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28