diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-28 16:51:18 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-31 10:03:57 -0400 |
| commit | 595c5457b6821403d071088588cf9c2c00cc1d0d (patch) | |
| tree | 827f76d14a96d8eda06c5af4ba60291d52c36975 /src/Util/AdditionChainExponentiation.v | |
| parent | a8f0148ef74356e7e11faede459cd271503d088f (diff) | |
Removed lingering SearchAbout.
Diffstat (limited to 'src/Util/AdditionChainExponentiation.v')
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index 39e2a2770..b0aae0f91 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -32,7 +32,6 @@ Section AddChainExp. Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}. Local Infix "=" := eq : type_scope. Local Open Scope N_scope. - SearchAbout (N -> nat). Local Notation "n * P" := (scalarmult (N.to_nat n) P) (only parsing). Lemma fold_chain_exp' : forall (x:G) is acc ref |