diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 10:34:57 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 10:34:57 +0000 |
| commit | 1011266b84371b34536dd5aa5afb3a44b8f8d53c (patch) | |
| tree | d36b17a2127b1d9df2135b04f7b4f4e28f096615 /theories/Numbers/Cyclic | |
| parent | 6ffdff6e96aa52ca8512634c4bf1bba4252b91d6 (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 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index c30d38186..00a840520 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -285,7 +285,7 @@ Section Z_2nZ. (* ** Record of operators on 2 words *) - Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) := + Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 := ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 @@ -305,7 +305,7 @@ Section Z_2nZ. sqrt2 sqrt. - Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) := + Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 := ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 |