From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- test-suite/success/Scopes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/success/Scopes.v') diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 55d8343e..a79d28fa 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -3,6 +3,6 @@ Require Import ZArith. Module A. -Definition opp := Zopp. +Definition opp := Z.opp. End A. Check (A.opp 3). -- cgit v1.2.3