aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-17 10:34:57 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-17 10:34:57 +0000
commit1011266b84371b34536dd5aa5afb3a44b8f8d53c (patch)
treed36b17a2127b1d9df2135b04f7b4f4e28f096615 /Makefile.common
parent6ffdff6e96aa52ca8512634c4bf1bba4252b91d6 (diff)
Merge subinstances branch by me and Tom Prince.
This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions