aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/locusops.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
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Moving function about locs in locusops.Gravatar Hugo Herbelin2014-10-13
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Modulification of identifierGravatar ppedrot2012-12-14
* More equality functionsGravatar ppedrot2012-11-25
* Updating headers.Gravatar herbelin2012-08-08
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29