aboutsummaryrefslogtreecommitdiff
path: root/intf/pattern.mli
AgeCommit message (Expand)Author
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-02-14Tactic_matching API using EConstr.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey