From 595c5457b6821403d071088588cf9c2c00cc1d0d Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 28 Aug 2016 16:51:18 -0400 Subject: Removed lingering SearchAbout. --- src/Util/AdditionChainExponentiation.v | 1 - 1 file changed, 1 deletion(-) (limited to 'src/Util/AdditionChainExponentiation.v') 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 -- cgit v1.2.3